:: BCIALG_6 semantic presentation begin definition let D be set ; let f be Function of NAT,D; let n be Nat; :: original: . redefine funcf . n -> Element of D; coherence f . n is Element of D proof reconsider n = n as Element of NAT by ORDINAL1:def_12; f . n is Element of D ; hence f . n is Element of D ; ::_thesis: verum end; end; definition let G be non empty BCIStr_0 ; func BCI-power G -> Function of [: the carrier of G,NAT:], the carrier of G means :Def1: :: BCIALG_6:def 1 for x being Element of G holds ( it . (x,0) = 0. G & ( for n being Element of NAT holds it . (x,(n + 1)) = x \ ((it . (x,n)) `) ) ); existence ex b1 being Function of [: the carrier of G,NAT:], the carrier of G st for x being Element of G holds ( b1 . (x,0) = 0. G & ( for n being Element of NAT holds b1 . (x,(n + 1)) = x \ ((b1 . (x,n)) `) ) ) proof defpred S1[ set , set ] means ex f being Function of NAT, the carrier of G ex x being Element of G st ( $1 = x & f = $2 & f . 0 = 0. G & ( for n being Element of NAT holds f . (n + 1) = x \ ((f . n) `) ) ); A1: for x being set st x in the carrier of G holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier of G implies ex y being set st S1[x,y] ) assume x in the carrier of G ; ::_thesis: ex y being set st S1[x,y] then reconsider b = x as Element of G ; deffunc H1( Nat, Element of G) -> Element of the carrier of G = b \ ($2 `); consider g0 being Function of NAT, the carrier of G such that A2: ( g0 . 0 = 0. G & ( for n being Nat holds g0 . (n + 1) = H1(n,g0 . n) ) ) from NAT_1:sch_12(); reconsider y = g0 as set ; take y ; ::_thesis: S1[x,y] take g0 ; ::_thesis: ex x being Element of G st ( x = x & g0 = y & g0 . 0 = 0. G & ( for n being Element of NAT holds g0 . (n + 1) = x \ ((g0 . n) `) ) ) take b ; ::_thesis: ( x = b & g0 = y & g0 . 0 = 0. G & ( for n being Element of NAT holds g0 . (n + 1) = b \ ((g0 . n) `) ) ) thus ( x = b & g0 = y & g0 . 0 = 0. G ) by A2; ::_thesis: for n being Element of NAT holds g0 . (n + 1) = b \ ((g0 . n) `) let n be Element of NAT ; ::_thesis: g0 . (n + 1) = b \ ((g0 . n) `) thus g0 . (n + 1) = b \ ((g0 . n) `) by A2; ::_thesis: verum end; consider f being Function such that A3: ( dom f = the carrier of G & ( for x being set st x in the carrier of G holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); defpred S2[ Element of G, Element of NAT , set ] means ex g0 being Function of NAT, the carrier of G st ( g0 = f . $1 & $3 = g0 . $2 ); A4: for a being Element of G for n being Element of NAT ex b being Element of G st S2[a,n,b] proof let a be Element of G; ::_thesis: for n being Element of NAT ex b being Element of G st S2[a,n,b] let n be Element of NAT ; ::_thesis: ex b being Element of G st S2[a,n,b] consider g0 being Function of NAT, the carrier of G, h being Element of G such that a = h and A5: g0 = f . a and g0 . 0 = 0. G and for n being Element of NAT holds g0 . (n + 1) = h \ ((g0 . n) `) by A3; take g0 . n ; ::_thesis: S2[a,n,g0 . n] take g0 ; ::_thesis: ( g0 = f . a & g0 . n = g0 . n ) thus ( g0 = f . a & g0 . n = g0 . n ) by A5; ::_thesis: verum end; consider F being Function of [: the carrier of G,NAT:], the carrier of G such that A6: for a being Element of G for n being Element of NAT holds S2[a,n,F . (a,n)] from BINOP_1:sch_3(A4); take F ; ::_thesis: for x being Element of G holds ( F . (x,0) = 0. G & ( for n being Element of NAT holds F . (x,(n + 1)) = x \ ((F . (x,n)) `) ) ) let h be Element of G; ::_thesis: ( F . (h,0) = 0. G & ( for n being Element of NAT holds F . (h,(n + 1)) = h \ ((F . (h,n)) `) ) ) A7: ex g2 being Function of NAT, the carrier of G ex b being Element of G st ( h = b & g2 = f . h & g2 . 0 = 0. G & ( for n being Element of NAT holds g2 . (n + 1) = b \ ((g2 . n) `) ) ) by A3; ex g1 being Function of NAT, the carrier of G st ( g1 = f . h & F . (h,0) = g1 . 0 ) by A6; hence F . (h,0) = 0. G by A7; ::_thesis: for n being Element of NAT holds F . (h,(n + 1)) = h \ ((F . (h,n)) `) let n be Element of NAT ; ::_thesis: F . (h,(n + 1)) = h \ ((F . (h,n)) `) A8: ex g2 being Function of NAT, the carrier of G ex b being Element of G st ( h = b & g2 = f . h & g2 . 0 = 0. G & ( for n being Element of NAT holds g2 . (n + 1) = b \ ((g2 . n) `) ) ) by A3; ( ex g0 being Function of NAT, the carrier of G st ( g0 = f . h & F . (h,n) = g0 . n ) & ex g1 being Function of NAT, the carrier of G st ( g1 = f . h & F . (h,(n + 1)) = g1 . (n + 1) ) ) by A6; hence F . (h,(n + 1)) = h \ ((F . (h,n)) `) by A8; ::_thesis: verum end; uniqueness for b1, b2 being Function of [: the carrier of G,NAT:], the carrier of G st ( for x being Element of G holds ( b1 . (x,0) = 0. G & ( for n being Element of NAT holds b1 . (x,(n + 1)) = x \ ((b1 . (x,n)) `) ) ) ) & ( for x being Element of G holds ( b2 . (x,0) = 0. G & ( for n being Element of NAT holds b2 . (x,(n + 1)) = x \ ((b2 . (x,n)) `) ) ) ) holds b1 = b2 proof let f, g be Function of [: the carrier of G,NAT:], the carrier of G; ::_thesis: ( ( for x being Element of G holds ( f . (x,0) = 0. G & ( for n being Element of NAT holds f . (x,(n + 1)) = x \ ((f . (x,n)) `) ) ) ) & ( for x being Element of G holds ( g . (x,0) = 0. G & ( for n being Element of NAT holds g . (x,(n + 1)) = x \ ((g . (x,n)) `) ) ) ) implies f = g ) assume that A9: for h being Element of G holds ( f . (h,0) = 0. G & ( for n being Element of NAT holds f . (h,(n + 1)) = h \ ((f . (h,n)) `) ) ) and A10: for h being Element of G holds ( g . (h,0) = 0. G & ( for n being Element of NAT holds g . (h,(n + 1)) = h \ ((g . (h,n)) `) ) ) ; ::_thesis: f = g now__::_thesis:_for_h_being_Element_of_G for_n_being_Element_of_NAT_holds_f_._(h,n)_=_g_._(h,n) let h be Element of G; ::_thesis: for n being Element of NAT holds f . (h,n) = g . (h,n) let n be Element of NAT ; ::_thesis: f . (h,n) = g . (h,n) defpred S1[ Element of NAT ] means f . [h,$1] = g . [h,$1]; A11: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A12: S1[n] ; ::_thesis: S1[n + 1] A13: g . [h,n] = g . (h,n) ; f . [h,(n + 1)] = f . (h,(n + 1)) .= h \ ((f . (h,n)) `) by A9 .= g . (h,(n + 1)) by A10, A12, A13 .= g . [h,(n + 1)] ; hence S1[n + 1] ; ::_thesis: verum end; f . [h,0] = f . (h,0) .= 0. G by A9 .= g . (h,0) by A10 .= g . [h,0] ; then A14: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A14, A11); hence f . (h,n) = g . (h,n) ; ::_thesis: verum end; hence f = g by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines BCI-power BCIALG_6:def_1_:_ for G being non empty BCIStr_0 for b2 being Function of [: the carrier of G,NAT:], the carrier of G holds ( b2 = BCI-power G iff for x being Element of G holds ( b2 . (x,0) = 0. G & ( for n being Element of NAT holds b2 . (x,(n + 1)) = x \ ((b2 . (x,n)) `) ) ) ); definition let X be BCI-algebra; let i be Integer; let x be Element of X; funcx |^ i -> Element of X equals :Def2: :: BCIALG_6:def 2 (BCI-power X) . (x,(abs i)) if 0 <= i otherwise (BCI-power X) . ((x `),(abs i)); correctness coherence ( ( 0 <= i implies (BCI-power X) . (x,(abs i)) is Element of X ) & ( not 0 <= i implies (BCI-power X) . ((x `),(abs i)) is Element of X ) ); consistency for b1 being Element of X holds verum; ; end; :: deftheorem Def2 defines |^ BCIALG_6:def_2_:_ for X being BCI-algebra for i being Integer for x being Element of X holds ( ( 0 <= i implies x |^ i = (BCI-power X) . (x,(abs i)) ) & ( not 0 <= i implies x |^ i = (BCI-power X) . ((x `),(abs i)) ) ); definition let X be BCI-algebra; let n be Nat; let x be Element of X; redefine func x |^ n equals :: BCIALG_6:def 3 (BCI-power X) . (x,n); compatibility for b1 being Element of X holds ( b1 = x |^ n iff b1 = (BCI-power X) . (x,n) ) proof let g be Element of X; ::_thesis: ( g = x |^ n iff g = (BCI-power X) . (x,n) ) abs n = n by ABSVALUE:def_1; hence ( g = x |^ n iff g = (BCI-power X) . (x,n) ) by Def2; ::_thesis: verum end; end; :: deftheorem defines |^ BCIALG_6:def_3_:_ for X being BCI-algebra for n being Nat for x being Element of X holds x |^ n = (BCI-power X) . (x,n); theorem Th1: :: BCIALG_6:1 for X being BCI-algebra for x being Element of X for a, b being Element of AtomSet X holds a \ (x \ b) = b \ (x \ a) proof let X be BCI-algebra; ::_thesis: for x being Element of X for a, b being Element of AtomSet X holds a \ (x \ b) = b \ (x \ a) let x be Element of X; ::_thesis: for a, b being Element of AtomSet X holds a \ (x \ b) = b \ (x \ a) let a, b be Element of AtomSet X; ::_thesis: a \ (x \ b) = b \ (x \ a) b in AtomSet X ; then A1: ex y1 being Element of X st ( b = y1 & y1 is atom ) ; (x \ (x \ b)) \ b = 0. X by BCIALG_1:1; then (b \ (x \ a)) \ (a \ (x \ b)) = ((x \ (x \ b)) \ (x \ a)) \ (a \ (x \ b)) by A1, BCIALG_1:def_14; then (b \ (x \ a)) \ (a \ (x \ b)) = ((x \ (x \ a)) \ (x \ b)) \ (a \ (x \ b)) by BCIALG_1:7; then (b \ (x \ a)) \ (a \ (x \ b)) = (((x \ (x \ a)) \ (x \ b)) \ (a \ (x \ b))) \ (0. X) by BCIALG_1:2; then (b \ (x \ a)) \ (a \ (x \ b)) = (((x \ (x \ a)) \ (x \ b)) \ (a \ (x \ b))) \ ((x \ (x \ a)) \ a) by BCIALG_1:1; then A2: (b \ (x \ a)) \ (a \ (x \ b)) = 0. X by BCIALG_1:def_3; a \ (x \ b) <= b \ (x \ a) by BCIALG_1:26; then (a \ (x \ b)) \ (b \ (x \ a)) = 0. X by BCIALG_1:def_11; hence a \ (x \ b) = b \ (x \ a) by A2, BCIALG_1:def_7; ::_thesis: verum end; theorem Th2: :: BCIALG_6:2 for X being BCI-algebra for x being Element of X for n being Nat holds x |^ (n + 1) = x \ ((x |^ n) `) proof let X be BCI-algebra; ::_thesis: for x being Element of X for n being Nat holds x |^ (n + 1) = x \ ((x |^ n) `) let x be Element of X; ::_thesis: for n being Nat holds x |^ (n + 1) = x \ ((x |^ n) `) let n be Nat; ::_thesis: x |^ (n + 1) = x \ ((x |^ n) `) reconsider n = n as Element of NAT by ORDINAL1:def_12; x |^ (n + 1) = x \ ((x |^ n) `) by Def1; hence x |^ (n + 1) = x \ ((x |^ n) `) ; ::_thesis: verum end; theorem Th3: :: BCIALG_6:3 for X being BCI-algebra for x being Element of X holds x |^ 0 = 0. X by Def1; theorem Th4: :: BCIALG_6:4 for X being BCI-algebra for x being Element of X holds x |^ 1 = x proof let X be BCI-algebra; ::_thesis: for x being Element of X holds x |^ 1 = x let x be Element of X; ::_thesis: x |^ 1 = x x |^ 1 = x |^ (0 + 1) .= x \ ((x |^ 0) `) by Def1 .= x \ ((0. X) `) by Def1 .= x \ (0. X) by BCIALG_1:def_5 ; hence x |^ 1 = x by BCIALG_1:2; ::_thesis: verum end; theorem Th5: :: BCIALG_6:5 for X being BCI-algebra for x being Element of X holds x |^ (- 1) = x ` proof let X be BCI-algebra; ::_thesis: for x being Element of X holds x |^ (- 1) = x ` let x be Element of X; ::_thesis: x |^ (- 1) = x ` x |^ (- 1) = (BCI-power X) . ((x `),(abs (- 1))) by Def2; then x |^ (- 1) = (BCI-power X) . ((x `),(- (- 1))) by ABSVALUE:def_1; then x |^ (- 1) = (x `) |^ 1 ; hence x |^ (- 1) = x ` by Th4; ::_thesis: verum end; theorem :: BCIALG_6:6 for X being BCI-algebra for x being Element of X holds x |^ 2 = x \ (x `) proof let X be BCI-algebra; ::_thesis: for x being Element of X holds x |^ 2 = x \ (x `) let x be Element of X; ::_thesis: x |^ 2 = x \ (x `) x |^ 2 = x |^ (1 + 1) .= x \ ((x |^ 1) `) by Def1 ; hence x |^ 2 = x \ (x `) by Th4; ::_thesis: verum end; theorem Th7: :: BCIALG_6:7 for X being BCI-algebra for n being Nat holds (0. X) |^ n = 0. X proof let X be BCI-algebra; ::_thesis: for n being Nat holds (0. X) |^ n = 0. X let n be Nat; ::_thesis: (0. X) |^ n = 0. X defpred S1[ Nat] means (0. X) |^ $1 = 0. X; A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then (0. X) |^ (n + 1) = ((0. X) `) ` by Th2 .= (0. X) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_5 ; hence S1[n + 1] ; ::_thesis: verum end; A2: S1[ 0 ] by Def1; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1); hence (0. X) |^ n = 0. X ; ::_thesis: verum end; theorem :: BCIALG_6:8 for X being BCI-algebra for a being Element of AtomSet X holds (a |^ (- 1)) |^ (- 1) = a proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X holds (a |^ (- 1)) |^ (- 1) = a let a be Element of AtomSet X; ::_thesis: (a |^ (- 1)) |^ (- 1) = a (a |^ (- 1)) |^ (- 1) = (a `) |^ (- 1) by Th5 .= (a `) ` by Th5 ; hence (a |^ (- 1)) |^ (- 1) = a by BCIALG_1:29; ::_thesis: verum end; theorem :: BCIALG_6:9 for X being BCI-algebra for x being Element of X for n being Nat holds x |^ (- n) = ((x `) `) |^ (- n) proof let X be BCI-algebra; ::_thesis: for x being Element of X for n being Nat holds x |^ (- n) = ((x `) `) |^ (- n) let x be Element of X; ::_thesis: for n being Nat holds x |^ (- n) = ((x `) `) |^ (- n) let n be Nat; ::_thesis: x |^ (- n) = ((x `) `) |^ (- n) defpred S1[ Nat] means x |^ (- $1) = ((x `) `) |^ (- $1); A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] set m = - (n + 1); - (- (n + 1)) > 0 ; then A2: - (n + 1) < 0 ; then x |^ (- (n + 1)) = (BCI-power X) . ((x `),(abs (- (n + 1)))) by Def2 .= (BCI-power X) . ((((x `) `) `),(abs (- (n + 1)))) by BCIALG_1:8 .= ((x `) `) |^ (- (n + 1)) by A2, Def2 ; hence S1[n + 1] ; ::_thesis: verum end; x |^ 0 = 0. X by Def1 .= ((x `) `) |^ 0 by Def1 ; then A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence x |^ (- n) = ((x `) `) |^ (- n) ; ::_thesis: verum end; theorem Th10: :: BCIALG_6:10 for X being BCI-algebra for a being Element of AtomSet X for n being Nat holds (a `) |^ n = a |^ (- n) proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for n being Nat holds (a `) |^ n = a |^ (- n) let a be Element of AtomSet X; ::_thesis: for n being Nat holds (a `) |^ n = a |^ (- n) let n be Nat; ::_thesis: (a `) |^ n = a |^ (- n) percases ( n = 0 or n > 0 ) ; supposeA1: n = 0 ; ::_thesis: (a `) |^ n = a |^ (- n) hence (a `) |^ n = 0. X by Def1 .= a |^ (- n) by A1, Th3 ; ::_thesis: verum end; supposeA2: n > 0 ; ::_thesis: (a `) |^ n = a |^ (- n) set m = - n; - (- n) > 0 by A2; then A3: - n < 0 ; then a |^ (- n) = (BCI-power X) . ((a `),(abs (- n))) by Def2 .= (BCI-power X) . ((a `),(- (- n))) by A3, ABSVALUE:def_1 ; hence (a `) |^ n = a |^ (- n) ; ::_thesis: verum end; end; end; theorem :: BCIALG_6:11 for X being BCI-algebra for x being Element of X for n being Nat st x in BCK-part X & n >= 1 holds x |^ n = x proof let X be BCI-algebra; ::_thesis: for x being Element of X for n being Nat st x in BCK-part X & n >= 1 holds x |^ n = x let x be Element of X; ::_thesis: for n being Nat st x in BCK-part X & n >= 1 holds x |^ n = x let n be Nat; ::_thesis: ( x in BCK-part X & n >= 1 implies x |^ n = x ) assume that A1: x in BCK-part X and A2: n >= 1 ; ::_thesis: x |^ n = x defpred S1[ Nat] means x |^ $1 = x; A3: ex y being Element of X st ( y = x & 0. X <= y ) by A1; A4: now__::_thesis:_for_n_being_Nat_st_n_>=_1_&_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume n >= 1 ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then x |^ (n + 1) = x \ (x `) by Th2 .= x \ (0. X) by A3, BCIALG_1:def_11 .= x by BCIALG_1:2 ; hence S1[n + 1] ; ::_thesis: verum end; A5: S1[1] by Th4; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A5, A4); hence x |^ n = x by A2; ::_thesis: verum end; theorem :: BCIALG_6:12 for X being BCI-algebra for x being Element of X for n being Nat st x in BCK-part X holds x |^ (- n) = 0. X proof let X be BCI-algebra; ::_thesis: for x being Element of X for n being Nat st x in BCK-part X holds x |^ (- n) = 0. X let x be Element of X; ::_thesis: for n being Nat st x in BCK-part X holds x |^ (- n) = 0. X let n be Nat; ::_thesis: ( x in BCK-part X implies x |^ (- n) = 0. X ) defpred S1[ Nat] means x |^ (- $1) = 0. X; assume x in BCK-part X ; ::_thesis: x |^ (- n) = 0. X then A1: ex y being Element of X st ( y = x & 0. X <= y ) ; A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[b1 + 1] ) assume A3: S1[n] ; ::_thesis: S1[b1 + 1] - (- (n + 1)) > 0 ; then A4: - (n + 1) < 0 ; percases ( - n = 0 or - n < 0 ) ; suppose - n = 0 ; ::_thesis: S1[b1 + 1] then x |^ (- (n + 1)) = x ` by Th5 .= 0. X by A1, BCIALG_1:def_11 ; hence S1[n + 1] ; ::_thesis: verum end; supposeA5: - n < 0 ; ::_thesis: S1[b1 + 1] then (BCI-power X) . ((x `),(abs (- n))) = 0. X by A3, Def2; then (BCI-power X) . ((x `),(- (- n))) = 0. X by A5, ABSVALUE:def_1; then (x `) \ (((x `) |^ n) `) = (x \ (0. X)) ` by BCIALG_1:9 .= x ` by BCIALG_1:2 ; then (x `) \ (((x `) |^ n) `) = 0. X by A1, BCIALG_1:def_11; then 0. X = (x `) |^ (n + 1) by Th2 .= (BCI-power X) . ((x `),(- (- (n + 1)))) .= (BCI-power X) . ((x `),(abs (- (n + 1)))) by A4, ABSVALUE:def_1 .= x |^ (- (n + 1)) by A4, Def2 ; hence S1[n + 1] ; ::_thesis: verum end; end; end; A6: S1[ 0 ] by Def1; for n being Nat holds S1[n] from NAT_1:sch_2(A6, A2); hence x |^ (- n) = 0. X ; ::_thesis: verum end; theorem Th13: :: BCIALG_6:13 for X being BCI-algebra for a being Element of AtomSet X for i being Integer holds a |^ i in AtomSet X proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for i being Integer holds a |^ i in AtomSet X let a be Element of AtomSet X; ::_thesis: for i being Integer holds a |^ i in AtomSet X let i be Integer; ::_thesis: a |^ i in AtomSet X defpred S1[ Integer] means a |^ $1 in AtomSet X; 0. X in AtomSet X ; then A1: S1[ 0 ] by Def1; percases ( i >= 0 or i <= 0 ) ; supposeA2: i >= 0 ; ::_thesis: a |^ i in AtomSet X A3: for i2 being Integer st i2 >= 0 & S1[i2] holds S1[i2 + 1] proof let i2 be Integer; ::_thesis: ( i2 >= 0 & S1[i2] implies S1[i2 + 1] ) assume i2 >= 0 ; ::_thesis: ( not S1[i2] or S1[i2 + 1] ) then reconsider j = i2 as Element of NAT by INT_1:3; ((a |^ (j + 1)) `) ` = ((a \ ((a |^ j) `)) `) ` by Def1; then ((a |^ (j + 1)) `) ` = ((a `) \ (((a |^ j) `) `)) ` by BCIALG_1:9; then ((a |^ (j + 1)) `) ` = ((a `) `) \ ((((a |^ j) `) `) `) by BCIALG_1:9; then A4: ((a |^ (j + 1)) `) ` = a \ ((((a |^ j) `) `) `) by BCIALG_1:29; assume S1[i2] ; ::_thesis: S1[i2 + 1] then ((a |^ (j + 1)) `) ` = a \ ((a |^ j) `) by A4, BCIALG_1:29; then ((a |^ (j + 1)) `) ` = a |^ (j + 1) by Def1; hence S1[i2 + 1] by BCIALG_1:29; ::_thesis: verum end; for i being Integer st i >= 0 holds S1[i] from INT_1:sch_2(A1, A3); hence a |^ i in AtomSet X by A2; ::_thesis: verum end; supposeA5: i <= 0 ; ::_thesis: a |^ i in AtomSet X A6: for i2 being Integer st i2 <= 0 & S1[i2] holds S1[i2 - 1] proof let i2 be Integer; ::_thesis: ( i2 <= 0 & S1[i2] implies S1[i2 - 1] ) assume A7: i2 <= 0 ; ::_thesis: ( not S1[i2] or S1[i2 - 1] ) assume A8: S1[i2] ; ::_thesis: S1[i2 - 1] percases ( i2 = 0 or i2 < 0 ) by A7; supposeA9: i2 = 0 ; ::_thesis: S1[i2 - 1] ((a `) `) ` = a ` by BCIALG_1:8; then a ` in AtomSet X by BCIALG_1:29; hence S1[i2 - 1] by A9, Th5; ::_thesis: verum end; supposeA10: i2 < 0 ; ::_thesis: S1[i2 - 1] set j = i2; reconsider m = - i2 as Element of NAT by A10, INT_1:3; a |^ (i2 - 1) = (BCI-power X) . ((a `),(abs (i2 - 1))) by A10, Def2; then a |^ (i2 - 1) = (BCI-power X) . ((a `),(- (i2 - 1))) by A10, ABSVALUE:def_1; then a |^ (i2 - 1) = (a `) |^ (m + 1) ; then a |^ (i2 - 1) = (a `) \ (((a `) |^ m) `) by Def1; then a |^ (i2 - 1) = (a `) \ ((a |^ (- (- i2))) `) by Th10; then ((a |^ (i2 - 1)) `) ` = (((a `) `) \ (((a |^ i2) `) `)) ` by BCIALG_1:9; then ((a |^ (i2 - 1)) `) ` = (a \ (((a |^ i2) `) `)) ` by BCIALG_1:29; then ((a |^ (i2 - 1)) `) ` = (a \ (a |^ i2)) ` by A8, BCIALG_1:29; then ((a |^ (i2 - 1)) `) ` = (a `) \ ((a |^ (- m)) `) by BCIALG_1:9; then ((a |^ (i2 - 1)) `) ` = (a `) \ (((a `) |^ m) `) by Th10; then ((a |^ (i2 - 1)) `) ` = (a `) |^ (m + 1) by Def1; then ((a |^ (i2 - 1)) `) ` = (BCI-power X) . ((a `),(- (i2 - 1))) ; then ((a |^ (i2 - 1)) `) ` = (BCI-power X) . ((a `),(abs (i2 - 1))) by A10, ABSVALUE:def_1; then ((a |^ (i2 - 1)) `) ` = a |^ (i2 - 1) by A10, Def2; hence S1[i2 - 1] by BCIALG_1:29; ::_thesis: verum end; end; end; for i being Integer st i <= 0 holds S1[i] from INT_1:sch_3(A1, A6); hence a |^ i in AtomSet X by A5; ::_thesis: verum end; end; end; theorem Th14: :: BCIALG_6:14 for X being BCI-algebra for a being Element of AtomSet X for n being Nat holds (a |^ (n + 1)) ` = ((a |^ n) `) \ a proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for n being Nat holds (a |^ (n + 1)) ` = ((a |^ n) `) \ a let a be Element of AtomSet X; ::_thesis: for n being Nat holds (a |^ (n + 1)) ` = ((a |^ n) `) \ a let n be Nat; ::_thesis: (a |^ (n + 1)) ` = ((a |^ n) `) \ a A1: a |^ n in AtomSet X by Th13; (a |^ (n + 1)) ` = (a \ ((a |^ n) `)) ` by Th2 .= (a `) \ (((a |^ n) `) `) by BCIALG_1:9 .= (a `) \ (a |^ n) by A1, BCIALG_1:29 ; hence (a |^ (n + 1)) ` = ((a |^ n) `) \ a by BCIALG_1:7; ::_thesis: verum end; Lm1: for X being BCI-algebra for a being Element of AtomSet X for n, m being Nat holds a |^ (n + m) = (a |^ m) \ ((a |^ n) `) proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for n, m being Nat holds a |^ (n + m) = (a |^ m) \ ((a |^ n) `) let a be Element of AtomSet X; ::_thesis: for n, m being Nat holds a |^ (n + m) = (a |^ m) \ ((a |^ n) `) let n, m be Nat; ::_thesis: a |^ (n + m) = (a |^ m) \ ((a |^ n) `) reconsider p = a |^ n as Element of AtomSet X by Th13; defpred S1[ Nat] means a |^ (n + $1) = (a |^ $1) \ ((a |^ n) `); A1: now__::_thesis:_for_m_being_Nat_st_S1[m]_holds_ S1[m_+_1] let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) reconsider q = a |^ (m + 1) as Element of AtomSet X by Th13; assume A2: S1[m] ; ::_thesis: S1[m + 1] a |^ (n + (m + 1)) = a |^ ((n + m) + 1) .= a \ (((a |^ m) \ ((a |^ n) `)) `) by A2, Th2 .= a \ (((a |^ m) `) \ (((a |^ n) `) `)) by BCIALG_1:9 .= a \ (((a |^ m) `) \ p) by BCIALG_1:29 .= p \ (((a |^ m) `) \ a) by Th1 .= (a |^ n) \ ((a |^ (m + 1)) `) by Th14 .= q \ (p `) by Th1 .= (a |^ (m + 1)) \ ((a |^ n) `) ; hence S1[m + 1] ; ::_thesis: verum end; (a |^ 0) \ ((a |^ n) `) = ((a |^ n) `) ` by Def1 .= p by BCIALG_1:29 ; then A3: S1[ 0 ] ; for m being Nat holds S1[m] from NAT_1:sch_2(A3, A1); hence a |^ (n + m) = (a |^ m) \ ((a |^ n) `) ; ::_thesis: verum end; Lm2: for X being BCI-algebra for a being Element of AtomSet X for m, n being Nat holds (a |^ m) |^ n = a |^ (m * n) proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for m, n being Nat holds (a |^ m) |^ n = a |^ (m * n) let a be Element of AtomSet X; ::_thesis: for m, n being Nat holds (a |^ m) |^ n = a |^ (m * n) let m, n be Nat; ::_thesis: (a |^ m) |^ n = a |^ (m * n) defpred S1[ Nat] means (a |^ m) |^ $1 = a |^ (m * $1); A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then (a |^ m) |^ (n + 1) = (a |^ m) \ ((a |^ (m * n)) `) by Th2 .= a |^ (m + (m * n)) by Lm1 .= a |^ (m * (n + 1)) ; hence S1[n + 1] ; ::_thesis: verum end; (a |^ m) |^ 0 = 0. X by Def1; then A2: S1[ 0 ] by Def1; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1); hence (a |^ m) |^ n = a |^ (m * n) ; ::_thesis: verum end; theorem Th15: :: BCIALG_6:15 for X being BCI-algebra for a, b being Element of AtomSet X for n being Nat holds (a \ b) |^ n = (a |^ n) \ (b |^ n) proof let X be BCI-algebra; ::_thesis: for a, b being Element of AtomSet X for n being Nat holds (a \ b) |^ n = (a |^ n) \ (b |^ n) let a, b be Element of AtomSet X; ::_thesis: for n being Nat holds (a \ b) |^ n = (a |^ n) \ (b |^ n) let n be Nat; ::_thesis: (a \ b) |^ n = (a |^ n) \ (b |^ n) defpred S1[ Nat] means (a \ b) |^ $1 = (a |^ $1) \ (b |^ $1); A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) A2: (b |^ n) ` in AtomSet X by BCIALG_1:34; A3: a |^ (n + 1) in AtomSet X by Th13; assume S1[n] ; ::_thesis: S1[n + 1] then (a \ b) |^ (n + 1) = (a \ b) \ (((a |^ n) \ (b |^ n)) `) by Th2 .= (a \ (((a |^ n) \ (b |^ n)) `)) \ b by BCIALG_1:7 .= (a \ (((a |^ n) `) \ ((b |^ n) `))) \ b by BCIALG_1:9 .= (((b |^ n) `) \ (((a |^ n) `) \ a)) \ b by A2, Th1 .= (((b |^ n) `) \ b) \ (((a |^ n) `) \ a) by BCIALG_1:7 .= ((b |^ (n + 1)) `) \ (((a |^ n) `) \ a) by Th14 .= ((b |^ (n + 1)) `) \ ((a |^ (n + 1)) `) by Th14 .= ((b |^ (n + 1)) \ (a |^ (n + 1))) ` by BCIALG_1:9 .= (a |^ (n + 1)) \ (b |^ (n + 1)) by A3, BCIALG_1:30 ; hence S1[n + 1] ; ::_thesis: verum end; (a \ b) |^ 0 = 0. X by Def1 .= (0. X) ` by BCIALG_1:def_5 .= (a |^ 0) \ (0. X) by Def1 ; then A4: S1[ 0 ] by Def1; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1); hence (a \ b) |^ n = (a |^ n) \ (b |^ n) ; ::_thesis: verum end; theorem :: BCIALG_6:16 for X being BCI-algebra for a, b being Element of AtomSet X for n being Nat holds (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n)) proof let X be BCI-algebra; ::_thesis: for a, b being Element of AtomSet X for n being Nat holds (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n)) let a, b be Element of AtomSet X; ::_thesis: for n being Nat holds (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n)) let n be Nat; ::_thesis: (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n)) set c = a ` ; set d = b ` ; reconsider c = a ` , d = b ` as Element of AtomSet X by BCIALG_1:34; A1: ( c |^ n = a |^ (- n) & d |^ n = b |^ (- n) ) by Th10; (a \ b) |^ (- n) = ((a \ b) `) |^ n by Th10 .= ((a `) \ (b `)) |^ n by BCIALG_1:9 ; hence (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n)) by A1, Th15; ::_thesis: verum end; theorem Th17: :: BCIALG_6:17 for X being BCI-algebra for a being Element of AtomSet X for n being Nat holds (a `) |^ n = (a |^ n) ` proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for n being Nat holds (a `) |^ n = (a |^ n) ` let a be Element of AtomSet X; ::_thesis: for n being Nat holds (a `) |^ n = (a |^ n) ` let n be Nat; ::_thesis: (a `) |^ n = (a |^ n) ` defpred S1[ Nat] means (a `) |^ $1 = (a |^ $1) ` ; A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] 0. X in AtomSet X ; then (a `) |^ (n + 1) = ((0. X) |^ (n + 1)) \ (a |^ (n + 1)) by Th15 .= (a |^ (n + 1)) ` by Th7 ; hence S1[n + 1] ; ::_thesis: verum end; (a `) |^ 0 = 0. X by Def1 .= (0. X) ` by BCIALG_1:def_5 ; then A2: S1[ 0 ] by Def1; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1); hence (a `) |^ n = (a |^ n) ` ; ::_thesis: verum end; theorem Th18: :: BCIALG_6:18 for X being BCI-algebra for x being Element of X for n being Nat holds (x `) |^ n = (x |^ n) ` proof let X be BCI-algebra; ::_thesis: for x being Element of X for n being Nat holds (x `) |^ n = (x |^ n) ` let x be Element of X; ::_thesis: for n being Nat holds (x `) |^ n = (x |^ n) ` let n be Nat; ::_thesis: (x `) |^ n = (x |^ n) ` defpred S1[ Nat] means (x `) |^ $1 = (x |^ $1) ` ; A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then (x `) |^ (n + 1) = (x `) \ (((x |^ n) `) `) by Th2 .= (x \ ((x |^ n) `)) ` by BCIALG_1:9 .= (x |^ (n + 1)) ` by Th2 ; hence S1[n + 1] ; ::_thesis: verum end; (x `) |^ 0 = 0. X by Def1 .= (0. X) ` by BCIALG_1:def_5 ; then A2: S1[ 0 ] by Def1; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1); hence (x `) |^ n = (x |^ n) ` ; ::_thesis: verum end; theorem :: BCIALG_6:19 for X being BCI-algebra for a being Element of AtomSet X for n being Nat holds (a `) |^ (- n) = (a |^ (- n)) ` proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for n being Nat holds (a `) |^ (- n) = (a |^ (- n)) ` let a be Element of AtomSet X; ::_thesis: for n being Nat holds (a `) |^ (- n) = (a |^ (- n)) ` let n be Nat; ::_thesis: (a `) |^ (- n) = (a |^ (- n)) ` reconsider c = a ` as Element of AtomSet X by BCIALG_1:34; c |^ (- n) = (c `) |^ n by Th10 .= (c |^ n) ` by Th17 .= (a |^ (- n)) ` by Th10 ; hence (a `) |^ (- n) = (a |^ (- n)) ` ; ::_thesis: verum end; theorem Th20: :: BCIALG_6:20 for X being BCI-algebra for x being Element of X for a being Element of AtomSet X for n being Nat st a = ((x `) `) |^ n holds x |^ n in BranchV a proof let X be BCI-algebra; ::_thesis: for x being Element of X for a being Element of AtomSet X for n being Nat st a = ((x `) `) |^ n holds x |^ n in BranchV a let x be Element of X; ::_thesis: for a being Element of AtomSet X for n being Nat st a = ((x `) `) |^ n holds x |^ n in BranchV a let a be Element of AtomSet X; ::_thesis: for n being Nat st a = ((x `) `) |^ n holds x |^ n in BranchV a let n be Nat; ::_thesis: ( a = ((x `) `) |^ n implies x |^ n in BranchV a ) defpred S1[ Nat] means for a being Element of AtomSet X st a = ((x `) `) |^ $1 holds x |^ $1 in BranchV a; A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_for_a_being_Element_of_AtomSet_X_st_a_=_((x_`)_`)_|^_(n_+_1)_&_a_=_((x_`)_`)_|^_(n_+_1)_holds_ x_|^_(n_+_1)_in_BranchV_a set b = ((x `) `) |^ n; let a be Element of AtomSet X; ::_thesis: ( a = ((x `) `) |^ (n + 1) & a = ((x `) `) |^ (n + 1) implies x |^ (n + 1) in BranchV a ) assume a = ((x `) `) |^ (n + 1) ; ::_thesis: ( a = ((x `) `) |^ (n + 1) implies x |^ (n + 1) in BranchV a ) (x `) ` in AtomSet X by BCIALG_1:34; then reconsider b = ((x `) `) |^ n as Element of AtomSet X by Th13; ( 0. X in AtomSet X & x |^ n in BranchV b ) by A2; then (x |^ n) ` = (((x `) `) |^ n) ` by BCIALG_1:37; then A3: x |^ (n + 1) = x \ ((((x `) `) |^ n) `) by Th2; ((((x `) `) \ ((((x `) `) |^ n) `)) \ (x \ ((((x `) `) |^ n) `))) \ (((x `) `) \ x) = 0. X by BCIALG_1:def_3; then ((((x `) `) |^ (n + 1)) \ (x |^ (n + 1))) \ (((x `) `) \ x) = 0. X by A3, Th2; then ((((x `) `) |^ (n + 1)) \ (x |^ (n + 1))) \ (0. X) = 0. X by BCIALG_1:1; then (((x `) `) |^ (n + 1)) \ (x |^ (n + 1)) = 0. X by BCIALG_1:2; then ((x `) `) |^ (n + 1) <= x |^ (n + 1) by BCIALG_1:def_11; hence ( a = ((x `) `) |^ (n + 1) implies x |^ (n + 1) in BranchV a ) ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; x |^ 0 = 0. X by Def1; then (0. X) \ (x |^ 0) = 0. X by BCIALG_1:2; then 0. X <= x |^ 0 by BCIALG_1:def_11; then ((x `) `) |^ 0 <= x |^ 0 by Def1; then A4: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1); hence ( a = ((x `) `) |^ n implies x |^ n in BranchV a ) ; ::_thesis: verum end; theorem Th21: :: BCIALG_6:21 for X being BCI-algebra for x being Element of X for n being Nat holds (x |^ n) ` = (((x `) `) |^ n) ` proof let X be BCI-algebra; ::_thesis: for x being Element of X for n being Nat holds (x |^ n) ` = (((x `) `) |^ n) ` let x be Element of X; ::_thesis: for n being Nat holds (x |^ n) ` = (((x `) `) |^ n) ` let n be Nat; ::_thesis: (x |^ n) ` = (((x `) `) |^ n) ` set b = ((x `) `) |^ n; (x `) ` in AtomSet X by BCIALG_1:34; then reconsider b = ((x `) `) |^ n as Element of AtomSet X by Th13; ( 0. X in AtomSet X & x |^ n in BranchV b ) by Th20; hence (x |^ n) ` = (((x `) `) |^ n) ` by BCIALG_1:37; ::_thesis: verum end; Lm3: for X being BCI-algebra for a being Element of AtomSet X for i, j being Integer st i > 0 & j > 0 holds (a |^ i) \ (a |^ j) = a |^ (i - j) proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for i, j being Integer st i > 0 & j > 0 holds (a |^ i) \ (a |^ j) = a |^ (i - j) let a be Element of AtomSet X; ::_thesis: for i, j being Integer st i > 0 & j > 0 holds (a |^ i) \ (a |^ j) = a |^ (i - j) let i, j be Integer; ::_thesis: ( i > 0 & j > 0 implies (a |^ i) \ (a |^ j) = a |^ (i - j) ) assume that A1: i > 0 and A2: j > 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) percases ( i = j or i > j or i < j ) by XXREAL_0:1; supposeA3: i = j ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) then (a |^ i) \ (a |^ j) = 0. X by BCIALG_1:def_5; then (a |^ i) \ (a |^ j) = a |^ 0 by Def1; hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A3; ::_thesis: verum end; supposeA4: i > j ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) set m = i - j; i - j > 0 by A4, XREAL_1:50; then reconsider j = j, m = i - j as Element of NAT by A2, INT_1:3; a |^ i = a |^ ((i - j) + j) .= (a |^ j) \ ((a |^ m) `) by Lm1 ; then A5: (a |^ i) \ (a |^ j) = ((a |^ j) \ (a |^ j)) \ ((a |^ m) `) by BCIALG_1:7; a |^ m in AtomSet X by Th13; then ((a |^ m) `) ` = a |^ m by BCIALG_1:29; hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A5, BCIALG_1:def_5; ::_thesis: verum end; supposeA6: i < j ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) set m = j - i; j - i > 0 by A6, XREAL_1:50; then reconsider i = i, m = j - i as Element of NAT by A1, INT_1:3; A7: 0. X in AtomSet X ; a |^ j = a |^ (i + (j - i)) .= (a |^ i) \ ((a |^ m) `) by Lm1 ; then (a |^ i) \ (a |^ j) = (a |^ m) ` by A7, BCIALG_1:32; then (a |^ i) \ (a |^ j) = (a `) |^ m by Th17; then (a |^ i) \ (a |^ j) = a |^ (- m) by Th10; hence (a |^ i) \ (a |^ j) = a |^ (i - j) ; ::_thesis: verum end; end; end; theorem Th22: :: BCIALG_6:22 for X being BCI-algebra for a being Element of AtomSet X for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j) proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j) let a be Element of AtomSet X; ::_thesis: for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j) let i, j be Integer; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) percases ( i > 0 or i = 0 or i < 0 ) ; supposeA1: i > 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) percases ( j > 0 or j = 0 or j < 0 ) ; suppose j > 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A1, Lm3; ::_thesis: verum end; supposeA2: j = 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) a |^ (i - 0) = (a |^ i) \ (0. X) by BCIALG_1:2 .= (a |^ i) \ (a |^ 0) by Def1 ; hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A2; ::_thesis: verum end; supposeA3: j < 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) set m = - j; reconsider i = i, m = - j as Element of NAT by A1, A3, INT_1:3; a |^ j = (BCI-power X) . ((a `),(abs j)) by A3, Def2 .= (a `) |^ m by A3, ABSVALUE:def_1 .= (a |^ m) ` by Th17 ; then (a |^ i) \ (a |^ j) = a |^ (i + m) by Lm1; hence (a |^ i) \ (a |^ j) = a |^ (i - j) ; ::_thesis: verum end; end; end; supposeA4: i = 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) percases ( j >= 0 or j < 0 ) ; suppose j >= 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) then reconsider j = j as Element of NAT by INT_1:3; (a |^ 0) \ (a |^ j) = (a |^ j) ` by Def1 .= (a `) |^ j by Th17 .= a |^ (- j) by Th10 ; hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A4; ::_thesis: verum end; supposeA5: j < 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) set m = - j; reconsider m = - j as Element of NAT by A5, INT_1:3; a |^ j = (BCI-power X) . ((a `),(abs j)) by A5, Def2 .= (a `) |^ m by A5, ABSVALUE:def_1 .= (a |^ m) ` by Th17 ; then (a |^ 0) \ (a |^ j) = a |^ (0 + m) by Lm1; hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A4; ::_thesis: verum end; end; end; supposeA6: i < 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) then reconsider m = - i as Element of NAT by INT_1:3; A7: - i > 0 by A6, XREAL_1:58; percases ( j >= 0 or j < 0 ) ; supposeA8: j >= 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) set n = - (i - j); reconsider n = - (i - j), j = j as Element of NAT by A6, A8, INT_1:3; reconsider b = a ` as Element of AtomSet X by BCIALG_1:34; A9: ((a `) |^ j) ` = (b `) |^ j by Th17 .= a |^ j by BCIALG_1:29 ; A10: a |^ i = (BCI-power X) . ((a `),(abs i)) by A6, Def2 .= (a `) |^ m by A6, ABSVALUE:def_1 ; a |^ (i - j) = (BCI-power X) . ((a `),(abs (i - j))) by A6, Def2 .= (a `) |^ n by A6, ABSVALUE:def_1 .= b |^ (j + m) .= ((a `) |^ m) \ (((a `) |^ j) `) by Lm1 ; hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A10, A9; ::_thesis: verum end; supposeA11: j < 0 ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) reconsider b = a ` as Element of AtomSet X by BCIALG_1:34; A12: - j > 0 by A11, XREAL_1:58; reconsider n = - j as Element of NAT by A11, INT_1:3; A13: a |^ j = (BCI-power X) . ((a `),(abs j)) by A11, Def2 .= (a `) |^ n by A11, ABSVALUE:def_1 ; a |^ i = (BCI-power X) . ((a `),(abs i)) by A6, Def2 .= (a `) |^ m by A6, ABSVALUE:def_1 ; then A14: (a |^ i) \ (a |^ j) = b |^ (m - n) by A7, A12, A13, Lm3; percases ( m >= n or m < n ) ; suppose m >= n ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) then reconsider q = m - n as Element of NAT by INT_1:3, XREAL_1:48; (a |^ i) \ (a |^ j) = a |^ (- q) by A14, Th10; hence (a |^ i) \ (a |^ j) = a |^ (i - j) ; ::_thesis: verum end; supposeA15: m < n ; ::_thesis: (a |^ i) \ (a |^ j) = a |^ (i - j) then n - m > 0 by XREAL_1:50; then reconsider p = n - m as Element of NAT by INT_1:3; A16: m - n < 0 by A15, XREAL_1:49; then (a |^ i) \ (a |^ j) = (BCI-power X) . ((b `),(abs (m - n))) by A14, Def2 .= (BCI-power X) . ((b `),(- (m - n))) by A16, ABSVALUE:def_1 .= a |^ p by BCIALG_1:29 ; hence (a |^ i) \ (a |^ j) = a |^ (i - j) ; ::_thesis: verum end; end; end; end; end; end; end; theorem Th23: :: BCIALG_6:23 for X being BCI-algebra for a being Element of AtomSet X for i, j being Integer holds (a |^ i) |^ j = a |^ (i * j) proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for i, j being Integer holds (a |^ i) |^ j = a |^ (i * j) let a be Element of AtomSet X; ::_thesis: for i, j being Integer holds (a |^ i) |^ j = a |^ (i * j) let i, j be Integer; ::_thesis: (a |^ i) |^ j = a |^ (i * j) percases ( i >= 0 or i < 0 ) ; supposeA1: i >= 0 ; ::_thesis: (a |^ i) |^ j = a |^ (i * j) percases ( j >= 0 or j < 0 ) ; suppose j >= 0 ; ::_thesis: (a |^ i) |^ j = a |^ (i * j) then reconsider i = i, j = j as Element of NAT by A1, INT_1:3; (a |^ i) |^ j = a |^ (i * j) by Lm2; hence (a |^ i) |^ j = a |^ (i * j) ; ::_thesis: verum end; supposeA2: j < 0 ; ::_thesis: (a |^ i) |^ j = a |^ (i * j) then reconsider m = - j as Element of NAT by INT_1:3; reconsider i = i as Element of NAT by A1, INT_1:3; percases ( i * j < 0 or i * j = 0 ) by A2; supposeA3: i * j < 0 ; ::_thesis: (a |^ i) |^ j = a |^ (i * j) then reconsider p = - (i * j) as Element of NAT by INT_1:3; reconsider b = a ` as Element of AtomSet X by BCIALG_1:34; reconsider d = a |^ i as Element of AtomSet X by Th13; a |^ (i * j) = (BCI-power X) . ((a `),(abs (i * j))) by A3, Def2 .= (a `) |^ p by A3, ABSVALUE:def_1 .= (a `) |^ (i * (- j)) .= (b |^ i) |^ m by Lm2 .= ((a |^ i) `) |^ m by Th17 .= d |^ (- m) by Th10 .= (a |^ i) |^ (- (- j)) ; hence (a |^ i) |^ j = a |^ (i * j) ; ::_thesis: verum end; supposeA4: i * j = 0 ; ::_thesis: (a |^ i) |^ j = a |^ (i * j) reconsider d = 0. X as Element of AtomSet X by BCIALG_1:23; (a |^ 0) |^ j = (0. X) |^ j by Def1 .= (BCI-power X) . (((0. X) `),(abs j)) by A2, Def2 .= ((0. X) `) |^ m by A2, ABSVALUE:def_1 .= (d |^ m) ` by Th17 .= (0. X) ` by Th7 .= 0. X by BCIALG_1:2 .= a |^ (i * j) by A4, Th3 ; hence (a |^ i) |^ j = a |^ (i * j) by A2, A4, XCMPLX_1:6; ::_thesis: verum end; end; end; end; end; supposeA5: i < 0 ; ::_thesis: (a |^ i) |^ j = a |^ (i * j) then reconsider m = - i as Element of NAT by INT_1:3; percases ( j > 0 or j = 0 or j < 0 ) ; supposeA6: j > 0 ; ::_thesis: (a |^ i) |^ j = a |^ (i * j) then reconsider j = j as Element of NAT by INT_1:3; reconsider b = a ` as Element of AtomSet X by BCIALG_1:34; reconsider p = - (i * j) as Element of NAT by A5, INT_1:3; A7: i * j < 0 * j by A5, A6, XREAL_1:68; then a |^ (i * j) = (BCI-power X) . ((a `),(abs (i * j))) by Def2 .= (a `) |^ p by A7, ABSVALUE:def_1 .= (a `) |^ ((- i) * j) .= (b |^ m) |^ j by Lm2 .= (a |^ (- m)) |^ j by Th10 ; hence (a |^ i) |^ j = a |^ (i * j) ; ::_thesis: verum end; supposeA8: j = 0 ; ::_thesis: (a |^ i) |^ j = a |^ (i * j) reconsider b = a |^ i as Element of AtomSet X by Th13; (a |^ i) |^ j = b |^ 0 by A8 .= 0. X by Def1 .= a |^ (i * 0) by Th3 ; hence (a |^ i) |^ j = a |^ (i * j) by A8; ::_thesis: verum end; suppose j < 0 ; ::_thesis: (a |^ i) |^ j = a |^ (i * j) then reconsider n = - j as Element of NAT by INT_1:3; reconsider d = a |^ m as Element of AtomSet X by Th13; reconsider e = d ` as Element of AtomSet X by BCIALG_1:34; a |^ i = (BCI-power X) . ((a `),(abs i)) by A5, Def2 .= (a `) |^ m by A5, ABSVALUE:def_1 ; then (a |^ i) |^ j = e |^ (- n) by Th17 .= (e `) |^ n by Th10 .= d |^ n by BCIALG_1:29 .= a |^ ((- i) * (- j)) by Lm2 ; hence (a |^ i) |^ j = a |^ (i * j) ; ::_thesis: verum end; end; end; end; end; theorem Th24: :: BCIALG_6:24 for X being BCI-algebra for a being Element of AtomSet X for i, j being Integer holds a |^ (i + j) = (a |^ i) \ ((a |^ j) `) proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for i, j being Integer holds a |^ (i + j) = (a |^ i) \ ((a |^ j) `) let a be Element of AtomSet X; ::_thesis: for i, j being Integer holds a |^ (i + j) = (a |^ i) \ ((a |^ j) `) let i, j be Integer; ::_thesis: a |^ (i + j) = (a |^ i) \ ((a |^ j) `) percases ( j > 0 or j = 0 or j < 0 ) ; suppose j > 0 ; ::_thesis: a |^ (i + j) = (a |^ i) \ ((a |^ j) `) then reconsider j = j as Element of NAT by INT_1:3; (a |^ i) \ ((a |^ j) `) = (a |^ i) \ ((a `) |^ j) by Th17 .= (a |^ i) \ (a |^ (- j)) by Th10 .= a |^ (i - (- j)) by Th22 ; hence a |^ (i + j) = (a |^ i) \ ((a |^ j) `) ; ::_thesis: verum end; supposeA1: j = 0 ; ::_thesis: a |^ (i + j) = (a |^ i) \ ((a |^ j) `) then a |^ (i + j) = (a |^ i) \ (0. X) by BCIALG_1:2 .= (a |^ i) \ ((0. X) `) by BCIALG_1:2 .= (a |^ i) \ ((a |^ j) `) by A1, Th3 ; hence a |^ (i + j) = (a |^ i) \ ((a |^ j) `) ; ::_thesis: verum end; suppose j < 0 ; ::_thesis: a |^ (i + j) = (a |^ i) \ ((a |^ j) `) then reconsider n = - j as Element of NAT by INT_1:3; reconsider b = a ` as Element of AtomSet X by BCIALG_1:34; (a |^ i) \ ((a |^ j) `) = (a |^ i) \ ((a |^ (- (- j))) `) .= (a |^ i) \ (((a `) |^ n) `) by Th10 .= (a |^ i) \ ((b `) |^ n) by Th17 .= (a |^ i) \ (a |^ n) by BCIALG_1:29 .= a |^ (i - n) by Th22 ; hence a |^ (i + j) = (a |^ i) \ ((a |^ j) `) ; ::_thesis: verum end; end; end; definition let X be BCI-algebra; let x be Element of X; attrx is finite-period means :Def4: :: BCIALG_6:def 4 ex n being Element of NAT st ( n <> 0 & x |^ n in BCK-part X ); end; :: deftheorem Def4 defines finite-period BCIALG_6:def_4_:_ for X being BCI-algebra for x being Element of X holds ( x is finite-period iff ex n being Element of NAT st ( n <> 0 & x |^ n in BCK-part X ) ); theorem Th25: :: BCIALG_6:25 for X being BCI-algebra for x being Element of X st x is finite-period holds (x `) ` is finite-period proof let X be BCI-algebra; ::_thesis: for x being Element of X st x is finite-period holds (x `) ` is finite-period let x be Element of X; ::_thesis: ( x is finite-period implies (x `) ` is finite-period ) reconsider b = (x `) ` as Element of AtomSet X by BCIALG_1:34; assume x is finite-period ; ::_thesis: (x `) ` is finite-period then consider p being Element of NAT such that A1: p <> 0 and A2: x |^ p in BCK-part X by Def4; ex y being Element of X st ( y = x |^ p & 0. X <= y ) by A2; then (x |^ p) ` = 0. X by BCIALG_1:def_11; then (b |^ p) ` = 0. X by Th21; then 0. X <= b |^ p by BCIALG_1:def_11; then b |^ p in BCK-part X ; hence (x `) ` is finite-period by A1, Def4; ::_thesis: verum end; definition let X be BCI-algebra; let x be Element of X; assume A1: x is finite-period ; func ord x -> Element of NAT means :Def5: :: BCIALG_6:def 5 ( x |^ it in BCK-part X & it <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds it <= m ) ); existence ex b1 being Element of NAT st ( x |^ b1 in BCK-part X & b1 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds b1 <= m ) ) proof defpred S1[ Nat] means ( x |^ $1 in BCK-part X & $1 <> 0 ); ex n being Element of NAT st ( n <> 0 & x |^ n in BCK-part X ) by A1, Def4; then A1: ex n being Nat st S1[n] ; consider k being Nat such that A2: S1[k] and A3: for n being Nat st S1[n] holds k <= n from NAT_1:sch_5(A1); reconsider k = k as Element of NAT by ORDINAL1:def_12; take k ; ::_thesis: ( x |^ k in BCK-part X & k <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds k <= m ) ) thus ( x |^ k in BCK-part X & k <> 0 ) by A2; ::_thesis: for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds k <= m let m be Element of NAT ; ::_thesis: ( x |^ m in BCK-part X & m <> 0 implies k <= m ) assume ( x |^ m in BCK-part X & m <> 0 ) ; ::_thesis: k <= m hence k <= m by A3; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st x |^ b1 in BCK-part X & b1 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds b1 <= m ) & x |^ b2 in BCK-part X & b2 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds b2 <= m ) holds b1 = b2 proof let n1, n2 be Element of NAT ; ::_thesis: ( x |^ n1 in BCK-part X & n1 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds n1 <= m ) & x |^ n2 in BCK-part X & n2 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds n2 <= m ) implies n1 = n2 ) assume ( x |^ n1 in BCK-part X & n1 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds n1 <= m ) & x |^ n2 in BCK-part X & n2 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds n2 <= m ) ) ; ::_thesis: n1 = n2 then ( n1 <= n2 & n2 <= n1 ) ; hence n1 = n2 by XXREAL_0:1; ::_thesis: verum end; end; :: deftheorem Def5 defines ord BCIALG_6:def_5_:_ for X being BCI-algebra for x being Element of X st x is finite-period holds for b3 being Element of NAT holds ( b3 = ord x iff ( x |^ b3 in BCK-part X & b3 <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds b3 <= m ) ) ); theorem Th26: :: BCIALG_6:26 for X being BCI-algebra for a being Element of AtomSet X for n being Nat st a is finite-period & ord a = n holds a |^ n = 0. X proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for n being Nat st a is finite-period & ord a = n holds a |^ n = 0. X let a be Element of AtomSet X; ::_thesis: for n being Nat st a is finite-period & ord a = n holds a |^ n = 0. X let n be Nat; ::_thesis: ( a is finite-period & ord a = n implies a |^ n = 0. X ) assume ( a is finite-period & ord a = n ) ; ::_thesis: a |^ n = 0. X then a |^ n in BCK-part X by Def5; then ex x being Element of X st ( x = a |^ n & 0. X <= x ) ; then A1: (0. X) \ (a |^ n) = 0. X by BCIALG_1:def_11; a |^ n in AtomSet X by Th13; then ex y being Element of X st ( y = a |^ n & y is atom ) ; hence a |^ n = 0. X by A1, BCIALG_1:def_14; ::_thesis: verum end; theorem :: BCIALG_6:27 for X being BCI-algebra holds ( X is BCK-algebra iff for x being Element of X holds ( x is finite-period & ord x = 1 ) ) proof let X be BCI-algebra; ::_thesis: ( X is BCK-algebra iff for x being Element of X holds ( x is finite-period & ord x = 1 ) ) thus ( X is BCK-algebra implies for x being Element of X holds ( x is finite-period & ord x = 1 ) ) ::_thesis: ( ( for x being Element of X holds ( x is finite-period & ord x = 1 ) ) implies X is BCK-algebra ) proof assume A1: X is BCK-algebra ; ::_thesis: for x being Element of X holds ( x is finite-period & ord x = 1 ) let x be Element of X; ::_thesis: ( x is finite-period & ord x = 1 ) A2: for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds 1 <= m proof let m be Element of NAT ; ::_thesis: ( x |^ m in BCK-part X & m <> 0 implies 1 <= m ) assume that x |^ m in BCK-part X and A3: m <> 0 ; ::_thesis: 1 <= m 0 + 1 <= m by A3, INT_1:7; hence 1 <= m ; ::_thesis: verum end; x ` = 0. X by A1, BCIALG_1:def_8; then 0. X <= x by BCIALG_1:def_11; then x in BCK-part X ; then A4: x |^ 1 in BCK-part X by Th4; then x is finite-period by Def4; hence ( x is finite-period & ord x = 1 ) by A4, A2, Def5; ::_thesis: verum end; assume A5: for x being Element of X holds ( x is finite-period & ord x = 1 ) ; ::_thesis: X is BCK-algebra for y, z being Element of X holds (y \ z) \ y = 0. X proof let y, z be Element of X; ::_thesis: (y \ z) \ y = 0. X ( z is finite-period & ord z = 1 ) by A5; then z |^ 1 in BCK-part X by Def5; then z in BCK-part X by Th4; then A6: ex z1 being Element of X st ( z = z1 & 0. X <= z1 ) ; (y \ z) \ y = (y \ y) \ z by BCIALG_1:7; then (y \ z) \ y = z ` by BCIALG_1:def_5; hence (y \ z) \ y = 0. X by A6, BCIALG_1:def_11; ::_thesis: verum end; then X is being_K by BCIALG_1:def_6; hence X is BCK-algebra by BCIALG_1:18; ::_thesis: verum end; theorem Th28: :: BCIALG_6:28 for X being BCI-algebra for x being Element of X for a being Element of AtomSet X st x is finite-period & a is finite-period & x in BranchV a holds ord x = ord a proof let X be BCI-algebra; ::_thesis: for x being Element of X for a being Element of AtomSet X st x is finite-period & a is finite-period & x in BranchV a holds ord x = ord a let x be Element of X; ::_thesis: for a being Element of AtomSet X st x is finite-period & a is finite-period & x in BranchV a holds ord x = ord a let a be Element of AtomSet X; ::_thesis: ( x is finite-period & a is finite-period & x in BranchV a implies ord x = ord a ) assume that A1: x is finite-period and A2: a is finite-period and A3: x in BranchV a ; ::_thesis: ord x = ord a set na = ord a; ord a <> 0 by A2, Def5; then A4: ord a >= 1 by NAT_1:14; percases ( ord a = 1 or ord a > 1 ) by A4, XXREAL_0:1; supposeA5: ord a = 1 ; ::_thesis: ord x = ord a then a |^ 1 in BCK-part X by A2, Def5; then a in BCK-part X by Th4; then ex aa being Element of X st ( a = aa & 0. X <= aa ) ; then A6: a ` = 0. X by BCIALG_1:def_11; a in AtomSet X ; then ex ab being Element of X st ( a = ab & ab is atom ) ; then a = 0. X by A6, BCIALG_1:def_14; then A7: x |^ 1 in BCK-part X by A3, Th4; for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds 1 <= m by NAT_1:14; hence ord x = ord a by A1, A5, A7, Def5; ::_thesis: verum end; supposeA8: ord a > 1 ; ::_thesis: ord x = ord a 0. X in AtomSet X ; then A9: x ` = a ` by A3, BCIALG_1:37; A10: for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds ord a <= m proof let m be Element of NAT ; ::_thesis: ( x |^ m in BCK-part X & m <> 0 implies ord a <= m ) assume that A11: x |^ m in BCK-part X and A12: m <> 0 ; ::_thesis: ord a <= m ex xx being Element of X st ( x |^ m = xx & 0. X <= xx ) by A11; then (x |^ m) ` = 0. X by BCIALG_1:def_11; then (a `) |^ m = 0. X by A9, Th18; then (a |^ m) ` = 0. X by Th17; then 0. X <= a |^ m by BCIALG_1:def_11; then a |^ m in BCK-part X ; hence ord a <= m by A2, A12, Def5; ::_thesis: verum end; a |^ (ord a) in BCK-part X by A2, Def5; then ex aa being Element of X st ( a |^ (ord a) = aa & 0. X <= aa ) ; then (a |^ (ord a)) ` = 0. X by BCIALG_1:def_11; then (x `) |^ (ord a) = 0. X by A9, Th17; then (x |^ (ord a)) ` = 0. X by Th18; then 0. X <= x |^ (ord a) by BCIALG_1:def_11; then x |^ (ord a) in BCK-part X ; hence ord x = ord a by A1, A8, A10, Def5; ::_thesis: verum end; end; end; theorem Th29: :: BCIALG_6:29 for X being BCI-algebra for x being Element of X for n, m being Nat st x is finite-period & ord x = n holds ( x |^ m in BCK-part X iff n divides m ) proof let X be BCI-algebra; ::_thesis: for x being Element of X for n, m being Nat st x is finite-period & ord x = n holds ( x |^ m in BCK-part X iff n divides m ) let x be Element of X; ::_thesis: for n, m being Nat st x is finite-period & ord x = n holds ( x |^ m in BCK-part X iff n divides m ) let n, m be Nat; ::_thesis: ( x is finite-period & ord x = n implies ( x |^ m in BCK-part X iff n divides m ) ) reconsider b = (x `) ` as Element of AtomSet X by BCIALG_1:34; reconsider bn = b |^ n as Element of AtomSet X by Th13; assume that A1: x is finite-period and A2: ord x = n ; ::_thesis: ( x |^ m in BCK-part X iff n divides m ) A3: b is finite-period by A1, Th25; thus ( x |^ m in BCK-part X implies n divides m ) ::_thesis: ( n divides m implies x |^ m in BCK-part X ) proof defpred S1[ Nat] means ( x |^ $1 in BCK-part X implies n divides $1 ); A4: for m being Nat st ( for k being Nat st k < m holds S1[k] ) holds S1[m] proof let m be Nat; ::_thesis: ( ( for k being Nat st k < m holds S1[k] ) implies S1[m] ) assume A5: for k being Nat st k < m holds S1[k] ; ::_thesis: S1[m] assume A6: x |^ m in BCK-part X ; ::_thesis: n divides m percases ( m = 0 or m <> 0 ) ; suppose m = 0 ; ::_thesis: n divides m hence n divides m by INT_2:12; ::_thesis: verum end; supposeA7: m <> 0 ; ::_thesis: n divides m reconsider mm = m as Element of NAT by ORDINAL1:def_12; x |^ mm in BCK-part X by A6; then n <= m by A1, A2, A7, Def5; then consider k being Nat such that A8: m = n + k by NAT_1:10; reconsider b = (x `) ` as Element of AtomSet X by BCIALG_1:34; A9: b is finite-period by A1, Th25; b \ x = 0. X by BCIALG_1:1; then b <= x by BCIALG_1:def_11; then x in BranchV b ; then n = ord b by A1, A2, A9, Th28; then b |^ n in BCK-part X by A9, Def5; then ex z being Element of X st ( z = b |^ n & 0. X <= z ) ; then A10: (b |^ n) ` = 0. X by BCIALG_1:def_11; ex zz being Element of X st ( zz = x |^ m & 0. X <= zz ) by A6; then (x |^ m) ` = 0. X by BCIALG_1:def_11; then (b |^ (n + k)) ` = 0. X by A8, Th21; then ((b |^ n) \ ((b |^ k) `)) ` = 0. X by Th24; then (((b |^ k) `) `) ` = 0. X by A10, BCIALG_1:9; then (b |^ k) ` = 0. X by BCIALG_1:8; then (x |^ k) ` = 0. X by Th21; then 0. X <= x |^ k by BCIALG_1:def_11; then A11: x |^ k in BCK-part X ; n <> 0 by A1, A2, Def5; then n divides k by A5, A8, A11, NAT_1:16; then consider i being Nat such that A12: k = n * i by NAT_D:def_3; m = n * (1 + i) by A8, A12; hence n divides m by NAT_D:def_3; ::_thesis: verum end; end; end; for m being Nat holds S1[m] from NAT_1:sch_4(A4); hence ( x |^ m in BCK-part X implies n divides m ) ; ::_thesis: verum end; assume n divides m ; ::_thesis: x |^ m in BCK-part X then consider i being Nat such that A13: m = n * i by NAT_D:def_3; b \ x = 0. X by BCIALG_1:1; then b <= x by BCIALG_1:def_11; then x in BranchV b ; then n = ord b by A1, A2, A3, Th28; then b |^ n in BCK-part X by A3, Def5; then ex z being Element of X st ( z = b |^ n & 0. X <= z ) ; then A14: (b |^ n) ` = 0. X by BCIALG_1:def_11; (b |^ m) ` = (bn |^ i) ` by A13, Th23; then (b |^ m) ` = (0. X) |^ i by A14, Th17; then (b |^ m) ` = 0. X by Th7; then (x |^ m) ` = 0. X by Th21; then 0. X <= x |^ m by BCIALG_1:def_11; hence x |^ m in BCK-part X ; ::_thesis: verum end; theorem :: BCIALG_6:30 for X being BCI-algebra for x being Element of X for m, n being Nat st x is finite-period & x |^ m is finite-period & ord x = n & m > 0 holds ord (x |^ m) = n div (m gcd n) proof let X be BCI-algebra; ::_thesis: for x being Element of X for m, n being Nat st x is finite-period & x |^ m is finite-period & ord x = n & m > 0 holds ord (x |^ m) = n div (m gcd n) let x be Element of X; ::_thesis: for m, n being Nat st x is finite-period & x |^ m is finite-period & ord x = n & m > 0 holds ord (x |^ m) = n div (m gcd n) let m, n be Nat; ::_thesis: ( x is finite-period & x |^ m is finite-period & ord x = n & m > 0 implies ord (x |^ m) = n div (m gcd n) ) assume that A1: x is finite-period and A2: x |^ m is finite-period and A3: ord x = n and A4: m > 0 ; ::_thesis: ord (x |^ m) = n div (m gcd n) reconsider b = (x `) ` as Element of AtomSet X by BCIALG_1:34; A5: b is finite-period by A1, Th25; b \ x = 0. X by BCIALG_1:1; then b <= x by BCIALG_1:def_11; then x in BranchV b ; then A6: n = ord b by A1, A3, A5, Th28; then b |^ n in BCK-part X by A5, Def5; then A7: ex z being Element of X st ( z = b |^ n & 0. X <= z ) ; reconsider mgn = m gcd n as Element of NAT ; m gcd n divides n by INT_2:21; then consider vn being Nat such that A8: n = mgn * vn by NAT_D:def_3; reconsider vn = vn as Element of NAT by ORDINAL1:def_12; m gcd n divides m by INT_2:21; then consider i being Nat such that A9: m = mgn * i by NAT_D:def_3; reconsider i = i as Element of NAT by ORDINAL1:def_12; A10: n = (mgn * vn) + 0 by A8; A11: vn,i are_relative_prime proof i gcd vn divides i by NAT_D:def_5; then consider b2 being Nat such that A12: i = (i gcd vn) * b2 by NAT_D:def_3; m = ((m gcd n) * (i gcd vn)) * b2 by A9, A12; then A13: (m gcd n) * (i gcd vn) divides m by NAT_D:def_3; i gcd vn divides vn by NAT_D:def_5; then consider b1 being Nat such that A14: vn = (i gcd vn) * b1 by NAT_D:def_3; n = ((m gcd n) * (i gcd vn)) * b1 by A8, A14; then (m gcd n) * (i gcd vn) divides n by NAT_D:def_3; then (m gcd n) * (i gcd vn) divides m gcd n by A13, NAT_D:def_5; then consider c being Nat such that A15: m gcd n = ((m gcd n) * (i gcd vn)) * c by NAT_D:def_3; A16: m gcd n <> 0 by A4, INT_2:5; (m gcd n) * 1 = (m gcd n) * ((i gcd vn) * c) by A15; then 1 = i gcd vn by A16, NAT_1:15, XCMPLX_1:5; hence vn,i are_relative_prime by INT_2:def_3; ::_thesis: verum end; A17: for mm being Element of NAT st (x |^ m) |^ mm in BCK-part X & mm <> 0 holds vn <= mm proof let mm be Element of NAT ; ::_thesis: ( (x |^ m) |^ mm in BCK-part X & mm <> 0 implies vn <= mm ) assume that A18: (x |^ m) |^ mm in BCK-part X and A19: mm <> 0 ; ::_thesis: vn <= mm ex z being Element of X st ( z = (x |^ m) |^ mm & 0. X <= z ) by A18; then ((x |^ m) |^ mm) ` = 0. X by BCIALG_1:def_11; then ((x |^ m) `) |^ mm = 0. X by Th18; then ((b |^ m) `) |^ mm = 0. X by Th21; then ((b |^ m) |^ mm) ` = 0. X by Th18; then (b |^ (m * mm)) ` = 0. X by Th23; then 0. X <= b |^ (m * mm) by BCIALG_1:def_11; then b |^ (m * mm) in BCK-part X ; then mgn * vn divides (mgn * i) * mm by A8, A9, A5, A6, Th29; then consider c being Nat such that A20: (mgn * i) * mm = (mgn * vn) * c by NAT_D:def_3; A21: mgn <> 0 by A4, INT_2:5; mgn * (i * mm) = mgn * (vn * c) by A20; then i * mm = vn * c by A21, XCMPLX_1:5; then vn divides i * mm by NAT_D:def_3; then vn divides mm by A11, INT_2:25; then consider cc being Nat such that A22: mm = vn * cc by NAT_D:def_3; cc <> 0 by A19, A22; hence vn <= mm by A22, NAT_1:24; ::_thesis: verum end; ((x |^ m) |^ vn) ` = ((x |^ m) `) |^ vn by Th18 .= ((b |^ m) `) |^ vn by Th21 .= ((b |^ m) |^ vn) ` by Th18 .= (b |^ ((mgn * i) * vn)) ` by A9, Th23 .= (b |^ (n * i)) ` by A8 .= ((b |^ n) |^ i) ` by Th23 .= ((b |^ n) `) |^ i by Th18 .= (0. X) |^ i by A7, BCIALG_1:def_11 .= 0. X by Th7 ; then 0. X <= (x |^ m) |^ vn by BCIALG_1:def_11; then A23: (x |^ m) |^ vn in BCK-part X ; n gcd m > 0 by A4, NEWTON:58; then A24: n div mgn = vn by A10, NAT_D:def_1; vn <> 0 by A1, A3, A8, Def5; hence ord (x |^ m) = n div (m gcd n) by A2, A24, A23, A17, Def5; ::_thesis: verum end; theorem :: BCIALG_6:31 for X being BCI-algebra for x being Element of X st x is finite-period & x ` is finite-period holds ord x = ord (x `) proof let X be BCI-algebra; ::_thesis: for x being Element of X st x is finite-period & x ` is finite-period holds ord x = ord (x `) let x be Element of X; ::_thesis: ( x is finite-period & x ` is finite-period implies ord x = ord (x `) ) assume that A1: x is finite-period and A2: x ` is finite-period ; ::_thesis: ord x = ord (x `) set m = ord (x `); (x `) |^ (ord (x `)) in BCK-part X by A2, Def5; then ex zz being Element of X st ( zz = (x `) |^ (ord (x `)) & 0. X <= zz ) ; then ((x `) |^ (ord (x `))) ` = 0. X by BCIALG_1:def_11; then ((x `) `) |^ (ord (x `)) = 0. X by Th18; then (((x `) `) |^ (ord (x `))) ` = 0. X by BCIALG_1:def_5; then (x |^ (ord (x `))) ` = 0. X by Th21; then 0. X <= x |^ (ord (x `)) by BCIALG_1:def_11; then A3: x |^ (ord (x `)) in BCK-part X ; set n = ord x; ord (x `) <> 0 by A2, Def5; then A4: ord x <= ord (x `) by A1, A3, Def5; x |^ (ord x) in BCK-part X by A1, Def5; then ex zz being Element of X st ( zz = x |^ (ord x) & 0. X <= zz ) ; then (x |^ (ord x)) ` = 0. X by BCIALG_1:def_11; then (x `) |^ (ord x) = 0. X by Th18; then ((x `) |^ (ord x)) ` = 0. X by BCIALG_1:def_5; then 0. X <= (x `) |^ (ord x) by BCIALG_1:def_11; then A5: (x `) |^ (ord x) in BCK-part X ; ord x <> 0 by A1, Def5; then ord (x `) <= ord x by A2, A5, Def5; hence ord x = ord (x `) by A4, XXREAL_0:1; ::_thesis: verum end; theorem :: BCIALG_6:32 for X being BCI-algebra for x, y being Element of X for a being Element of AtomSet X st x \ y is finite-period & x in BranchV a & y in BranchV a holds ord (x \ y) = 1 proof let X be BCI-algebra; ::_thesis: for x, y being Element of X for a being Element of AtomSet X st x \ y is finite-period & x in BranchV a & y in BranchV a holds ord (x \ y) = 1 let x, y be Element of X; ::_thesis: for a being Element of AtomSet X st x \ y is finite-period & x in BranchV a & y in BranchV a holds ord (x \ y) = 1 let a be Element of AtomSet X; ::_thesis: ( x \ y is finite-period & x in BranchV a & y in BranchV a implies ord (x \ y) = 1 ) assume that A1: x \ y is finite-period and A2: ( x in BranchV a & y in BranchV a ) ; ::_thesis: ord (x \ y) = 1 A3: for m being Element of NAT st (x \ y) |^ m in BCK-part X & m <> 0 holds 1 <= m by NAT_1:14; x \ y in BCK-part X by A2, BCIALG_1:40; then (x \ y) |^ 1 in BCK-part X by Th4; hence ord (x \ y) = 1 by A1, A3, Def5; ::_thesis: verum end; theorem :: BCIALG_6:33 for X being BCI-algebra for x, y being Element of X for a, b being Element of AtomSet X st a \ b is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & x in BranchV a & y in BranchV b holds ord (a \ b) divides (ord x) lcm (ord y) proof let X be BCI-algebra; ::_thesis: for x, y being Element of X for a, b being Element of AtomSet X st a \ b is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & x in BranchV a & y in BranchV b holds ord (a \ b) divides (ord x) lcm (ord y) let x, y be Element of X; ::_thesis: for a, b being Element of AtomSet X st a \ b is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & x in BranchV a & y in BranchV b holds ord (a \ b) divides (ord x) lcm (ord y) let a, b be Element of AtomSet X; ::_thesis: ( a \ b is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & x in BranchV a & y in BranchV b implies ord (a \ b) divides (ord x) lcm (ord y) ) assume that A1: a \ b is finite-period and A2: x is finite-period and A3: y is finite-period and A4: a is finite-period and A5: b is finite-period and A6: x in BranchV a and A7: y in BranchV b ; ::_thesis: ord (a \ b) divides (ord x) lcm (ord y) ord y divides (ord x) lcm (ord y) by NAT_D:def_4; then consider yx being Nat such that A8: (ord x) lcm (ord y) = (ord y) * yx by NAT_D:def_3; reconsider na = ord a as Element of NAT ; reconsider xly = (ord x) lcm (ord y) as Element of NAT ; ord x divides (ord x) lcm (ord y) by NAT_D:def_4; then consider xy being Nat such that A9: (ord x) lcm (ord y) = (ord x) * xy by NAT_D:def_3; (a \ b) |^ xly = (a |^ ((ord x) * xy)) \ (b |^ ((ord y) * yx)) by A9, A8, Th15 .= ((a |^ (ord x)) |^ xy) \ (b |^ ((ord y) * yx)) by Th23 .= ((a |^ (ord x)) |^ xy) \ ((b |^ (ord y)) |^ yx) by Th23 .= ((a |^ na) |^ xy) \ ((b |^ (ord y)) |^ yx) by A2, A4, A6, Th28 .= ((0. X) |^ xy) \ ((b |^ (ord y)) |^ yx) by A4, Th26 .= ((0. X) |^ xy) \ ((b |^ (ord b)) |^ yx) by A3, A5, A7, Th28 .= ((0. X) |^ xy) \ ((0. X) |^ yx) by A5, Th26 .= ((0. X) |^ yx) ` by Th7 .= (0. X) ` by Th7 .= 0. X by BCIALG_1:def_5 ; then ((a \ b) |^ xly) ` = 0. X by BCIALG_1:def_5; then 0. X <= (a \ b) |^ xly by BCIALG_1:def_11; then (a \ b) |^ xly in BCK-part X ; hence ord (a \ b) divides (ord x) lcm (ord y) by A1, Th29; ::_thesis: verum end; begin theorem Th34: :: BCIALG_6:34 for X being BCI-algebra for Y being SubAlgebra of X for x, y being Element of X for x9, y9 being Element of Y st x = x9 & y = y9 holds x \ y = x9 \ y9 proof let X be BCI-algebra; ::_thesis: for Y being SubAlgebra of X for x, y being Element of X for x9, y9 being Element of Y st x = x9 & y = y9 holds x \ y = x9 \ y9 let Y be SubAlgebra of X; ::_thesis: for x, y being Element of X for x9, y9 being Element of Y st x = x9 & y = y9 holds x \ y = x9 \ y9 let x, y be Element of X; ::_thesis: for x9, y9 being Element of Y st x = x9 & y = y9 holds x \ y = x9 \ y9 let x9, y9 be Element of Y; ::_thesis: ( x = x9 & y = y9 implies x \ y = x9 \ y9 ) assume A1: ( x = x9 & y = y9 ) ; ::_thesis: x \ y = x9 \ y9 A2: [x9,y9] in [: the carrier of Y, the carrier of Y:] by ZFMISC_1:87; x9 \ y9 = ( the InternalDiff of X || the carrier of Y) . (x9,y9) by BCIALG_1:def_10 .= x \ y by A1, A2, FUNCT_1:49 ; hence x \ y = x9 \ y9 ; ::_thesis: verum end; definition let X, X9 be non empty BCIStr_0 ; let f be Function of X,X9; attrf is multiplicative means :Def6: :: BCIALG_6:def 6 for a, b being Element of X holds f . (a \ b) = (f . a) \ (f . b); end; :: deftheorem Def6 defines multiplicative BCIALG_6:def_6_:_ for X, X9 being non empty BCIStr_0 for f being Function of X,X9 holds ( f is multiplicative iff for a, b being Element of X holds f . (a \ b) = (f . a) \ (f . b) ); registration let X, X9 be BCI-algebra; cluster Relation-like the carrier of X -defined the carrier of X9 -valued Function-like non empty V14( the carrier of X) quasi_total multiplicative for Element of bool [: the carrier of X, the carrier of X9:]; existence ex b1 being Function of X,X9 st b1 is multiplicative proof reconsider f = the carrier of X --> (0. X9) as Function of X,X9 ; take f ; ::_thesis: f is multiplicative for x, y being Element of X holds f . (x \ y) = (f . x) \ (f . y) proof let x, y be Element of X; ::_thesis: f . (x \ y) = (f . x) \ (f . y) f . (x \ y) = 0. X9 by FUNCOP_1:7 .= (0. X9) ` by BCIALG_1:2 .= (f . x) \ (0. X9) by FUNCOP_1:7 ; hence f . (x \ y) = (f . x) \ (f . y) by FUNCOP_1:7; ::_thesis: verum end; hence f is multiplicative by Def6; ::_thesis: verum end; end; definition let X, X9 be BCI-algebra; mode BCI-homomorphism of X,X9 is multiplicative Function of X,X9; end; definition let X, X9 be BCI-algebra; let f be BCI-homomorphism of X,X9; attrf is isotonic means :: BCIALG_6:def 7 for x, y being Element of X st x <= y holds f . x <= f . y; end; :: deftheorem defines isotonic BCIALG_6:def_7_:_ for X, X9 being BCI-algebra for f being BCI-homomorphism of X,X9 holds ( f is isotonic iff for x, y being Element of X st x <= y holds f . x <= f . y ); definition let X be BCI-algebra; mode Endomorphism of X is BCI-homomorphism of X,X; end; definition let X, X9 be BCI-algebra; let f be BCI-homomorphism of X,X9; func Ker f -> set equals :: BCIALG_6:def 8 { x where x is Element of X : f . x = 0. X9 } ; coherence { x where x is Element of X : f . x = 0. X9 } is set ; end; :: deftheorem defines Ker BCIALG_6:def_8_:_ for X, X9 being BCI-algebra for f being BCI-homomorphism of X,X9 holds Ker f = { x where x is Element of X : f . x = 0. X9 } ; theorem Th35: :: BCIALG_6:35 for X, X9 being BCI-algebra for f being BCI-homomorphism of X,X9 holds f . (0. X) = 0. X9 proof let X, X9 be BCI-algebra; ::_thesis: for f being BCI-homomorphism of X,X9 holds f . (0. X) = 0. X9 let f be BCI-homomorphism of X,X9; ::_thesis: f . (0. X) = 0. X9 f . (0. X) = f . ((0. X) `) by BCIALG_1:2 .= (f . (0. X)) \ (f . (0. X)) by Def6 ; hence f . (0. X) = 0. X9 by BCIALG_1:def_5; ::_thesis: verum end; registration let X, X9 be BCI-algebra; let f be BCI-homomorphism of X,X9; cluster Ker f -> non empty ; coherence not Ker f is empty proof f . (0. X) = 0. X9 by Th35; then 0. X in Ker f ; hence not Ker f is empty ; ::_thesis: verum end; end; theorem :: BCIALG_6:36 for X, X9 being BCI-algebra for x, y being Element of X for f being BCI-homomorphism of X,X9 st x <= y holds f . x <= f . y proof let X, X9 be BCI-algebra; ::_thesis: for x, y being Element of X for f being BCI-homomorphism of X,X9 st x <= y holds f . x <= f . y let x, y be Element of X; ::_thesis: for f being BCI-homomorphism of X,X9 st x <= y holds f . x <= f . y let f be BCI-homomorphism of X,X9; ::_thesis: ( x <= y implies f . x <= f . y ) assume A1: x <= y ; ::_thesis: f . x <= f . y (f . x) \ (f . y) = f . (x \ y) by Def6 .= f . (0. X) by A1, BCIALG_1:def_11 .= 0. X9 by Th35 ; hence f . x <= f . y by BCIALG_1:def_11; ::_thesis: verum end; theorem :: BCIALG_6:37 for X9, X being BCI-algebra for f being BCI-homomorphism of X,X9 holds ( f is one-to-one iff Ker f = {(0. X)} ) proof let X9, X be BCI-algebra; ::_thesis: for f being BCI-homomorphism of X,X9 holds ( f is one-to-one iff Ker f = {(0. X)} ) let f be BCI-homomorphism of X,X9; ::_thesis: ( f is one-to-one iff Ker f = {(0. X)} ) thus ( f is one-to-one implies Ker f = {(0. X)} ) ::_thesis: ( Ker f = {(0. X)} implies f is one-to-one ) proof assume A1: f is one-to-one ; ::_thesis: Ker f = {(0. X)} thus Ker f c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= Ker f proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Ker f or a in {(0. X)} ) assume a in Ker f ; ::_thesis: a in {(0. X)} then A2: ex x being Element of X st ( a = x & f . x = 0. X9 ) ; then reconsider a = a as Element of X ; f . a = f . (0. X) by A2, Th35; then a = 0. X by A1, FUNCT_2:19; hence a in {(0. X)} by TARSKI:def_1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(0. X)} or a in Ker f ) assume A3: a in {(0. X)} ; ::_thesis: a in Ker f then reconsider a = a as Element of X by TARSKI:def_1; a = 0. X by A3, TARSKI:def_1; then f . a = 0. X9 by Th35; hence a in Ker f ; ::_thesis: verum end; assume A4: Ker f = {(0. X)} ; ::_thesis: f is one-to-one now__::_thesis:_for_a,_b_being_Element_of_X_st_a_<>_b_holds_ not_f_._a_=_f_._b let a, b be Element of X; ::_thesis: ( a <> b implies not f . a = f . b ) assume that A5: a <> b and A6: f . a = f . b ; ::_thesis: contradiction (f . b) \ (f . a) = 0. X9 by A6, BCIALG_1:def_5; then f . (b \ a) = 0. X9 by Def6; then b \ a in Ker f ; then A7: b \ a = 0. X by A4, TARSKI:def_1; (f . a) \ (f . b) = 0. X9 by A6, BCIALG_1:def_5; then f . (a \ b) = 0. X9 by Def6; then a \ b in Ker f ; then a \ b = 0. X by A4, TARSKI:def_1; hence contradiction by A5, A7, BCIALG_1:def_7; ::_thesis: verum end; then for a, b being Element of X st f . a = f . b holds a = b ; hence f is one-to-one by GROUP_6:1; ::_thesis: verum end; theorem :: BCIALG_6:38 for X9, X being BCI-algebra for f being BCI-homomorphism of X,X9 for g being BCI-homomorphism of X9,X st f is bijective & g = f " holds g is bijective proof let X9, X be BCI-algebra; ::_thesis: for f being BCI-homomorphism of X,X9 for g being BCI-homomorphism of X9,X st f is bijective & g = f " holds g is bijective let f be BCI-homomorphism of X,X9; ::_thesis: for g being BCI-homomorphism of X9,X st f is bijective & g = f " holds g is bijective let g be BCI-homomorphism of X9,X; ::_thesis: ( f is bijective & g = f " implies g is bijective ) assume A1: ( f is bijective & g = f " ) ; ::_thesis: g is bijective dom f = the carrier of X by FUNCT_2:def_1; then rng g = the carrier of X by A1, FUNCT_1:33; then A2: g is onto by FUNCT_2:def_3; g is one-to-one by A1, FUNCT_1:40; hence g is bijective by A2; ::_thesis: verum end; theorem :: BCIALG_6:39 for X9, X, Y being BCI-algebra for f being BCI-homomorphism of X,X9 for h being BCI-homomorphism of X9,Y holds h * f is BCI-homomorphism of X,Y proof let X9, X, Y be BCI-algebra; ::_thesis: for f being BCI-homomorphism of X,X9 for h being BCI-homomorphism of X9,Y holds h * f is BCI-homomorphism of X,Y let f be BCI-homomorphism of X,X9; ::_thesis: for h being BCI-homomorphism of X9,Y holds h * f is BCI-homomorphism of X,Y let h be BCI-homomorphism of X9,Y; ::_thesis: h * f is BCI-homomorphism of X,Y reconsider g = h * f as Function of X,Y ; now__::_thesis:_for_a,_b_being_Element_of_X_holds_g_._(a_\_b)_=_(g_._a)_\_(g_._b) let a, b be Element of X; ::_thesis: g . (a \ b) = (g . a) \ (g . b) thus g . (a \ b) = h . (f . (a \ b)) by FUNCT_2:15 .= h . ((f . a) \ (f . b)) by Def6 .= (h . (f . a)) \ (h . (f . b)) by Def6 .= (g . a) \ (h . (f . b)) by FUNCT_2:15 .= (g . a) \ (g . b) by FUNCT_2:15 ; ::_thesis: verum end; hence h * f is BCI-homomorphism of X,Y by Def6; ::_thesis: verum end; theorem :: BCIALG_6:40 for X9, X being BCI-algebra for f being BCI-homomorphism of X,X9 for Z being SubAlgebra of X9 st the carrier of Z = rng f holds f is BCI-homomorphism of X,Z proof let X9, X be BCI-algebra; ::_thesis: for f being BCI-homomorphism of X,X9 for Z being SubAlgebra of X9 st the carrier of Z = rng f holds f is BCI-homomorphism of X,Z let f be BCI-homomorphism of X,X9; ::_thesis: for Z being SubAlgebra of X9 st the carrier of Z = rng f holds f is BCI-homomorphism of X,Z let Z be SubAlgebra of X9; ::_thesis: ( the carrier of Z = rng f implies f is BCI-homomorphism of X,Z ) A1: dom f = the carrier of X by FUNCT_2:def_1; assume the carrier of Z = rng f ; ::_thesis: f is BCI-homomorphism of X,Z then reconsider f9 = f as Function of X,Z by A1, RELSET_1:4; now__::_thesis:_for_a,_b_being_Element_of_X_holds_(f9_._a)_\_(f9_._b)_=_f9_._(a_\_b) let a, b be Element of X; ::_thesis: (f9 . a) \ (f9 . b) = f9 . (a \ b) thus (f9 . a) \ (f9 . b) = (f . a) \ (f . b) by Th34 .= f9 . (a \ b) by Def6 ; ::_thesis: verum end; hence f is BCI-homomorphism of X,Z by Def6; ::_thesis: verum end; theorem Th41: :: BCIALG_6:41 for X9, X being BCI-algebra for f being BCI-homomorphism of X,X9 holds Ker f is closed Ideal of X proof let X9, X be BCI-algebra; ::_thesis: for f being BCI-homomorphism of X,X9 holds Ker f is closed Ideal of X let f be BCI-homomorphism of X,X9; ::_thesis: Ker f is closed Ideal of X now__::_thesis:_for_x_being_set_st_x_in_Ker_f_holds_ x_in_the_carrier_of_X let x be set ; ::_thesis: ( x in Ker f implies x in the carrier of X ) assume x in Ker f ; ::_thesis: x in the carrier of X then ex x9 being Element of X st ( x = x9 & f . x9 = 0. X9 ) ; hence x in the carrier of X ; ::_thesis: verum end; then A1: Ker f is non empty Subset of X by TARSKI:def_3; A2: now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_in_Ker_f_&_y_in_Ker_f_holds_ x_in_Ker_f let x, y be Element of X; ::_thesis: ( x \ y in Ker f & y in Ker f implies x in Ker f ) assume ( x \ y in Ker f & y in Ker f ) ; ::_thesis: x in Ker f then ( ex y9 being Element of X st ( y = y9 & f . y9 = 0. X9 ) & ex x9 being Element of X st ( x \ y = x9 & f . x9 = 0. X9 ) ) ; then (f . x) \ (0. X9) = 0. X9 by Def6; then f . x = 0. X9 by BCIALG_1:2; hence x in Ker f ; ::_thesis: verum end; f . (0. X) = 0. X9 by Th35; then 0. X in Ker f ; then reconsider Kf = Ker f as Ideal of X by A1, A2, BCIALG_1:def_18; Kf is closed proof let x be Element of Kf; :: according to BCIALG_1:def_19 ::_thesis: x ` in Kf x in Kf ; then A3: ex x9 being Element of X st ( x = x9 & f . x9 = 0. X9 ) ; f . (x `) = (f . (0. X)) \ (f . x) by Def6; then f . (x `) = (0. X9) ` by A3, Th35; then f . (x `) = 0. X9 by BCIALG_1:def_5; hence x ` in Kf ; ::_thesis: verum end; hence Ker f is closed Ideal of X ; ::_thesis: verum end; registration let X, X9 be BCI-algebra; let f be BCI-homomorphism of X,X9; cluster Ker f -> closed for Ideal of X; coherence for b1 being Ideal of X st b1 = Ker f holds b1 is closed by Th41; end; theorem Th42: :: BCIALG_6:42 for X9, X being BCI-algebra for f being BCI-homomorphism of X,X9 st f is onto holds for c being Element of X9 ex x being Element of X st c = f . x proof let X9, X be BCI-algebra; ::_thesis: for f being BCI-homomorphism of X,X9 st f is onto holds for c being Element of X9 ex x being Element of X st c = f . x let f be BCI-homomorphism of X,X9; ::_thesis: ( f is onto implies for c being Element of X9 ex x being Element of X st c = f . x ) A1: for c being set holds ( c in rng f iff ex x being Element of X st c = f . x ) proof let c be set ; ::_thesis: ( c in rng f iff ex x being Element of X st c = f . x ) thus ( c in rng f implies ex x being Element of X st c = f . x ) ::_thesis: ( ex x being Element of X st c = f . x implies c in rng f ) proof assume c in rng f ; ::_thesis: ex x being Element of X st c = f . x then consider y being set such that A2: y in dom f and A3: f . y = c by FUNCT_1:def_3; reconsider y = y as Element of X by A2; take y ; ::_thesis: c = f . y thus c = f . y by A3; ::_thesis: verum end; given x being Element of X such that A4: c = f . x ; ::_thesis: c in rng f the carrier of X = dom f by FUNCT_2:def_1; hence c in rng f by A4, FUNCT_1:def_3; ::_thesis: verum end; assume f is onto ; ::_thesis: for c being Element of X9 ex x being Element of X st c = f . x then rng f = the carrier of X9 by FUNCT_2:def_3; hence for c being Element of X9 ex x being Element of X st c = f . x by A1; ::_thesis: verum end; theorem :: BCIALG_6:43 for X9, X being BCI-algebra for f being BCI-homomorphism of X,X9 for a being Element of X st a is minimal holds f . a is minimal proof let X9, X be BCI-algebra; ::_thesis: for f being BCI-homomorphism of X,X9 for a being Element of X st a is minimal holds f . a is minimal let f be BCI-homomorphism of X,X9; ::_thesis: for a being Element of X st a is minimal holds f . a is minimal let a be Element of X; ::_thesis: ( a is minimal implies f . a is minimal ) assume a is minimal ; ::_thesis: f . a is minimal then f . a = f . ((a `) `) by BCIALG_2:29; then f . a = (f . (0. X)) \ (f . ((0. X) \ a)) by Def6; then f . a = (f . (0. X)) \ ((f . (0. X)) \ (f . a)) by Def6; then f . a = ((f . (0. X)) \ (f . a)) ` by Th35; then f . a = ((f . a) `) ` by Th35; hence f . a is minimal by BCIALG_2:29; ::_thesis: verum end; theorem :: BCIALG_6:44 for X, X9 being BCI-algebra for f being BCI-homomorphism of X,X9 for a being Element of AtomSet X for b being Element of AtomSet X9 st b = f . a holds f .: (BranchV a) c= BranchV b proof let X, X9 be BCI-algebra; ::_thesis: for f being BCI-homomorphism of X,X9 for a being Element of AtomSet X for b being Element of AtomSet X9 st b = f . a holds f .: (BranchV a) c= BranchV b let f be BCI-homomorphism of X,X9; ::_thesis: for a being Element of AtomSet X for b being Element of AtomSet X9 st b = f . a holds f .: (BranchV a) c= BranchV b let a be Element of AtomSet X; ::_thesis: for b being Element of AtomSet X9 st b = f . a holds f .: (BranchV a) c= BranchV b let b be Element of AtomSet X9; ::_thesis: ( b = f . a implies f .: (BranchV a) c= BranchV b ) assume A1: b = f . a ; ::_thesis: f .: (BranchV a) c= BranchV b let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (BranchV a) or y in BranchV b ) assume y in f .: (BranchV a) ; ::_thesis: y in BranchV b then consider x being set such that x in dom f and A2: x in BranchV a and A3: y = f . x by FUNCT_1:def_6; A4: ex x1 being Element of X st ( x = x1 & a <= x1 ) by A2; reconsider x = x as Element of X by A2; (f . a) \ (f . x) = f . (a \ x) by Def6; then (f . a) \ (f . x) = f . (0. X) by A4, BCIALG_1:def_11; then (f . a) \ (f . x) = 0. X9 by Th35; then b <= f . x by A1, BCIALG_1:def_11; hence y in BranchV b by A3; ::_thesis: verum end; theorem Th45: :: BCIALG_6:45 for X9, X being BCI-algebra for A9 being non empty Subset of X9 for f being BCI-homomorphism of X,X9 st A9 is Ideal of X9 holds f " A9 is Ideal of X proof let X9, X be BCI-algebra; ::_thesis: for A9 being non empty Subset of X9 for f being BCI-homomorphism of X,X9 st A9 is Ideal of X9 holds f " A9 is Ideal of X let A9 be non empty Subset of X9; ::_thesis: for f being BCI-homomorphism of X,X9 st A9 is Ideal of X9 holds f " A9 is Ideal of X let f be BCI-homomorphism of X,X9; ::_thesis: ( A9 is Ideal of X9 implies f " A9 is Ideal of X ) assume A1: A9 is Ideal of X9 ; ::_thesis: f " A9 is Ideal of X A2: now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_in_f_"_A9_&_y_in_f_"_A9_holds_ x_in_f_"_A9 let x, y be Element of X; ::_thesis: ( x \ y in f " A9 & y in f " A9 implies x in f " A9 ) assume that A3: x \ y in f " A9 and A4: y in f " A9 ; ::_thesis: x in f " A9 f . (x \ y) in A9 by A3, FUNCT_2:38; then A5: (f . x) \ (f . y) in A9 by Def6; f . y in A9 by A4, FUNCT_2:38; then f . x in A9 by A1, A5, BCIALG_1:def_18; hence x in f " A9 by FUNCT_2:38; ::_thesis: verum end; 0. X9 in A9 by A1, BCIALG_1:def_18; then f . (0. X) in A9 by Th35; then 0. X in f " A9 by FUNCT_2:38; hence f " A9 is Ideal of X by A2, BCIALG_1:def_18; ::_thesis: verum end; theorem :: BCIALG_6:46 for X9, X being BCI-algebra for A9 being non empty Subset of X9 for f being BCI-homomorphism of X,X9 st A9 is closed Ideal of X9 holds f " A9 is closed Ideal of X proof let X9, X be BCI-algebra; ::_thesis: for A9 being non empty Subset of X9 for f being BCI-homomorphism of X,X9 st A9 is closed Ideal of X9 holds f " A9 is closed Ideal of X let A9 be non empty Subset of X9; ::_thesis: for f being BCI-homomorphism of X,X9 st A9 is closed Ideal of X9 holds f " A9 is closed Ideal of X let f be BCI-homomorphism of X,X9; ::_thesis: ( A9 is closed Ideal of X9 implies f " A9 is closed Ideal of X ) assume A1: A9 is closed Ideal of X9 ; ::_thesis: f " A9 is closed Ideal of X then reconsider XY = f " A9 as Ideal of X by Th45; for y being Element of XY holds y ` in XY proof let y be Element of XY; ::_thesis: y ` in XY A2: f . y in A9 by FUNCT_2:38; reconsider y = y as Element of X ; (f . y) ` in A9 by A1, A2, BCIALG_1:def_19; then (f . (0. X)) \ (f . y) in A9 by Th35; then f . (y `) in A9 by Def6; hence y ` in XY by FUNCT_2:38; ::_thesis: verum end; hence f " A9 is closed Ideal of X by BCIALG_1:def_19; ::_thesis: verum end; theorem Th47: :: BCIALG_6:47 for X, X9 being BCI-algebra for I being Ideal of X for f being BCI-homomorphism of X,X9 st f is onto holds f .: I is Ideal of X9 proof let X, X9 be BCI-algebra; ::_thesis: for I being Ideal of X for f being BCI-homomorphism of X,X9 st f is onto holds f .: I is Ideal of X9 let I be Ideal of X; ::_thesis: for f being BCI-homomorphism of X,X9 st f is onto holds f .: I is Ideal of X9 let f be BCI-homomorphism of X,X9; ::_thesis: ( f is onto implies f .: I is Ideal of X9 ) 0. X in the carrier of X ; then A1: 0. X in dom f by FUNCT_2:def_1; ( 0. X in I & f . (0. X) = 0. X9 ) by Th35, BCIALG_1:def_18; then reconsider imaf = f .: I as non empty Subset of X9 by A1, FUNCT_1:def_6; 0. X in the carrier of X ; then A2: 0. X in dom f by FUNCT_2:def_1; assume A3: f is onto ; ::_thesis: f .: I is Ideal of X9 A4: for x, y being Element of X9 st x \ y in imaf & y in imaf holds x in imaf proof let x, y be Element of X9; ::_thesis: ( x \ y in imaf & y in imaf implies x in imaf ) assume that A5: x \ y in imaf and A6: y in imaf ; ::_thesis: x in imaf consider y9 being set such that A7: y9 in dom f and A8: y9 in I and A9: y = f . y9 by A6, FUNCT_1:def_6; consider yy being Element of X such that A10: f . yy = x by A3, Th42; consider z being set such that A11: z in dom f and A12: z in I and A13: x \ y = f . z by A5, FUNCT_1:def_6; reconsider y9 = y9, z = z as Element of X by A7, A11; set u = yy \ ((yy \ y9) \ z); ((yy \ y9) \ ((yy \ y9) \ z)) \ z = 0. X by BCIALG_1:1; then ((yy \ ((yy \ y9) \ z)) \ y9) \ z = 0. X by BCIALG_1:7; then ((yy \ ((yy \ y9) \ z)) \ y9) \ z in I by BCIALG_1:def_18; then (yy \ ((yy \ y9) \ z)) \ y9 in I by A12, BCIALG_1:def_18; then A14: yy \ ((yy \ y9) \ z) in I by A8, BCIALG_1:def_18; yy \ ((yy \ y9) \ z) in the carrier of X ; then yy \ ((yy \ y9) \ z) in dom f by FUNCT_2:def_1; then [(yy \ ((yy \ y9) \ z)),(f . (yy \ ((yy \ y9) \ z)))] in f by FUNCT_1:1; then f . (yy \ ((yy \ y9) \ z)) in f .: I by A14, RELAT_1:def_13; then (f . yy) \ (f . ((yy \ y9) \ z)) in f .: I by Def6; then (f . yy) \ ((f . (yy \ y9)) \ (f . z)) in f .: I by Def6; then (f . yy) \ ((x \ y) \ (x \ y)) in f .: I by A9, A13, A10, Def6; then (f . yy) \ (0. X9) in f .: I by BCIALG_1:def_5; hence x in imaf by A10, BCIALG_1:2; ::_thesis: verum end; ( 0. X in I & f . (0. X) = 0. X9 ) by Th35, BCIALG_1:def_18; then 0. X9 in imaf by A2, FUNCT_1:def_6; hence f .: I is Ideal of X9 by A4, BCIALG_1:def_18; ::_thesis: verum end; theorem :: BCIALG_6:48 for X, X9 being BCI-algebra for CI being closed Ideal of X for f being BCI-homomorphism of X,X9 st f is onto holds f .: CI is closed Ideal of X9 proof let X, X9 be BCI-algebra; ::_thesis: for CI being closed Ideal of X for f being BCI-homomorphism of X,X9 st f is onto holds f .: CI is closed Ideal of X9 let CI be closed Ideal of X; ::_thesis: for f being BCI-homomorphism of X,X9 st f is onto holds f .: CI is closed Ideal of X9 let f be BCI-homomorphism of X,X9; ::_thesis: ( f is onto implies f .: CI is closed Ideal of X9 ) assume f is onto ; ::_thesis: f .: CI is closed Ideal of X9 then reconsider Kf = f .: CI as Ideal of X9 by Th47; now__::_thesis:_for_x9_being_Element_of_Kf_holds_x9_`_in_Kf let x9 be Element of Kf; ::_thesis: x9 ` in Kf consider x being set such that x in dom f and A1: x in CI and A2: x9 = f . x by FUNCT_1:def_6; reconsider x = x as Element of CI by A1; x ` in the carrier of X ; then x ` in dom f by FUNCT_2:def_1; then ( x ` in CI & [(x `),(f . (x `))] in f ) by BCIALG_1:def_19, FUNCT_1:1; then f . (x `) in f .: CI by RELAT_1:def_13; then (f . (0. X)) \ (f . x) in f .: CI by Def6; hence x9 ` in Kf by A2, Th35; ::_thesis: verum end; hence f .: CI is closed Ideal of X9 by BCIALG_1:def_19; ::_thesis: verum end; definition let X, X9 be BCI-algebra; predX,X9 are_isomorphic means :Def9: :: BCIALG_6:def 9 ex f being BCI-homomorphism of X,X9 st f is bijective ; end; :: deftheorem Def9 defines are_isomorphic BCIALG_6:def_9_:_ for X, X9 being BCI-algebra holds ( X,X9 are_isomorphic iff ex f being BCI-homomorphism of X,X9 st f is bijective ); registration let X be BCI-algebra; let I be Ideal of X; let RI be I-congruence of X,I; clusterX ./. RI -> strict being_B being_C being_I being_BCI-4 ; coherence ( X ./. RI is strict & X ./. RI is being_B & X ./. RI is being_C & X ./. RI is being_I & X ./. RI is being_BCI-4 ) ; end; definition let X be BCI-algebra; let I be Ideal of X; let RI be I-congruence of X,I; func nat_hom RI -> BCI-homomorphism of X,(X ./. RI) means :Def10: :: BCIALG_6:def 10 for x being Element of X holds it . x = Class (RI,x); existence ex b1 being BCI-homomorphism of X,(X ./. RI) st for x being Element of X holds b1 . x = Class (RI,x) proof defpred S1[ Element of X, set ] means $2 = Class (RI,$1); A1: for x being Element of X ex y being Element of (X ./. RI) st S1[x,y] proof let x be Element of X; ::_thesis: ex y being Element of (X ./. RI) st S1[x,y] reconsider y = Class (RI,x) as Element of (X ./. RI) by EQREL_1:def_3; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider f being Function of X,(X ./. RI) such that A2: for x being Element of X holds S1[x,f . x] from FUNCT_2:sch_3(A1); now__::_thesis:_for_a,_b_being_Element_of_X_holds_(f_._a)_\_(f_._b)_=_f_._(a_\_b) let a, b be Element of X; ::_thesis: (f . a) \ (f . b) = f . (a \ b) ( f . a = Class (RI,a) & f . b = Class (RI,b) ) by A2; then (f . a) \ (f . b) = Class (RI,(a \ b)) by BCIALG_2:def_17; hence (f . a) \ (f . b) = f . (a \ b) by A2; ::_thesis: verum end; then reconsider f = f as BCI-homomorphism of X,(X ./. RI) by Def6; take f ; ::_thesis: for x being Element of X holds f . x = Class (RI,x) thus for x being Element of X holds f . x = Class (RI,x) by A2; ::_thesis: verum end; uniqueness for b1, b2 being BCI-homomorphism of X,(X ./. RI) st ( for x being Element of X holds b1 . x = Class (RI,x) ) & ( for x being Element of X holds b2 . x = Class (RI,x) ) holds b1 = b2 proof let f, g be BCI-homomorphism of X,(X ./. RI); ::_thesis: ( ( for x being Element of X holds f . x = Class (RI,x) ) & ( for x being Element of X holds g . x = Class (RI,x) ) implies f = g ) assume that A3: for x being Element of X holds f . x = Class (RI,x) and A4: for x being Element of X holds g . x = Class (RI,x) ; ::_thesis: f = g now__::_thesis:_for_x_being_Element_of_X_holds_f_._x_=_g_._x let x be Element of X; ::_thesis: f . x = g . x f . x = Class (RI,x) by A3; hence f . x = g . x by A4; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def10 defines nat_hom BCIALG_6:def_10_:_ for X being BCI-algebra for I being Ideal of X for RI being I-congruence of X,I for b4 being BCI-homomorphism of X,(X ./. RI) holds ( b4 = nat_hom RI iff for x being Element of X holds b4 . x = Class (RI,x) ); begin theorem :: BCIALG_6:49 for X being BCI-algebra for I being Ideal of X for RI being I-congruence of X,I holds nat_hom RI is onto proof let X be BCI-algebra; ::_thesis: for I being Ideal of X for RI being I-congruence of X,I holds nat_hom RI is onto let I be Ideal of X; ::_thesis: for RI being I-congruence of X,I holds nat_hom RI is onto let RI be I-congruence of X,I; ::_thesis: nat_hom RI is onto set f = nat_hom RI; set Y = X ./. RI; reconsider Y = X ./. RI as BCI-algebra ; reconsider f = nat_hom RI as BCI-homomorphism of X,Y ; for y being set st y in the carrier of Y holds ex x being set st ( x in the carrier of X & y = f . x ) proof let y be set ; ::_thesis: ( y in the carrier of Y implies ex x being set st ( x in the carrier of X & y = f . x ) ) assume A1: y in the carrier of Y ; ::_thesis: ex x being set st ( x in the carrier of X & y = f . x ) then reconsider y = y as Element of Y ; consider x being set such that A2: x in the carrier of X and A3: y = Class (RI,x) by A1, EQREL_1:def_3; take x ; ::_thesis: ( x in the carrier of X & y = f . x ) thus ( x in the carrier of X & y = f . x ) by A2, A3, Def10; ::_thesis: verum end; then rng f = the carrier of Y by FUNCT_2:10; hence nat_hom RI is onto by FUNCT_2:def_3; ::_thesis: verum end; theorem Th50: :: BCIALG_6:50 for X, X9 being BCI-algebra for I being Ideal of X for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f holds ex h being BCI-homomorphism of (X ./. RI),X9 st ( f = h * (nat_hom RI) & h is one-to-one ) proof let X, X9 be BCI-algebra; ::_thesis: for I being Ideal of X for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f holds ex h being BCI-homomorphism of (X ./. RI),X9 st ( f = h * (nat_hom RI) & h is one-to-one ) let I be Ideal of X; ::_thesis: for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f holds ex h being BCI-homomorphism of (X ./. RI),X9 st ( f = h * (nat_hom RI) & h is one-to-one ) let RI be I-congruence of X,I; ::_thesis: for f being BCI-homomorphism of X,X9 st I = Ker f holds ex h being BCI-homomorphism of (X ./. RI),X9 st ( f = h * (nat_hom RI) & h is one-to-one ) let f be BCI-homomorphism of X,X9; ::_thesis: ( I = Ker f implies ex h being BCI-homomorphism of (X ./. RI),X9 st ( f = h * (nat_hom RI) & h is one-to-one ) ) set J = X ./. RI; defpred S1[ set , set ] means for a being Element of X st $1 = Class (RI,a) holds $2 = f . a; A1: dom (nat_hom RI) = the carrier of X by FUNCT_2:def_1; assume A2: I = Ker f ; ::_thesis: ex h being BCI-homomorphism of (X ./. RI),X9 st ( f = h * (nat_hom RI) & h is one-to-one ) A3: for x being Element of (X ./. RI) ex y being Element of X9 st S1[x,y] proof let x be Element of (X ./. RI); ::_thesis: ex y being Element of X9 st S1[x,y] x in Class RI ; then consider y being set such that A4: y in the carrier of X and A5: x = Class (RI,y) by EQREL_1:def_3; reconsider y = y as Element of X by A4; reconsider t = f . y as Element of X9 ; take t ; ::_thesis: S1[x,t] let a be Element of X; ::_thesis: ( x = Class (RI,a) implies t = f . a ) assume x = Class (RI,a) ; ::_thesis: t = f . a then y in Class (RI,a) by A5, EQREL_1:23; then A6: [a,y] in RI by EQREL_1:18; then y \ a in Ker f by A2, BCIALG_2:def_12; then ex x2 being Element of X st ( y \ a = x2 & f . x2 = 0. X9 ) ; then A7: (f . y) \ (f . a) = 0. X9 by Def6; a \ y in Ker f by A2, A6, BCIALG_2:def_12; then ex x1 being Element of X st ( a \ y = x1 & f . x1 = 0. X9 ) ; then (f . a) \ (f . y) = 0. X9 by Def6; hence t = f . a by A7, BCIALG_1:def_7; ::_thesis: verum end; consider h being Function of (X ./. RI),X9 such that A8: for x being Element of (X ./. RI) holds S1[x,h . x] from FUNCT_2:sch_3(A3); now__::_thesis:_for_a,_b_being_Element_of_(X_./._RI)_holds_(h_._a)_\_(h_._b)_=_h_._(a_\_b) let a, b be Element of (X ./. RI); ::_thesis: (h . a) \ (h . b) = h . (a \ b) a in Class RI ; then consider a1 being set such that A9: a1 in the carrier of X and A10: a = Class (RI,a1) by EQREL_1:def_3; b in Class RI ; then consider b1 being set such that A11: b1 in the carrier of X and A12: b = Class (RI,b1) by EQREL_1:def_3; reconsider a1 = a1, b1 = b1 as Element of X by A9, A11; A13: a \ b = Class (RI,(a1 \ b1)) by A10, A12, BCIALG_2:def_17; A14: h . b = f . b1 by A8, A12; h . a = f . a1 by A8, A10; then (h . a) \ (h . b) = f . (a1 \ b1) by A14, Def6; hence (h . a) \ (h . b) = h . (a \ b) by A8, A13; ::_thesis: verum end; then reconsider h = h as BCI-homomorphism of (X ./. RI),X9 by Def6; A15: h is one-to-one proof let y1, y2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not y1 in dom h or not y2 in dom h or not h . y1 = h . y2 or y1 = y2 ) assume that A16: ( y1 in dom h & y2 in dom h ) and A17: h . y1 = h . y2 ; ::_thesis: y1 = y2 reconsider S = y1, T = y2 as Element of (X ./. RI) by A16; S in Class RI ; then consider a1 being set such that A18: a1 in the carrier of X and A19: S = Class (RI,a1) by EQREL_1:def_3; T in Class RI ; then consider b1 being set such that A20: b1 in the carrier of X and A21: T = Class (RI,b1) by EQREL_1:def_3; reconsider a1 = a1, b1 = b1 as Element of X by A18, A20; A22: h . T = f . b1 by A8, A21; A23: h . S = f . a1 by A8, A19; then (f . b1) \ (f . a1) = 0. X9 by A17, A22, BCIALG_1:def_5; then f . (b1 \ a1) = 0. X9 by Def6; then A24: b1 \ a1 in Ker f ; (f . a1) \ (f . b1) = 0. X9 by A17, A23, A22, BCIALG_1:def_5; then f . (a1 \ b1) = 0. X9 by Def6; then a1 \ b1 in Ker f ; then [a1,b1] in RI by A2, A24, BCIALG_2:def_12; then b1 in Class (RI,a1) by EQREL_1:18; hence y1 = y2 by A19, A21, EQREL_1:23; ::_thesis: verum end; A25: dom f = the carrier of X by FUNCT_2:def_1; A26: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_f_implies_(_x_in_dom_(nat_hom_RI)_&_(nat_hom_RI)_._x_in_dom_h_)_)_&_(_x_in_dom_(nat_hom_RI)_&_(nat_hom_RI)_._x_in_dom_h_implies_x_in_dom_f_)_) let x be set ; ::_thesis: ( ( x in dom f implies ( x in dom (nat_hom RI) & (nat_hom RI) . x in dom h ) ) & ( x in dom (nat_hom RI) & (nat_hom RI) . x in dom h implies x in dom f ) ) thus ( x in dom f implies ( x in dom (nat_hom RI) & (nat_hom RI) . x in dom h ) ) ::_thesis: ( x in dom (nat_hom RI) & (nat_hom RI) . x in dom h implies x in dom f ) proof assume A27: x in dom f ; ::_thesis: ( x in dom (nat_hom RI) & (nat_hom RI) . x in dom h ) hence x in dom (nat_hom RI) by A1; ::_thesis: (nat_hom RI) . x in dom h A28: dom h = the carrier of (X ./. RI) by FUNCT_2:def_1; (nat_hom RI) . x in rng (nat_hom RI) by A1, A27, FUNCT_1:def_3; hence (nat_hom RI) . x in dom h by A28; ::_thesis: verum end; assume that A29: x in dom (nat_hom RI) and (nat_hom RI) . x in dom h ; ::_thesis: x in dom f thus x in dom f by A25, A29; ::_thesis: verum end; take h ; ::_thesis: ( f = h * (nat_hom RI) & h is one-to-one ) now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_h_._((nat_hom_RI)_._x) let x be set ; ::_thesis: ( x in dom f implies f . x = h . ((nat_hom RI) . x) ) assume x in dom f ; ::_thesis: f . x = h . ((nat_hom RI) . x) then reconsider a = x as Element of X ; (nat_hom RI) . a = Class (RI,a) by Def10; hence f . x = h . ((nat_hom RI) . x) by A8; ::_thesis: verum end; hence ( f = h * (nat_hom RI) & h is one-to-one ) by A15, A26, FUNCT_1:10; ::_thesis: verum end; theorem :: BCIALG_6:51 for X, X9 being BCI-algebra for I being Ideal of X for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f holds ex h being BCI-homomorphism of (X ./. RI),X9 st ( f = h * (nat_hom RI) & h is one-to-one ) by Th50; theorem :: BCIALG_6:52 for X being BCI-algebra for K being closed Ideal of X for RK being I-congruence of X,K holds Ker (nat_hom RK) = K proof let X be BCI-algebra; ::_thesis: for K being closed Ideal of X for RK being I-congruence of X,K holds Ker (nat_hom RK) = K let K be closed Ideal of X; ::_thesis: for RK being I-congruence of X,K holds Ker (nat_hom RK) = K let RK be I-congruence of X,K; ::_thesis: Ker (nat_hom RK) = K set h = nat_hom RK; set Y = X ./. RK; thus Ker (nat_hom RK) c= K :: according to XBOOLE_0:def_10 ::_thesis: K c= Ker (nat_hom RK) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Ker (nat_hom RK) or y in K ) assume y in Ker (nat_hom RK) ; ::_thesis: y in K then consider x being Element of X such that A1: y = x and A2: (nat_hom RK) . x = 0. (X ./. RK) ; Class (RK,(0. X)) = Class (RK,x) by A2, Def10; then x in Class (RK,(0. X)) by EQREL_1:23; then [(0. X),x] in RK by EQREL_1:18; then x \ (0. X) in K by BCIALG_2:def_12; hence y in K by A1, BCIALG_1:2; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in K or y in Ker (nat_hom RK) ) assume A3: y in K ; ::_thesis: y in Ker (nat_hom RK) then reconsider x = y as Element of X ; ( x \ (0. X) in K & x ` in K ) by A3, BCIALG_1:2, BCIALG_1:def_19; then [(0. X),x] in RK by BCIALG_2:def_12; then x in Class (RK,(0. X)) by EQREL_1:18; then Class (RK,(0. X)) = Class (RK,x) by EQREL_1:23; then (nat_hom RK) . x = 0. (X ./. RK) by Def10; hence y in Ker (nat_hom RK) ; ::_thesis: verum end; Lm4: for X9, X being BCI-algebra for H9 being SubAlgebra of X9 for f being BCI-homomorphism of X,X9 st the carrier of H9 = rng f holds f is BCI-homomorphism of X,H9 proof let X9, X be BCI-algebra; ::_thesis: for H9 being SubAlgebra of X9 for f being BCI-homomorphism of X,X9 st the carrier of H9 = rng f holds f is BCI-homomorphism of X,H9 let H9 be SubAlgebra of X9; ::_thesis: for f being BCI-homomorphism of X,X9 st the carrier of H9 = rng f holds f is BCI-homomorphism of X,H9 let f be BCI-homomorphism of X,X9; ::_thesis: ( the carrier of H9 = rng f implies f is BCI-homomorphism of X,H9 ) A1: the carrier of X = dom f by FUNCT_2:def_1; assume the carrier of H9 = rng f ; ::_thesis: f is BCI-homomorphism of X,H9 then reconsider h = f as Function of X,H9 by A1, RELSET_1:4; now__::_thesis:_for_a,_b_being_Element_of_X_holds_h_._(a_\_b)_=_(h_._a)_\_(h_._b) let a, b be Element of X; ::_thesis: h . (a \ b) = (h . a) \ (h . b) (h . a) \ (h . b) = (f . a) \ (f . b) by Th34; hence h . (a \ b) = (h . a) \ (h . b) by Def6; ::_thesis: verum end; hence f is BCI-homomorphism of X,H9 by Def6; ::_thesis: verum end; begin theorem :: BCIALG_6:53 for X9, X being BCI-algebra for H9 being SubAlgebra of X9 for I being Ideal of X for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f & the carrier of H9 = rng f holds X ./. RI,H9 are_isomorphic proof let X9, X be BCI-algebra; ::_thesis: for H9 being SubAlgebra of X9 for I being Ideal of X for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f & the carrier of H9 = rng f holds X ./. RI,H9 are_isomorphic let H9 be SubAlgebra of X9; ::_thesis: for I being Ideal of X for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f & the carrier of H9 = rng f holds X ./. RI,H9 are_isomorphic let I be Ideal of X; ::_thesis: for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f & the carrier of H9 = rng f holds X ./. RI,H9 are_isomorphic let RI be I-congruence of X,I; ::_thesis: for f being BCI-homomorphism of X,X9 st I = Ker f & the carrier of H9 = rng f holds X ./. RI,H9 are_isomorphic let f be BCI-homomorphism of X,X9; ::_thesis: ( I = Ker f & the carrier of H9 = rng f implies X ./. RI,H9 are_isomorphic ) assume that A1: I = Ker f and A2: the carrier of H9 = rng f ; ::_thesis: X ./. RI,H9 are_isomorphic defpred S1[ set , set ] means for a being Element of X st $1 = Class (RI,a) holds $2 = f . a; set J = X ./. RI; A3: for x being Element of (X ./. RI) ex y being Element of H9 st S1[x,y] proof let x be Element of (X ./. RI); ::_thesis: ex y being Element of H9 st S1[x,y] x in Class RI ; then consider y being set such that A4: y in the carrier of X and A5: x = Class (RI,y) by EQREL_1:def_3; reconsider y = y as Element of X by A4; dom f = the carrier of X by FUNCT_2:def_1; then reconsider t = f . y as Element of H9 by A2, FUNCT_1:def_3; take t ; ::_thesis: S1[x,t] let a be Element of X; ::_thesis: ( x = Class (RI,a) implies t = f . a ) assume x = Class (RI,a) ; ::_thesis: t = f . a then y in Class (RI,a) by A5, EQREL_1:23; then A6: [a,y] in RI by EQREL_1:18; then y \ a in Ker f by A1, BCIALG_2:def_12; then ex x2 being Element of X st ( y \ a = x2 & f . x2 = 0. X9 ) ; then A7: (f . y) \ (f . a) = 0. X9 by Def6; a \ y in Ker f by A1, A6, BCIALG_2:def_12; then ex x1 being Element of X st ( a \ y = x1 & f . x1 = 0. X9 ) ; then (f . a) \ (f . y) = 0. X9 by Def6; hence t = f . a by A7, BCIALG_1:def_7; ::_thesis: verum end; consider h being Function of (X ./. RI),H9 such that A8: for x being Element of (X ./. RI) holds S1[x,h . x] from FUNCT_2:sch_3(A3); now__::_thesis:_for_a,_b_being_Element_of_(X_./._RI)_holds_(h_._a)_\_(h_._b)_=_h_._(a_\_b) reconsider f = f as BCI-homomorphism of X,H9 by A2, Lm4; let a, b be Element of (X ./. RI); ::_thesis: (h . a) \ (h . b) = h . (a \ b) a in Class RI ; then consider a1 being set such that A9: a1 in the carrier of X and A10: a = Class (RI,a1) by EQREL_1:def_3; b in Class RI ; then consider b1 being set such that A11: b1 in the carrier of X and A12: b = Class (RI,b1) by EQREL_1:def_3; reconsider a1 = a1, b1 = b1 as Element of X by A9, A11; A13: a \ b = Class (RI,(a1 \ b1)) by A10, A12, BCIALG_2:def_17; A14: h . b = f . b1 by A8, A12; h . a = f . a1 by A8, A10; then (h . a) \ (h . b) = f . (a1 \ b1) by A14, Def6; hence (h . a) \ (h . b) = h . (a \ b) by A8, A13; ::_thesis: verum end; then reconsider h = h as BCI-homomorphism of (X ./. RI),H9 by Def6; A15: h is one-to-one proof let y1, y2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not y1 in dom h or not y2 in dom h or not h . y1 = h . y2 or y1 = y2 ) assume that A16: ( y1 in dom h & y2 in dom h ) and A17: h . y1 = h . y2 ; ::_thesis: y1 = y2 reconsider y1 = y1, y2 = y2 as Element of (X ./. RI) by A16; y1 in Class RI ; then consider a1 being set such that A18: a1 in the carrier of X and A19: y1 = Class (RI,a1) by EQREL_1:def_3; y2 in Class RI ; then consider b1 being set such that A20: b1 in the carrier of X and A21: y2 = Class (RI,b1) by EQREL_1:def_3; reconsider a1 = a1, b1 = b1 as Element of X by A18, A20; A22: h . y2 = f . b1 by A8, A21; A23: h . y1 = f . a1 by A8, A19; then (f . b1) \ (f . a1) = 0. X9 by A17, A22, BCIALG_1:def_5; then f . (b1 \ a1) = 0. X9 by Def6; then A24: b1 \ a1 in Ker f ; (f . a1) \ (f . b1) = 0. X9 by A17, A23, A22, BCIALG_1:def_5; then f . (a1 \ b1) = 0. X9 by Def6; then a1 \ b1 in Ker f ; then [a1,b1] in RI by A1, A24, BCIALG_2:def_12; then b1 in Class (RI,a1) by EQREL_1:18; hence y1 = y2 by A19, A21, EQREL_1:23; ::_thesis: verum end; the carrier of H9 c= rng h proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of H9 or y in rng h ) A25: the carrier of (X ./. RI) = dom h by FUNCT_2:def_1; assume y in the carrier of H9 ; ::_thesis: y in rng h then consider x being set such that A26: x in dom f and A27: y = f . x by A2, FUNCT_1:def_3; reconsider S = Class (RI,x) as Element of (X ./. RI) by A26, EQREL_1:def_3; h . S = f . x by A8, A26; hence y in rng h by A27, A25, FUNCT_1:def_3; ::_thesis: verum end; then rng h = the carrier of H9 by XBOOLE_0:def_10; then h is onto by FUNCT_2:def_3; hence X ./. RI,H9 are_isomorphic by A15, Def9; ::_thesis: verum end; theorem Th54: :: BCIALG_6:54 for X, X9 being BCI-algebra for I being Ideal of X for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f & f is onto holds X ./. RI,X9 are_isomorphic proof let X, X9 be BCI-algebra; ::_thesis: for I being Ideal of X for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f & f is onto holds X ./. RI,X9 are_isomorphic let I be Ideal of X; ::_thesis: for RI being I-congruence of X,I for f being BCI-homomorphism of X,X9 st I = Ker f & f is onto holds X ./. RI,X9 are_isomorphic let RI be I-congruence of X,I; ::_thesis: for f being BCI-homomorphism of X,X9 st I = Ker f & f is onto holds X ./. RI,X9 are_isomorphic let f be BCI-homomorphism of X,X9; ::_thesis: ( I = Ker f & f is onto implies X ./. RI,X9 are_isomorphic ) assume that A1: I = Ker f and A2: f is onto ; ::_thesis: X ./. RI,X9 are_isomorphic consider h being BCI-homomorphism of (X ./. RI),X9 such that A3: f = h * (nat_hom RI) and A4: h is one-to-one by A1, Th50; for y being set st y in the carrier of X9 holds ex z being set st ( z in the carrier of (X ./. RI) & h . z = y ) proof let y be set ; ::_thesis: ( y in the carrier of X9 implies ex z being set st ( z in the carrier of (X ./. RI) & h . z = y ) ) assume y in the carrier of X9 ; ::_thesis: ex z being set st ( z in the carrier of (X ./. RI) & h . z = y ) then y in rng f by A2, FUNCT_2:def_3; then consider x being set such that A5: x in dom f and A6: y = f . x by FUNCT_1:def_3; take (nat_hom RI) . x ; ::_thesis: ( (nat_hom RI) . x in the carrier of (X ./. RI) & h . ((nat_hom RI) . x) = y ) A7: dom (nat_hom RI) = the carrier of X by FUNCT_2:def_1; then (nat_hom RI) . x in rng (nat_hom RI) by A5, FUNCT_1:def_3; hence ( (nat_hom RI) . x in the carrier of (X ./. RI) & h . ((nat_hom RI) . x) = y ) by A3, A5, A6, A7, FUNCT_1:13; ::_thesis: verum end; then rng h = the carrier of X9 by FUNCT_2:10; then h is onto by FUNCT_2:def_3; hence X ./. RI,X9 are_isomorphic by A4, Def9; ::_thesis: verum end; begin definition let X be BCI-algebra; let G be SubAlgebra of X; let K be closed Ideal of X; let RK be I-congruence of X,K; func Union (G,RK) -> non empty Subset of X equals :: BCIALG_6:def 11 union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ; correctness coherence union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } is non empty Subset of X; proof set Z2 = { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ; set Z1 = union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ; A1: now__::_thesis:_for_x_being_set_st_x_in_union__{__(Class_(RK,a))_where_a_is_Element_of_G_:_Class_(RK,a)_in_the_carrier_of_(X_./._RK)__}__holds_ x_in_the_carrier_of_X let x be set ; ::_thesis: ( x in union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } implies x in the carrier of X ) assume x in union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ; ::_thesis: x in the carrier of X then consider g being set such that A2: x in g and A3: g in { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } by TARSKI:def_4; ex a being Element of G st ( g = Class (RK,a) & Class (RK,a) in the carrier of (X ./. RK) ) by A3; hence x in the carrier of X by A2; ::_thesis: verum end; 0. X = 0. G by BCIALG_1:def_10; then A4: Class (RK,(0. X)) in { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ; [(0. X),(0. X)] in RK by EQREL_1:5; then 0. X in Class (RK,(0. X)) by EQREL_1:18; hence union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } is non empty Subset of X by A4, A1, TARSKI:def_3, TARSKI:def_4; ::_thesis: verum end; end; :: deftheorem defines Union BCIALG_6:def_11_:_ for X being BCI-algebra for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K holds Union (G,RK) = union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ; Lm5: for X being BCI-algebra for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K for w being Element of Union (G,RK) ex a being Element of G st w in Class (RK,a) proof let X be BCI-algebra; ::_thesis: for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K for w being Element of Union (G,RK) ex a being Element of G st w in Class (RK,a) let G be SubAlgebra of X; ::_thesis: for K being closed Ideal of X for RK being I-congruence of X,K for w being Element of Union (G,RK) ex a being Element of G st w in Class (RK,a) let K be closed Ideal of X; ::_thesis: for RK being I-congruence of X,K for w being Element of Union (G,RK) ex a being Element of G st w in Class (RK,a) let RK be I-congruence of X,K; ::_thesis: for w being Element of Union (G,RK) ex a being Element of G st w in Class (RK,a) set Z2 = { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ; let w be Element of Union (G,RK); ::_thesis: ex a being Element of G st w in Class (RK,a) consider g being set such that A1: w in g and A2: g in { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } by TARSKI:def_4; consider a being Element of G such that A3: g = Class (RK,a) and Class (RK,a) in the carrier of (X ./. RK) by A2; take a ; ::_thesis: w in Class (RK,a) thus w in Class (RK,a) by A1, A3; ::_thesis: verum end; definition let X be BCI-algebra; let G be SubAlgebra of X; let K be closed Ideal of X; let RK be I-congruence of X,K; func HKOp (G,RK) -> BinOp of (Union (G,RK)) means :Def12: :: BCIALG_6:def 12 for w1, w2 being Element of Union (G,RK) for x, y being Element of X st w1 = x & w2 = y holds it . (w1,w2) = x \ y; existence ex b1 being BinOp of (Union (G,RK)) st for w1, w2 being Element of Union (G,RK) for x, y being Element of X st w1 = x & w2 = y holds b1 . (w1,w2) = x \ y proof defpred S1[ Element of Union (G,RK), Element of Union (G,RK), set ] means for x, y being Element of X st $1 = x & $2 = y holds $3 = x \ y; A1: for w1, w2 being Element of Union (G,RK) ex v being Element of Union (G,RK) st S1[w1,w2,v] proof let w1, w2 be Element of Union (G,RK); ::_thesis: ex v being Element of Union (G,RK) st S1[w1,w2,v] consider a being Element of G such that A2: w1 in Class (RK,a) by Lm5; A3: [a,w1] in RK by A2, EQREL_1:18; consider b being Element of G such that A4: w2 in Class (RK,b) by Lm5; the carrier of G c= the carrier of X by BCIALG_1:def_10; then reconsider a1 = a, b1 = b as Element of X by TARSKI:def_3; Class (RK,(a1 \ b1)) in the carrier of (X ./. RK) by EQREL_1:def_3; then Class (RK,(a \ b)) in the carrier of (X ./. RK) by Th34; then A5: Class (RK,(a \ b)) in { (Class (RK,c)) where c is Element of G : Class (RK,c) in the carrier of (X ./. RK) } ; A6: [b,w2] in RK by A4, EQREL_1:18; reconsider w1 = w1, w2 = w2 as Element of X ; [(a1 \ b1),(w1 \ w2)] in RK by A3, A6, BCIALG_2:def_9; then w1 \ w2 in Class (RK,(a1 \ b1)) by EQREL_1:18; then w1 \ w2 in Class (RK,(a \ b)) by Th34; then reconsider C = w1 \ w2 as Element of Union (G,RK) by A5, TARSKI:def_4; take C ; ::_thesis: S1[w1,w2,C] thus S1[w1,w2,C] ; ::_thesis: verum end; thus ex B being BinOp of (Union (G,RK)) st for w1, w2 being Element of Union (G,RK) holds S1[w1,w2,B . (w1,w2)] from BINOP_1:sch_3(A1); ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Union (G,RK)) st ( for w1, w2 being Element of Union (G,RK) for x, y being Element of X st w1 = x & w2 = y holds b1 . (w1,w2) = x \ y ) & ( for w1, w2 being Element of Union (G,RK) for x, y being Element of X st w1 = x & w2 = y holds b2 . (w1,w2) = x \ y ) holds b1 = b2 proof let o1, o2 be BinOp of (Union (G,RK)); ::_thesis: ( ( for w1, w2 being Element of Union (G,RK) for x, y being Element of X st w1 = x & w2 = y holds o1 . (w1,w2) = x \ y ) & ( for w1, w2 being Element of Union (G,RK) for x, y being Element of X st w1 = x & w2 = y holds o2 . (w1,w2) = x \ y ) implies o1 = o2 ) assume A7: for w1, w2 being Element of Union (G,RK) for x, y being Element of X st w1 = x & w2 = y holds o1 . (w1,w2) = x \ y ; ::_thesis: ( ex w1, w2 being Element of Union (G,RK) ex x, y being Element of X st ( w1 = x & w2 = y & not o2 . (w1,w2) = x \ y ) or o1 = o2 ) assume A8: for w1, w2 being Element of Union (G,RK) for x, y being Element of X st w1 = x & w2 = y holds o2 . (w1,w2) = x \ y ; ::_thesis: o1 = o2 now__::_thesis:_for_w1,_w2_being_Element_of_Union_(G,RK)_holds_o1_._(w1,w2)_=_o2_._(w1,w2) let w1, w2 be Element of Union (G,RK); ::_thesis: o1 . (w1,w2) = o2 . (w1,w2) o1 . (w1,w2) = w1 \ w2 by A7; hence o1 . (w1,w2) = o2 . (w1,w2) by A8; ::_thesis: verum end; hence o1 = o2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def12 defines HKOp BCIALG_6:def_12_:_ for X being BCI-algebra for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K for b5 being BinOp of (Union (G,RK)) holds ( b5 = HKOp (G,RK) iff for w1, w2 being Element of Union (G,RK) for x, y being Element of X st w1 = x & w2 = y holds b5 . (w1,w2) = x \ y ); definition let X be BCI-algebra; let G be SubAlgebra of X; let K be closed Ideal of X; let RK be I-congruence of X,K; func zeroHK (G,RK) -> Element of Union (G,RK) equals :: BCIALG_6:def 13 0. X; coherence 0. X is Element of Union (G,RK) proof A1: 0. G = 0. X by BCIALG_1:def_10; then ( 0. G in Class (RK,(0. G)) & Class (RK,(0. G)) in { (Class (RK,c)) where c is Element of G : Class (RK,c) in the carrier of (X ./. RK) } ) by EQREL_1:20; hence 0. X is Element of Union (G,RK) by A1, TARSKI:def_4; ::_thesis: verum end; end; :: deftheorem defines zeroHK BCIALG_6:def_13_:_ for X being BCI-algebra for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K holds zeroHK (G,RK) = 0. X; definition let X be BCI-algebra; let G be SubAlgebra of X; let K be closed Ideal of X; let RK be I-congruence of X,K; func HK (G,RK) -> BCIStr_0 equals :: BCIALG_6:def 14 BCIStr_0(# (Union (G,RK)),(HKOp (G,RK)),(zeroHK (G,RK)) #); coherence BCIStr_0(# (Union (G,RK)),(HKOp (G,RK)),(zeroHK (G,RK)) #) is BCIStr_0 ; end; :: deftheorem defines HK BCIALG_6:def_14_:_ for X being BCI-algebra for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K holds HK (G,RK) = BCIStr_0(# (Union (G,RK)),(HKOp (G,RK)),(zeroHK (G,RK)) #); registration let X be BCI-algebra; let G be SubAlgebra of X; let K be closed Ideal of X; let RK be I-congruence of X,K; cluster HK (G,RK) -> non empty ; coherence not HK (G,RK) is empty ; end; definition let X be BCI-algebra; let G be SubAlgebra of X; let K be closed Ideal of X; let RK be I-congruence of X,K; let w1, w2 be Element of Union (G,RK); funcw1 \ w2 -> Element of Union (G,RK) equals :: BCIALG_6:def 15 (HKOp (G,RK)) . (w1,w2); coherence (HKOp (G,RK)) . (w1,w2) is Element of Union (G,RK) ; end; :: deftheorem defines \ BCIALG_6:def_15_:_ for X being BCI-algebra for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K for w1, w2 being Element of Union (G,RK) holds w1 \ w2 = (HKOp (G,RK)) . (w1,w2); theorem Th55: :: BCIALG_6:55 for X being BCI-algebra for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K holds HK (G,RK) is BCI-algebra proof let X be BCI-algebra; ::_thesis: for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K holds HK (G,RK) is BCI-algebra let G be SubAlgebra of X; ::_thesis: for K being closed Ideal of X for RK being I-congruence of X,K holds HK (G,RK) is BCI-algebra let K be closed Ideal of X; ::_thesis: for RK being I-congruence of X,K holds HK (G,RK) is BCI-algebra let RK be I-congruence of X,K; ::_thesis: HK (G,RK) is BCI-algebra reconsider IT = HK (G,RK) as non empty BCIStr_0 ; A1: IT is being_BCI-4 proof let x, y be Element of IT; :: according to BCIALG_1:def_7 ::_thesis: ( not x \ y = 0. IT or not y \ x = 0. IT or x = y ) reconsider x1 = x, y1 = y as Element of Union (G,RK) ; reconsider x2 = x1, y2 = y1 as Element of X ; assume ( x \ y = 0. IT & y \ x = 0. IT ) ; ::_thesis: x = y then ( x2 \ y2 = 0. X & y2 \ x2 = 0. X ) by Def12; hence x = y by BCIALG_1:def_7; ::_thesis: verum end; A2: now__::_thesis:_for_x,_y,_z_being_Element_of_IT_holds_((x_\_y)_\_(z_\_y))_\_(x_\_z)_=_0._IT let x, y, z be Element of IT; ::_thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT reconsider x1 = x, y1 = y, z1 = z as Element of Union (G,RK) ; reconsider x2 = x1, y2 = y1, z2 = z1 as Element of X ; ( x2 \ y2 = x1 \ y1 & z2 \ y2 = z1 \ y1 ) by Def12; then A3: (x2 \ y2) \ (z2 \ y2) = (x1 \ y1) \ (z1 \ y1) by Def12; x2 \ z2 = x1 \ z1 by Def12; then ((x2 \ y2) \ (z2 \ y2)) \ (x2 \ z2) = ((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1) by A3, Def12; hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT by BCIALG_1:def_3; ::_thesis: verum end; A4: IT is being_C proof let x, y, z be Element of IT; :: according to BCIALG_1:def_4 ::_thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT reconsider x1 = x, y1 = y, z1 = z as Element of Union (G,RK) ; reconsider x2 = x1, y2 = y1, z2 = z1 as Element of X ; x2 \ z2 = x1 \ z1 by Def12; then A5: (x2 \ z2) \ y2 = (x1 \ z1) \ y1 by Def12; x2 \ y2 = x1 \ y1 by Def12; then (x2 \ y2) \ z2 = (x1 \ y1) \ z1 by Def12; then ((x2 \ y2) \ z2) \ ((x2 \ z2) \ y2) = ((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1) by A5, Def12; hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT by BCIALG_1:def_4; ::_thesis: verum end; IT is being_I proof let x be Element of IT; :: according to BCIALG_1:def_5 ::_thesis: x \ x = 0. IT reconsider x1 = x as Element of Union (G,RK) ; reconsider x2 = x1 as Element of X ; x2 \ x2 = x1 \ x1 by Def12; hence x \ x = 0. IT by BCIALG_1:def_5; ::_thesis: verum end; hence HK (G,RK) is BCI-algebra by A2, A4, A1, BCIALG_1:def_3; ::_thesis: verum end; registration let X be BCI-algebra; let G be SubAlgebra of X; let K be closed Ideal of X; let RK be I-congruence of X,K; cluster HK (G,RK) -> strict being_B being_C being_I being_BCI-4 ; coherence ( HK (G,RK) is strict & HK (G,RK) is being_B & HK (G,RK) is being_C & HK (G,RK) is being_I & HK (G,RK) is being_BCI-4 ) by Th55; end; theorem Th56: :: BCIALG_6:56 for X being BCI-algebra for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K holds HK (G,RK) is SubAlgebra of X proof let X be BCI-algebra; ::_thesis: for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K holds HK (G,RK) is SubAlgebra of X let G be SubAlgebra of X; ::_thesis: for K being closed Ideal of X for RK being I-congruence of X,K holds HK (G,RK) is SubAlgebra of X let K be closed Ideal of X; ::_thesis: for RK being I-congruence of X,K holds HK (G,RK) is SubAlgebra of X let RK be I-congruence of X,K; ::_thesis: HK (G,RK) is SubAlgebra of X set IT = HK (G,RK); set V1 = the carrier of (HK (G,RK)); reconsider D = the carrier of (HK (G,RK)) as non empty set ; set A = the InternalDiff of X || the carrier of (HK (G,RK)); set VV = the carrier of X; dom the InternalDiff of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def_1; then dom ( the InternalDiff of X || the carrier of (HK (G,RK))) = [: the carrier of X, the carrier of X:] /\ [: the carrier of (HK (G,RK)), the carrier of (HK (G,RK)):] by RELAT_1:61; then A1: dom ( the InternalDiff of X || the carrier of (HK (G,RK))) = [:D,D:] by XBOOLE_1:28, ZFMISC_1:96; for y being set holds ( y in D iff ex z being set st ( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) ) proof let y be set ; ::_thesis: ( y in D iff ex z being set st ( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) ) A2: now__::_thesis:_(_ex_z_being_set_st_ (_z_in_dom_(_the_InternalDiff_of_X_||_the_carrier_of_(HK_(G,RK)))_&_y_=_(_the_InternalDiff_of_X_||_the_carrier_of_(HK_(G,RK)))_._z_)_implies_y_in_D_) given z being set such that A3: z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) and A4: y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ; ::_thesis: y in D consider x1, x2 being set such that A5: ( x1 in D & x2 in D ) and A6: z = [x1,x2] by A1, A3, ZFMISC_1:def_2; reconsider x1 = x1, x2 = x2 as Element of Union (G,RK) by A5; reconsider v1 = x1, v2 = x2 as Element of the carrier of X ; y = v1 \ v2 by A3, A4, A6, FUNCT_1:47; then y = x1 \ x2 by Def12; hence y in D ; ::_thesis: verum end; ( y in D implies ex z being set st ( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) ) proof assume A7: y in D ; ::_thesis: ex z being set st ( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) then reconsider y1 = y, y2 = 0. (HK (G,RK)) as Element of X ; A8: [y,(0. (HK (G,RK)))] in [:D,D:] by A7, ZFMISC_1:87; then ( the InternalDiff of X || the carrier of (HK (G,RK))) . [y,(0. (HK (G,RK)))] = y1 \ y2 by FUNCT_1:49 .= y by BCIALG_1:2 ; hence ex z being set st ( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) by A1, A8; ::_thesis: verum end; hence ( y in D iff ex z being set st ( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) ) by A2; ::_thesis: verum end; then rng ( the InternalDiff of X || the carrier of (HK (G,RK))) = D by FUNCT_1:def_3; then reconsider A = the InternalDiff of X || the carrier of (HK (G,RK)) as BinOp of the carrier of (HK (G,RK)) by A1, FUNCT_2:def_1, RELSET_1:4; set B = the InternalDiff of (HK (G,RK)); now__::_thesis:_for_x,_y_being_Element_of_the_carrier_of_(HK_(G,RK))_holds_A_._(x,y)_=_the_InternalDiff_of_(HK_(G,RK))_._(x,y) let x, y be Element of the carrier of (HK (G,RK)); ::_thesis: A . (x,y) = the InternalDiff of (HK (G,RK)) . (x,y) ( x in the carrier of (HK (G,RK)) & y in the carrier of (HK (G,RK)) ) ; then reconsider vx = x, vy = y as Element of the carrier of X ; [x,y] in [: the carrier of (HK (G,RK)), the carrier of (HK (G,RK)):] by ZFMISC_1:def_2; then A . (x,y) = vx \ vy by FUNCT_1:49; hence A . (x,y) = the InternalDiff of (HK (G,RK)) . (x,y) by Def12; ::_thesis: verum end; then ( 0. (HK (G,RK)) = 0. X & A = the InternalDiff of (HK (G,RK)) ) by BINOP_1:2; hence HK (G,RK) is SubAlgebra of X by BCIALG_1:def_10; ::_thesis: verum end; theorem :: BCIALG_6:57 for X being BCI-algebra for G being SubAlgebra of X for K being closed Ideal of X holds the carrier of G /\ K is closed Ideal of G proof let X be BCI-algebra; ::_thesis: for G being SubAlgebra of X for K being closed Ideal of X holds the carrier of G /\ K is closed Ideal of G let G be SubAlgebra of X; ::_thesis: for K being closed Ideal of X holds the carrier of G /\ K is closed Ideal of G let K be closed Ideal of X; ::_thesis: the carrier of G /\ K is closed Ideal of G set GK = the carrier of G /\ K; A1: for x, y being Element of G st x \ y in the carrier of G /\ K & y in the carrier of G /\ K holds x in the carrier of G /\ K proof let x, y be Element of G; ::_thesis: ( x \ y in the carrier of G /\ K & y in the carrier of G /\ K implies x in the carrier of G /\ K ) assume that A2: x \ y in the carrier of G /\ K and A3: y in the carrier of G /\ K ; ::_thesis: x in the carrier of G /\ K the carrier of G c= the carrier of X by BCIALG_1:def_10; then reconsider x1 = x, y1 = y as Element of X by TARSKI:def_3; x \ y in K by A2, XBOOLE_0:def_4; then A4: x1 \ y1 in K by Th34; y1 in K by A3, XBOOLE_0:def_4; then x in K by A4, BCIALG_1:def_18; hence x in the carrier of G /\ K by XBOOLE_0:def_4; ::_thesis: verum end; A5: 0. G = 0. X by BCIALG_1:def_10; then A6: 0. G in K by BCIALG_1:def_18; then A7: 0. G in the carrier of G /\ K by XBOOLE_0:def_4; for x being set st x in the carrier of G /\ K holds x in the carrier of G by XBOOLE_0:def_4; then the carrier of G /\ K is non empty Subset of G by A6, TARSKI:def_3, XBOOLE_0:def_4; then reconsider GK = the carrier of G /\ K as Ideal of G by A7, A1, BCIALG_1:def_18; for x being Element of GK holds x ` in GK proof let x be Element of GK; ::_thesis: x ` in GK A8: x in K by XBOOLE_0:def_4; then reconsider y = x as Element of X ; y ` in K by A8, BCIALG_1:def_19; then x ` in K by A5, Th34; hence x ` in GK by XBOOLE_0:def_4; ::_thesis: verum end; hence the carrier of G /\ K is closed Ideal of G by BCIALG_1:def_19; ::_thesis: verum end; theorem :: BCIALG_6:58 for X being BCI-algebra for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K for K1 being Ideal of HK (G,RK) for RK1 being I-congruence of HK (G,RK),K1 for I being Ideal of G for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic proof let X be BCI-algebra; ::_thesis: for G being SubAlgebra of X for K being closed Ideal of X for RK being I-congruence of X,K for K1 being Ideal of HK (G,RK) for RK1 being I-congruence of HK (G,RK),K1 for I being Ideal of G for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic let G be SubAlgebra of X; ::_thesis: for K being closed Ideal of X for RK being I-congruence of X,K for K1 being Ideal of HK (G,RK) for RK1 being I-congruence of HK (G,RK),K1 for I being Ideal of G for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic let K be closed Ideal of X; ::_thesis: for RK being I-congruence of X,K for K1 being Ideal of HK (G,RK) for RK1 being I-congruence of HK (G,RK),K1 for I being Ideal of G for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic let RK be I-congruence of X,K; ::_thesis: for K1 being Ideal of HK (G,RK) for RK1 being I-congruence of HK (G,RK),K1 for I being Ideal of G for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic let K1 be Ideal of HK (G,RK); ::_thesis: for RK1 being I-congruence of HK (G,RK),K1 for I being Ideal of G for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic let RK1 be I-congruence of HK (G,RK),K1; ::_thesis: for I being Ideal of G for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic let I be Ideal of G; ::_thesis: for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic let RI be I-congruence of G,I; ::_thesis: ( RK1 = RK & I = the carrier of G /\ K implies G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic ) assume that A1: RK1 = RK and A2: I = the carrier of G /\ K ; ::_thesis: G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic defpred S1[ Element of G, set ] means $2 = Class (RK1,$1); A3: the carrier of G c= the carrier of (HK (G,RK)) proof let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in the carrier of G or xx in the carrier of (HK (G,RK)) ) assume xx in the carrier of G ; ::_thesis: xx in the carrier of (HK (G,RK)) then reconsider x = xx as Element of G ; the carrier of G c= the carrier of X by BCIALG_1:def_10; then A4: x in the carrier of X by TARSKI:def_3; then Class (RK,x) in the carrier of (X ./. RK) by EQREL_1:def_3; then A5: Class (RK,x) in { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } ; [x,x] in RK by A4, EQREL_1:5; then x in Class (RK,x) by EQREL_1:18; hence xx in the carrier of (HK (G,RK)) by A5, TARSKI:def_4; ::_thesis: verum end; A6: for x being Element of G ex y being Element of ((HK (G,RK)) ./. RK1) st S1[x,y] proof let x be Element of G; ::_thesis: ex y being Element of ((HK (G,RK)) ./. RK1) st S1[x,y] set y = Class (RK1,x); x in the carrier of G ; then reconsider y = Class (RK1,x) as Element of ((HK (G,RK)) ./. RK1) by A3, EQREL_1:def_3; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider f being Function of G,((HK (G,RK)) ./. RK1) such that A7: for x being Element of G holds S1[x,f . x] from FUNCT_2:sch_3(A6); now__::_thesis:_for_a,_b_being_Element_of_G_holds_f_._(a_\_b)_=_(f_._a)_\_(f_._b) let a, b be Element of G; ::_thesis: f . (a \ b) = (f . a) \ (f . b) the carrier of G c= the carrier of X by BCIALG_1:def_10; then reconsider xa = a, xb = b as Element of X by TARSKI:def_3; ( a in the carrier of G & b in the carrier of G ) ; then reconsider Wa = Class (RK1,a), Wb = Class (RK1,b) as Element of Class RK1 by A3, EQREL_1:def_3; ( a in the carrier of G & b in the carrier of G ) ; then reconsider a1 = a, b1 = b as Element of (HK (G,RK)) by A3; ( Wa = f . a & Wb = f . b ) by A7; then A8: (f . a) \ (f . b) = Class (RK1,(a1 \ b1)) by BCIALG_2:def_17; HK (G,RK) is SubAlgebra of X by Th56; then xa \ xb = a1 \ b1 by Th34; then (f . a) \ (f . b) = Class (RK1,(a \ b)) by A8, Th34; hence f . (a \ b) = (f . a) \ (f . b) by A7; ::_thesis: verum end; then reconsider f = f as BCI-homomorphism of G,((HK (G,RK)) ./. RK1) by Def6; A9: Ker f = I proof set X9 = (HK (G,RK)) ./. RK1; thus Ker f c= I :: according to XBOOLE_0:def_10 ::_thesis: I c= Ker f proof let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in Ker f or h in I ) assume h in Ker f ; ::_thesis: h in I then consider x being Element of G such that A10: h = x and A11: f . x = 0. ((HK (G,RK)) ./. RK1) ; ( x in the carrier of G & the carrier of G c= the carrier of X ) by BCIALG_1:def_10; then reconsider x = x as Element of X ; Class (RK,x) = Class (RK,(0. X)) by A1, A7, A11; then 0. X in Class (RK,x) by EQREL_1:23; then [x,(0. X)] in RK by EQREL_1:18; then A12: x \ (0. X) in K by BCIALG_2:def_12; x in K by A12, BCIALG_1:def_18; hence h in I by A2, A10, XBOOLE_0:def_4; ::_thesis: verum end; let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in I or h in Ker f ) assume A13: h in I ; ::_thesis: h in Ker f then reconsider x = h as Element of X by A2; h in K by A2, A13, XBOOLE_0:def_4; then ( x \ (0. X) in K & x ` in K ) by BCIALG_1:2, BCIALG_1:def_19; then [x,(0. X)] in RK by BCIALG_2:def_12; then 0. X in Class (RK,x) by EQREL_1:18; then Class (RK1,h) = Class (RK1,(0. X)) by A1, EQREL_1:23; then f . h = 0. ((HK (G,RK)) ./. RK1) by A7, A13; hence h in Ker f by A13; ::_thesis: verum end; now__::_thesis:_for_y_being_set_holds_ (_y_in_rng_f_iff_y_in_the_carrier_of_((HK_(G,RK))_./._RK1)_) let y be set ; ::_thesis: ( y in rng f iff y in the carrier of ((HK (G,RK)) ./. RK1) ) ( y in the carrier of ((HK (G,RK)) ./. RK1) implies y in rng f ) proof assume y in the carrier of ((HK (G,RK)) ./. RK1) ; ::_thesis: y in rng f then consider x being set such that A14: x in the carrier of (HK (G,RK)) and A15: y = Class (RK1,x) by EQREL_1:def_3; consider a being Element of G such that A16: x in Class (RK,a) by A14, Lm5; ( a in the carrier of G & the carrier of G c= the carrier of X ) by BCIALG_1:def_10; then y = Class (RK1,a) by A1, A15, A16, EQREL_1:23; then A17: y = f . a by A7; dom f = the carrier of G by FUNCT_2:def_1; hence y in rng f by A17, FUNCT_1:def_3; ::_thesis: verum end; hence ( y in rng f iff y in the carrier of ((HK (G,RK)) ./. RK1) ) ; ::_thesis: verum end; then rng f = the carrier of ((HK (G,RK)) ./. RK1) by TARSKI:1; then f is onto by FUNCT_2:def_3; hence G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic by A9, Th54; ::_thesis: verum end;