:: 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;