:: BCIALG_2 semantic presentation
begin
definition
let X be BCI-algebra;
let x, y be Element of X;
let n be Element of NAT ;
func(x,y) to_power n -> Element of X means :Def1: :: BCIALG_2:def 1
ex f being Function of NAT, the carrier of X st
( it = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) );
existence
ex b1 being Element of X ex f being Function of NAT, the carrier of X st
( b1 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) )
proof
defpred S1[ set ] means for x, y being Element of X
for n being Element of NAT st n = $1 holds
ex u being Element of X ex f being Function of NAT, the carrier of X st
( u = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) );
now__::_thesis:_for_n_being_Element_of_NAT_st_(_for_x,_y_being_Element_of_X
for_k_being_Element_of_NAT_st_k_=_n_holds_
ex_u_being_Element_of_X_ex_f_being_Function_of_NAT,_the_carrier_of_X_st_
(_u_=_f_._k_&_f_._0_=_x_&_(_for_j_being_Element_of_NAT_st_j_<_k_holds_
f_._(j_+_1)_=_(f_._j)_\_y_)_)_)_holds_
for_x,_y_being_Element_of_X
for_k_being_Element_of_NAT_st_k_=_n_+_1_holds_
ex_z_being_Element_of_the_carrier_of_X_ex_f99_being_Function_of_NAT,_the_carrier_of_X_st_
(_z_=_f99_._(n_+_1)_&_f99_._0_=_x_&_(_for_j_being_Element_of_NAT_st_j_<_n_+_1_holds_
f99_._(j_+_1)_=_(f99_._j)_\_y_)_)
let n be Element of NAT ; ::_thesis: ( ( for x, y being Element of X
for k being Element of NAT st k = n holds
ex u being Element of X ex f being Function of NAT, the carrier of X st
( u = f . k & f . 0 = x & ( for j being Element of NAT st j < k holds
f . (j + 1) = (f . j) \ y ) ) ) implies for x, y being Element of X
for k being Element of NAT st k = n + 1 holds
ex z being Element of the carrier of X ex f99 being Function of NAT, the carrier of X st
( z = f99 . (n + 1) & f99 . 0 = x & ( for j being Element of NAT st j < n + 1 holds
f99 . (j + 1) = (f99 . j) \ y ) ) )
assume A1: for x, y being Element of X
for k being Element of NAT st k = n holds
ex u being Element of X ex f being Function of NAT, the carrier of X st
( u = f . k & f . 0 = x & ( for j being Element of NAT st j < k holds
f . (j + 1) = (f . j) \ y ) ) ; ::_thesis: for x, y being Element of X
for k being Element of NAT st k = n + 1 holds
ex z being Element of the carrier of X ex f99 being Function of NAT, the carrier of X st
( z = f99 . (n + 1) & f99 . 0 = x & ( for j being Element of NAT st j < n + 1 holds
f99 . (j + 1) = (f99 . j) \ y ) )
let x, y be Element of X; ::_thesis: for k being Element of NAT st k = n + 1 holds
ex z being Element of the carrier of X ex f99 being Function of NAT, the carrier of X st
( z = f99 . (n + 1) & f99 . 0 = x & ( for j being Element of NAT st j < n + 1 holds
f99 . (j + 1) = (f99 . j) \ y ) )
let k be Element of NAT ; ::_thesis: ( k = n + 1 implies ex z being Element of the carrier of X ex f99 being Function of NAT, the carrier of X st
( z = f99 . (n + 1) & f99 . 0 = x & ( for j being Element of NAT st j < n + 1 holds
f99 . (j + 1) = (f99 . j) \ y ) ) )
consider u being Element of X, f being Function of NAT, the carrier of X such that
u = f . n and
A2: f . 0 = x and
A3: for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y by A1;
defpred S2[ set , set ] means for j being Element of NAT st $1 = j holds
( ( j < n + 1 implies $2 = f . $1 ) & ( n + 1 <= j implies $2 = (f . n) \ y ) );
assume k = n + 1 ; ::_thesis: ex z being Element of the carrier of X ex f99 being Function of NAT, the carrier of X st
( z = f99 . (n + 1) & f99 . 0 = x & ( for j being Element of NAT st j < n + 1 holds
f99 . (j + 1) = (f99 . j) \ y ) )
A4: for k being Element of NAT ex v being Element of X st S2[k,v]
proof
let k be Element of NAT ; ::_thesis: ex v being Element of X st S2[k,v]
reconsider i = k as Element of NAT ;
A5: now__::_thesis:_(_n_+_1_<=_i_implies_ex_v_being_Element_of_the_carrier_of_X_st_
for_j_being_Element_of_NAT_st_k_=_j_holds_
(_(_j_<_n_+_1_implies_v_=_f_._k_)_&_(_n_+_1_<=_j_implies_v_=_(f_._n)_\_y_)_)_)
assume A6: n + 1 <= i ; ::_thesis: ex v being Element of the carrier of X st
for j being Element of NAT st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies v = (f . n) \ y ) )
take v = (f . n) \ y; ::_thesis: for j being Element of NAT st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies v = (f . n) \ y ) )
let j be Element of NAT ; ::_thesis: ( k = j implies ( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies v = (f . n) \ y ) ) )
assume k = j ; ::_thesis: ( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies v = (f . n) \ y ) )
hence ( j < n + 1 implies v = f . k ) by A6; ::_thesis: ( n + 1 <= j implies v = (f . n) \ y )
assume n + 1 <= j ; ::_thesis: v = (f . n) \ y
thus v = (f . n) \ y ; ::_thesis: verum
end;
now__::_thesis:_(_i_<_n_+_1_implies_ex_v_being_Element_of_the_carrier_of_X_st_
for_j_being_Element_of_NAT_st_k_=_j_holds_
(_(_j_<_n_+_1_implies_v_=_f_._k_)_&_(_n_+_1_<=_j_implies_v_=_(f_._n)_\_y_)_)_)
assume A7: i < n + 1 ; ::_thesis: ex v being Element of the carrier of X st
for j being Element of NAT st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies v = (f . n) \ y ) )
take v = f . k; ::_thesis: for j being Element of NAT st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies v = (f . n) \ y ) )
let j be Element of NAT ; ::_thesis: ( k = j implies ( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies v = (f . n) \ y ) ) )
assume A8: k = j ; ::_thesis: ( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies v = (f . n) \ y ) )
thus ( j < n + 1 implies v = f . k ) ; ::_thesis: ( n + 1 <= j implies v = (f . n) \ y )
thus ( n + 1 <= j implies v = (f . n) \ y ) by A7, A8; ::_thesis: verum
end;
hence ex v being Element of X st S2[k,v] by A5; ::_thesis: verum
end;
consider f9 being Function of NAT, the carrier of X such that
A9: for k being Element of NAT holds S2[k,f9 . k] from FUNCT_2:sch_3(A4);
take z = f9 . (n + 1); ::_thesis: ex f99 being Function of NAT, the carrier of X st
( z = f99 . (n + 1) & f99 . 0 = x & ( for j being Element of NAT st j < n + 1 holds
f99 . (j + 1) = (f99 . j) \ y ) )
take f99 = f9; ::_thesis: ( z = f99 . (n + 1) & f99 . 0 = x & ( for j being Element of NAT st j < n + 1 holds
f99 . (j + 1) = (f99 . j) \ y ) )
thus z = f99 . (n + 1) ; ::_thesis: ( f99 . 0 = x & ( for j being Element of NAT st j < n + 1 holds
f99 . (j + 1) = (f99 . j) \ y ) )
0 < n + 1 by NAT_1:5;
hence f99 . 0 = x by A2, A9; ::_thesis: for j being Element of NAT st j < n + 1 holds
f99 . (j + 1) = (f99 . j) \ y
let j be Element of NAT ; ::_thesis: ( j < n + 1 implies f99 . (j + 1) = (f99 . j) \ y )
A10: now__::_thesis:_(_j_<_n_implies_f99_._(j_+_1)_=_(f99_._j)_\_y_)
assume A11: j < n ; ::_thesis: f99 . (j + 1) = (f99 . j) \ y
then ( f . (j + 1) = (f . j) \ y & j < n + 1 ) by A3, NAT_1:13;
then A12: f . (j + 1) = (f9 . j) \ y by A9;
j + 1 < n + 1 by A11, XREAL_1:6;
hence f99 . (j + 1) = (f99 . j) \ y by A9, A12; ::_thesis: verum
end;
A13: n < n + 1 by NAT_1:13;
A14: now__::_thesis:_(_j_=_n_implies_f99_._(j_+_1)_=_(f99_._j)_\_y_)
assume A15: j = n ; ::_thesis: f99 . (j + 1) = (f99 . j) \ y
then f99 . (j + 1) = (f . j) \ y by A9;
hence f99 . (j + 1) = (f99 . j) \ y by A13, A9, A15; ::_thesis: verum
end;
assume j < n + 1 ; ::_thesis: f99 . (j + 1) = (f99 . j) \ y
then j <= n by NAT_1:13;
hence f99 . (j + 1) = (f99 . j) \ y by A10, A14, XXREAL_0:1; ::_thesis: verum
end;
then A16: for n being Element of NAT st S1[n] holds
S1[n + 1] ;
now__::_thesis:_for_x,_y_being_Element_of_X
for_n_being_Element_of_NAT_st_n_=_0_holds_
ex_u_being_Element_of_the_carrier_of_X_ex_f9_being_Function_of_NAT,_the_carrier_of_X_st_
(_u_=_f9_._n_&_f9_._0_=_x_&_(_for_j_being_Element_of_NAT_st_j_<_n_holds_
f9_._(j_+_1)_=_(f9_._j)_\_y_)_)
let x, y be Element of X; ::_thesis: for n being Element of NAT st n = 0 holds
ex u being Element of the carrier of X ex f9 being Function of NAT, the carrier of X st
( u = f9 . n & f9 . 0 = x & ( for j being Element of NAT st j < n holds
f9 . (j + 1) = (f9 . j) \ y ) )
let n be Element of NAT ; ::_thesis: ( n = 0 implies ex u being Element of the carrier of X ex f9 being Function of NAT, the carrier of X st
( u = f9 . n & f9 . 0 = x & ( for j being Element of NAT st j < n holds
f9 . (j + 1) = (f9 . j) \ y ) ) )
assume A17: n = 0 ; ::_thesis: ex u being Element of the carrier of X ex f9 being Function of NAT, the carrier of X st
( u = f9 . n & f9 . 0 = x & ( for j being Element of NAT st j < n holds
f9 . (j + 1) = (f9 . j) \ y ) )
reconsider f = NAT --> x as Function of NAT, the carrier of X ;
take u = f . n; ::_thesis: ex f9 being Function of NAT, the carrier of X st
( u = f9 . n & f9 . 0 = x & ( for j being Element of NAT st j < n holds
f9 . (j + 1) = (f9 . j) \ y ) )
take f9 = f; ::_thesis: ( u = f9 . n & f9 . 0 = x & ( for j being Element of NAT st j < n holds
f9 . (j + 1) = (f9 . j) \ y ) )
thus ( u = f9 . n & f9 . 0 = x ) by FUNCOP_1:7; ::_thesis: for j being Element of NAT st j < n holds
f9 . (j + 1) = (f9 . j) \ y
thus for j being Element of NAT st j < n holds
f9 . (j + 1) = (f9 . j) \ y by A17, NAT_1:3; ::_thesis: verum
end;
then A18: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A18, A16);
hence ex b1 being Element of X ex f being Function of NAT, the carrier of X st
( b1 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of X st ex f being Function of NAT, the carrier of X st
( b1 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) & ex f being Function of NAT, the carrier of X st
( b2 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) holds
b1 = b2
proof
let v1, v2 be Element of X; ::_thesis: ( ex f being Function of NAT, the carrier of X st
( v1 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) & ex f being Function of NAT, the carrier of X st
( v2 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) implies v1 = v2 )
given f being Function of NAT, the carrier of X such that A19: v1 = f . n and
A20: f . 0 = x and
A21: for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ; ::_thesis: ( for f being Function of NAT, the carrier of X holds
( not v2 = f . n or not f . 0 = x or ex j being Element of NAT st
( j < n & not f . (j + 1) = (f . j) \ y ) ) or v1 = v2 )
given f9 being Function of NAT, the carrier of X such that A22: v2 = f9 . n and
A23: f9 . 0 = x and
A24: for j being Element of NAT st j < n holds
f9 . (j + 1) = (f9 . j) \ y ; ::_thesis: v1 = v2
defpred S1[ Nat] means ( $1 <= n implies f . $1 = f9 . $1 );
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_n_implies_f_._k_=_f9_._k_)_&_k_+_1_<=_n_holds_
f_._(k_+_1)_=_f9_._(k_+_1)
let k be Element of NAT ; ::_thesis: ( ( k <= n implies f . k = f9 . k ) & k + 1 <= n implies f . (k + 1) = f9 . (k + 1) )
assume A25: ( k <= n implies f . k = f9 . k ) ; ::_thesis: ( k + 1 <= n implies f . (k + 1) = f9 . (k + 1) )
assume k + 1 <= n ; ::_thesis: f . (k + 1) = f9 . (k + 1)
then A26: k < n by NAT_1:13;
then f . (k + 1) = (f . k) \ y by A21;
hence f . (k + 1) = f9 . (k + 1) by A24, A25, A26; ::_thesis: verum
end;
then A27: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A28: S1[ 0 ] by A20, A23;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A28, A27);
hence v1 = v2 by A19, A22; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines to_power BCIALG_2:def_1_:_
for X being BCI-algebra
for x, y being Element of X
for n being Element of NAT
for b5 being Element of X holds
( b5 = (x,y) to_power n iff ex f being Function of NAT, the carrier of X st
( b5 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) );
theorem Th1: :: BCIALG_2:1
for X being BCI-algebra
for x, y being Element of X holds (x,y) to_power 0 = x
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X holds (x,y) to_power 0 = x
let x, y be Element of X; ::_thesis: (x,y) to_power 0 = x
ex f being Function of NAT, the carrier of X st
( (x,y) to_power 0 = f . 0 & f . 0 = x & ( for j being Element of NAT st j < 0 holds
f . (j + 1) = (f . j) \ y ) ) by Def1;
hence (x,y) to_power 0 = x ; ::_thesis: verum
end;
theorem Th2: :: BCIALG_2:2
for X being BCI-algebra
for x, y being Element of X holds (x,y) to_power 1 = x \ y
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X holds (x,y) to_power 1 = x \ y
let x, y be Element of X; ::_thesis: (x,y) to_power 1 = x \ y
consider f being Function of NAT, the carrier of X such that
A1: (x,y) to_power 1 = f . 1 and
A2: ( f . 0 = x & ( for j being Element of NAT st j < 1 holds
f . (j + 1) = (f . j) \ y ) ) by Def1;
f . (0 + 1) = x \ y by A2, NAT_1:3;
hence (x,y) to_power 1 = x \ y by A1; ::_thesis: verum
end;
theorem :: BCIALG_2:3
for X being BCI-algebra
for x, y being Element of X holds (x,y) to_power 2 = (x \ y) \ y
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X holds (x,y) to_power 2 = (x \ y) \ y
let x, y be Element of X; ::_thesis: (x,y) to_power 2 = (x \ y) \ y
consider f being Function of NAT, the carrier of X such that
A1: ( (x,y) to_power 2 = f . 2 & f . 0 = x ) and
A2: for j being Element of NAT st j < 2 holds
f . (j + 1) = (f . j) \ y by Def1;
1 < 1 + 1 by NAT_1:13;
then f . (1 + 1) = (f . (0 + 1)) \ y by A2;
hence (x,y) to_power 2 = (x \ y) \ y by A1, A2, NAT_1:3; ::_thesis: verum
end;
theorem Th4: :: BCIALG_2:4
for X being BCI-algebra
for x, y being Element of X
for n being Element of NAT holds (x,y) to_power (n + 1) = ((x,y) to_power n) \ y
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X
for n being Element of NAT holds (x,y) to_power (n + 1) = ((x,y) to_power n) \ y
let x, y be Element of X; ::_thesis: for n being Element of NAT holds (x,y) to_power (n + 1) = ((x,y) to_power n) \ y
let n be Element of NAT ; ::_thesis: (x,y) to_power (n + 1) = ((x,y) to_power n) \ y
A1: n < n + 1 by NAT_1:3, XREAL_1:29;
consider g being Function of NAT, the carrier of X such that
A2: (x,y) to_power n = g . n and
A3: g . 0 = x and
A4: for j being Element of NAT st j < n holds
g . (j + 1) = (g . j) \ y by Def1;
consider f being Function of NAT, the carrier of X such that
A5: (x,y) to_power (n + 1) = f . (n + 1) and
A6: f . 0 = x and
A7: for j being Element of NAT st j < n + 1 holds
f . (j + 1) = (f . j) \ y by Def1;
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
f . m = g . m;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_
f_._m_=_g_._m_)_holds_
for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_
f_._m_=_g_._m
let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds
f . m = g . m ) implies for m being Element of NAT st m = k + 1 & m <= n holds
f . m = g . m )
assume A8: for m being Element of NAT st m = k & m <= n holds
f . m = g . m ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds
f . m = g . m
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies f . m = g . m )
assume that
A9: m = k + 1 and
A10: m <= n ; ::_thesis: f . m = g . m
k + 1 <= n + 1 by A9, A10, NAT_1:13;
then k < n + 1 by NAT_1:13;
then A11: f . (k + 1) = (f . k) \ y by A7;
A12: k < n by A9, A10, NAT_1:13;
then g . (k + 1) = (g . k) \ y by A4;
hence f . m = g . m by A8, A9, A12, A11; ::_thesis: verum
end;
then A13: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A14: S1[ 0 ] by A6, A3;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A14, A13);
then f . n = g . n ;
hence (x,y) to_power (n + 1) = ((x,y) to_power n) \ y by A5, A7, A2, A1; ::_thesis: verum
end;
theorem Th5: :: BCIALG_2:5
for X being BCI-algebra
for x being Element of X
for n being Element of NAT holds (x,(0. X)) to_power (n + 1) = x
proof
let X be BCI-algebra; ::_thesis: for x being Element of X
for n being Element of NAT holds (x,(0. X)) to_power (n + 1) = x
let x be Element of X; ::_thesis: for n being Element of NAT holds (x,(0. X)) to_power (n + 1) = x
let n be Element of NAT ; ::_thesis: (x,(0. X)) to_power (n + 1) = x
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(x,(0. X)) to_power (m + 1) = x;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_
(x,(0._X))_to_power_(m_+_1)_=_x_)_holds_
for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_
(x,(0._X))_to_power_(m_+_1)_=_x
let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds
(x,(0. X)) to_power (m + 1) = x ) implies for m being Element of NAT st m = k + 1 & m <= n holds
(x,(0. X)) to_power (m + 1) = x )
assume A1: for m being Element of NAT st m = k & m <= n holds
(x,(0. X)) to_power (m + 1) = x ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds
(x,(0. X)) to_power (m + 1) = x
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (x,(0. X)) to_power (m + 1) = x )
assume that
A2: m = k + 1 and
A3: m <= n ; ::_thesis: (x,(0. X)) to_power (m + 1) = x
(x,(0. X)) to_power (m + 1) = ((x,(0. X)) to_power (k + 1)) \ (0. X) by A2, Th4;
then A4: (x,(0. X)) to_power (m + 1) = (x,(0. X)) to_power (k + 1) by BCIALG_1:2;
k <= n by A2, A3, NAT_1:13;
hence (x,(0. X)) to_power (m + 1) = x by A1, A4; ::_thesis: verum
end;
then A5: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
(x,(0. X)) to_power (0 + 1) = x \ (0. X) by Th2;
then A6: S1[ 0 ] by BCIALG_1:2;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A5);
hence (x,(0. X)) to_power (n + 1) = x ; ::_thesis: verum
end;
theorem Th6: :: BCIALG_2:6
for X being BCI-algebra
for n being Element of NAT holds ((0. X),(0. X)) to_power n = 0. X
proof
let X be BCI-algebra; ::_thesis: for n being Element of NAT holds ((0. X),(0. X)) to_power n = 0. X
let n be Element of NAT ; ::_thesis: ((0. X),(0. X)) to_power n = 0. X
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
((0. X),(0. X)) to_power m = 0. X;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1] by Th5;
A2: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1);
hence ((0. X),(0. X)) to_power n = 0. X ; ::_thesis: verum
end;
theorem Th7: :: BCIALG_2:7
for X being BCI-algebra
for x, y, z being Element of X
for n being Element of NAT holds ((x,y) to_power n) \ z = ((x \ z),y) to_power n
proof
let X be BCI-algebra; ::_thesis: for x, y, z being Element of X
for n being Element of NAT holds ((x,y) to_power n) \ z = ((x \ z),y) to_power n
let x, y, z be Element of X; ::_thesis: for n being Element of NAT holds ((x,y) to_power n) \ z = ((x \ z),y) to_power n
let n be Element of NAT ; ::_thesis: ((x,y) to_power n) \ z = ((x \ z),y) to_power n
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power m;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_
((x,y)_to_power_m)_\_z_=_((x_\_z),y)_to_power_m_)_holds_
for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_
((x,y)_to_power_m)_\_z_=_((x_\_z),y)_to_power_(k_+_1)
let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power m ) implies for m being Element of NAT st m = k + 1 & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1) )
assume A1: for m being Element of NAT st m = k & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power m ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1)
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies ((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1) )
assume that
A2: m = k + 1 and
A3: m <= n ; ::_thesis: ((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1)
((x,y) to_power m) \ z = (((x,y) to_power k) \ y) \ z by A2, Th4;
then A4: ((x,y) to_power m) \ z = (((x,y) to_power k) \ z) \ y by BCIALG_1:7;
k <= n by A2, A3, NAT_1:13;
then ((x,y) to_power m) \ z = (((x \ z),y) to_power k) \ y by A1, A4;
hence ((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1) by Th4; ::_thesis: verum
end;
then A5: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
((x,y) to_power 0) \ z = x \ z by Th1;
then A6: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A5);
hence ((x,y) to_power n) \ z = ((x \ z),y) to_power n ; ::_thesis: verum
end;
theorem :: BCIALG_2:8
for X being BCI-algebra
for x, y being Element of X
for n being Element of NAT holds (x,(x \ (x \ y))) to_power n = (x,y) to_power n
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X
for n being Element of NAT holds (x,(x \ (x \ y))) to_power n = (x,y) to_power n
let x, y be Element of X; ::_thesis: for n being Element of NAT holds (x,(x \ (x \ y))) to_power n = (x,y) to_power n
let n be Element of NAT ; ::_thesis: (x,(x \ (x \ y))) to_power n = (x,y) to_power n
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(x,(x \ (x \ y))) to_power m = (x,y) to_power m;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_
(x,(x_\_(x_\_y)))_to_power_m_=_(x,y)_to_power_m_)_holds_
for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_
(x,(x_\_(x_\_y)))_to_power_(k_+_1)_=_(x,y)_to_power_(k_+_1)
let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds
(x,(x \ (x \ y))) to_power m = (x,y) to_power m ) implies for m being Element of NAT st m = k + 1 & m <= n holds
(x,(x \ (x \ y))) to_power (k + 1) = (x,y) to_power (k + 1) )
assume A1: for m being Element of NAT st m = k & m <= n holds
(x,(x \ (x \ y))) to_power m = (x,y) to_power m ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds
(x,(x \ (x \ y))) to_power (k + 1) = (x,y) to_power (k + 1)
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (x,(x \ (x \ y))) to_power (k + 1) = (x,y) to_power (k + 1) )
A2: (x,(x \ (x \ y))) to_power (k + 1) = ((x,(x \ (x \ y))) to_power k) \ (x \ (x \ y)) by Th4;
assume ( m = k + 1 & m <= n ) ; ::_thesis: (x,(x \ (x \ y))) to_power (k + 1) = (x,y) to_power (k + 1)
then k <= n by NAT_1:13;
hence (x,(x \ (x \ y))) to_power (k + 1) = ((x,y) to_power k) \ (x \ (x \ y)) by A1, A2
.= ((x \ (x \ (x \ y))),y) to_power k by Th7
.= ((x \ y),y) to_power k by BCIALG_1:8
.= ((x,y) to_power k) \ y by Th7
.= (x,y) to_power (k + 1) by Th4 ;
::_thesis: verum
end;
then A3: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
(x,(x \ (x \ y))) to_power 0 = x by Th1;
then A4: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3);
hence (x,(x \ (x \ y))) to_power n = (x,y) to_power n ; ::_thesis: verum
end;
theorem Th9: :: BCIALG_2:9
for X being BCI-algebra
for x being Element of X
for n being Element of NAT holds (((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n
proof
let X be BCI-algebra; ::_thesis: for x being Element of X
for n being Element of NAT holds (((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n
let x be Element of X; ::_thesis: for n being Element of NAT holds (((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n
let n be Element of NAT ; ::_thesis: (((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(((0. X),x) to_power m) ` = ((0. X),(x `)) to_power m;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_
(((0._X),x)_to_power_m)_`_=_((0._X),(x_`))_to_power_m_)_holds_
for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_
(((0._X),x)_to_power_(k_+_1))_`_=_((0._X),(x_`))_to_power_(k_+_1)
let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds
(((0. X),x) to_power m) ` = ((0. X),(x `)) to_power m ) implies for m being Element of NAT st m = k + 1 & m <= n holds
(((0. X),x) to_power (k + 1)) ` = ((0. X),(x `)) to_power (k + 1) )
assume A1: for m being Element of NAT st m = k & m <= n holds
(((0. X),x) to_power m) ` = ((0. X),(x `)) to_power m ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds
(((0. X),x) to_power (k + 1)) ` = ((0. X),(x `)) to_power (k + 1)
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (((0. X),x) to_power (k + 1)) ` = ((0. X),(x `)) to_power (k + 1) )
A2: (((0. X),x) to_power (k + 1)) ` = ((((0. X),x) to_power k) \ x) ` by Th4
.= ((((0. X),x) to_power k) `) \ (x `) by BCIALG_1:9 ;
assume ( m = k + 1 & m <= n ) ; ::_thesis: (((0. X),x) to_power (k + 1)) ` = ((0. X),(x `)) to_power (k + 1)
then k <= n by NAT_1:13;
hence (((0. X),x) to_power (k + 1)) ` = (((0. X),(x `)) to_power k) \ (x `) by A1, A2
.= ((0. X),(x `)) to_power (k + 1) by Th4 ;
::_thesis: verum
end;
then A3: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
(((0. X),x) to_power 0) ` = (0. X) ` by Th1;
then (((0. X),x) to_power 0) ` = 0. X by BCIALG_1:2;
then A4: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3);
hence (((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n ; ::_thesis: verum
end;
theorem Th10: :: BCIALG_2:10
for X being BCI-algebra
for x, y being Element of X
for n, m being Element of NAT holds (((x,y) to_power n),y) to_power m = (x,y) to_power (n + m)
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X
for n, m being Element of NAT holds (((x,y) to_power n),y) to_power m = (x,y) to_power (n + m)
let x, y be Element of X; ::_thesis: for n, m being Element of NAT holds (((x,y) to_power n),y) to_power m = (x,y) to_power (n + m)
let n, m be Element of NAT ; ::_thesis: (((x,y) to_power n),y) to_power m = (x,y) to_power (n + m)
defpred S1[ set ] means for m1 being Element of NAT st m1 = $1 & m1 <= n holds
(((x,y) to_power m1),y) to_power m = (x,y) to_power (m1 + m);
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m1_being_Element_of_NAT_st_m1_=_k_&_m1_<=_n_holds_
(((x,y)_to_power_m1),y)_to_power_m_=_(x,y)_to_power_(m1_+_m)_)_holds_
for_m1_being_Element_of_NAT_st_m1_=_k_+_1_&_m1_<=_n_holds_
(((x,y)_to_power_m1),y)_to_power_m_=_(x,y)_to_power_(m1_+_m)
let k be Element of NAT ; ::_thesis: ( ( for m1 being Element of NAT st m1 = k & m1 <= n holds
(((x,y) to_power m1),y) to_power m = (x,y) to_power (m1 + m) ) implies for m1 being Element of NAT st m1 = k + 1 & m1 <= n holds
(((x,y) to_power m1),y) to_power m = (x,y) to_power (m1 + m) )
assume A1: for m1 being Element of NAT st m1 = k & m1 <= n holds
(((x,y) to_power m1),y) to_power m = (x,y) to_power (m1 + m) ; ::_thesis: for m1 being Element of NAT st m1 = k + 1 & m1 <= n holds
(((x,y) to_power m1),y) to_power m = (x,y) to_power (m1 + m)
let m1 be Element of NAT ; ::_thesis: ( m1 = k + 1 & m1 <= n implies (((x,y) to_power m1),y) to_power m = (x,y) to_power (m1 + m) )
assume that
A2: m1 = k + 1 and
A3: m1 <= n ; ::_thesis: (((x,y) to_power m1),y) to_power m = (x,y) to_power (m1 + m)
k <= n by A2, A3, NAT_1:13;
then (((x,y) to_power k),y) to_power m = (x,y) to_power (k + m) by A1;
then ((((x,y) to_power k),y) to_power m) \ y = (x,y) to_power ((k + m) + 1) by Th4;
then ((((x,y) to_power k) \ y),y) to_power m = (x,y) to_power ((k + m) + 1) by Th7;
hence (((x,y) to_power m1),y) to_power m = (x,y) to_power (m1 + m) by A2, Th4; ::_thesis: verum
end;
then A4: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A5: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A4);
hence (((x,y) to_power n),y) to_power m = (x,y) to_power (n + m) ; ::_thesis: verum
end;
theorem :: BCIALG_2:11
for X being BCI-algebra
for x, y, z being Element of X
for n, m being Element of NAT holds (((x,y) to_power n),z) to_power m = (((x,z) to_power m),y) to_power n
proof
let X be BCI-algebra; ::_thesis: for x, y, z being Element of X
for n, m being Element of NAT holds (((x,y) to_power n),z) to_power m = (((x,z) to_power m),y) to_power n
let x, y, z be Element of X; ::_thesis: for n, m being Element of NAT holds (((x,y) to_power n),z) to_power m = (((x,z) to_power m),y) to_power n
let n, m be Element of NAT ; ::_thesis: (((x,y) to_power n),z) to_power m = (((x,z) to_power m),y) to_power n
defpred S1[ set ] means for m1 being Element of NAT st m1 = $1 & m1 <= n holds
(((x,y) to_power m1),z) to_power m = (((x,z) to_power m),y) to_power m1;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m1_being_Element_of_NAT_st_m1_=_k_&_m1_<=_n_holds_
(((x,y)_to_power_m1),z)_to_power_m_=_(((x,z)_to_power_m),y)_to_power_m1_)_holds_
for_m1_being_Element_of_NAT_st_m1_=_k_+_1_&_m1_<=_n_holds_
(((x,y)_to_power_(k_+_1)),z)_to_power_m_=_(((x,z)_to_power_m),y)_to_power_(k_+_1)
let k be Element of NAT ; ::_thesis: ( ( for m1 being Element of NAT st m1 = k & m1 <= n holds
(((x,y) to_power m1),z) to_power m = (((x,z) to_power m),y) to_power m1 ) implies for m1 being Element of NAT st m1 = k + 1 & m1 <= n holds
(((x,y) to_power (k + 1)),z) to_power m = (((x,z) to_power m),y) to_power (k + 1) )
assume A1: for m1 being Element of NAT st m1 = k & m1 <= n holds
(((x,y) to_power m1),z) to_power m = (((x,z) to_power m),y) to_power m1 ; ::_thesis: for m1 being Element of NAT st m1 = k + 1 & m1 <= n holds
(((x,y) to_power (k + 1)),z) to_power m = (((x,z) to_power m),y) to_power (k + 1)
let m1 be Element of NAT ; ::_thesis: ( m1 = k + 1 & m1 <= n implies (((x,y) to_power (k + 1)),z) to_power m = (((x,z) to_power m),y) to_power (k + 1) )
assume ( m1 = k + 1 & m1 <= n ) ; ::_thesis: (((x,y) to_power (k + 1)),z) to_power m = (((x,z) to_power m),y) to_power (k + 1)
then k <= n by NAT_1:13;
then ((((x,y) to_power k),z) to_power m) \ y = ((((x,z) to_power m),y) to_power k) \ y by A1
.= (((x,z) to_power m),y) to_power (k + 1) by Th4 ;
then (((x,z) to_power m),y) to_power (k + 1) = ((((x,y) to_power k) \ y),z) to_power m by Th7;
hence (((x,y) to_power (k + 1)),z) to_power m = (((x,z) to_power m),y) to_power (k + 1) by Th4; ::_thesis: verum
end;
then A2: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
(((x,y) to_power 0),z) to_power m = (x,z) to_power m by Th1;
then A3: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence (((x,y) to_power n),z) to_power m = (((x,z) to_power m),y) to_power n ; ::_thesis: verum
end;
theorem Th12: :: BCIALG_2:12
for X being BCI-algebra
for x being Element of X
for n being Element of NAT holds ((((0. X),x) to_power n) `) ` = ((0. X),x) to_power n
proof
let X be BCI-algebra; ::_thesis: for x being Element of X
for n being Element of NAT holds ((((0. X),x) to_power n) `) ` = ((0. X),x) to_power n
let x be Element of X; ::_thesis: for n being Element of NAT holds ((((0. X),x) to_power n) `) ` = ((0. X),x) to_power n
let n be Element of NAT ; ::_thesis: ((((0. X),x) to_power n) `) ` = ((0. X),x) to_power n
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
((((0. X),x) to_power m) `) ` = ((0. X),x) to_power m;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_
((((0._X),x)_to_power_m)_`)_`_=_((0._X),x)_to_power_m_)_holds_
for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_
((((0._X),x)_to_power_(k_+_1))_`)_`_=_((0._X),x)_to_power_(k_+_1)
let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds
((((0. X),x) to_power m) `) ` = ((0. X),x) to_power m ) implies for m being Element of NAT st m = k + 1 & m <= n holds
((((0. X),x) to_power (k + 1)) `) ` = ((0. X),x) to_power (k + 1) )
assume A1: for m being Element of NAT st m = k & m <= n holds
((((0. X),x) to_power m) `) ` = ((0. X),x) to_power m ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds
((((0. X),x) to_power (k + 1)) `) ` = ((0. X),x) to_power (k + 1)
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies ((((0. X),x) to_power (k + 1)) `) ` = ((0. X),x) to_power (k + 1) )
assume ( m = k + 1 & m <= n ) ; ::_thesis: ((((0. X),x) to_power (k + 1)) `) ` = ((0. X),x) to_power (k + 1)
then A2: k <= n by NAT_1:13;
((((0. X),x) to_power (k + 1)) `) ` = (((((0. X),x) to_power k) \ x) `) ` by Th4
.= (((((0. X),x) to_power k) `) \ (x `)) ` by BCIALG_1:9
.= (((((0. X),x) to_power k) `) `) \ ((x `) `) by BCIALG_1:9
.= (((0. X),x) to_power k) \ ((x `) `) by A1, A2
.= ((((x `) `) `),x) to_power k by Th7
.= ((x `),x) to_power k by BCIALG_1:8
.= (((0. X),x) to_power k) \ x by Th7 ;
hence ((((0. X),x) to_power (k + 1)) `) ` = ((0. X),x) to_power (k + 1) by Th4; ::_thesis: verum
end;
then A3: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
((((0. X),x) to_power 0) `) ` = ((0. X) `) ` by Th1
.= (0. X) ` by BCIALG_1:def_5
.= 0. X by BCIALG_1:def_5 ;
then A4: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3);
hence ((((0. X),x) to_power n) `) ` = ((0. X),x) to_power n ; ::_thesis: verum
end;
theorem Th13: :: BCIALG_2:13
for X being BCI-algebra
for x being Element of X
for n, m being Element of NAT holds ((0. X),x) to_power (n + m) = (((0. X),x) to_power n) \ ((((0. X),x) to_power m) `)
proof
let X be BCI-algebra; ::_thesis: for x being Element of X
for n, m being Element of NAT holds ((0. X),x) to_power (n + m) = (((0. X),x) to_power n) \ ((((0. X),x) to_power m) `)
let x be Element of X; ::_thesis: for n, m being Element of NAT holds ((0. X),x) to_power (n + m) = (((0. X),x) to_power n) \ ((((0. X),x) to_power m) `)
let n, m be Element of NAT ; ::_thesis: ((0. X),x) to_power (n + m) = (((0. X),x) to_power n) \ ((((0. X),x) to_power m) `)
defpred S1[ set ] means for j being Element of NAT st j = $1 & j <= n holds
((0. X),x) to_power (j + m) = (((0. X),x) to_power j) \ ((((0. X),x) to_power m) `);
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_j_being_Element_of_NAT_st_j_=_k_&_j_<=_n_holds_
((0._X),x)_to_power_(j_+_m)_=_(((0._X),x)_to_power_j)_\_((((0._X),x)_to_power_m)_`)_)_holds_
for_j_being_Element_of_NAT_st_j_=_k_+_1_&_j_<=_n_holds_
((0._X),x)_to_power_((k_+_1)_+_m)_=_(((0._X),x)_to_power_(k_+_1))_\_((((0._X),x)_to_power_m)_`)
let k be Element of NAT ; ::_thesis: ( ( for j being Element of NAT st j = k & j <= n holds
((0. X),x) to_power (j + m) = (((0. X),x) to_power j) \ ((((0. X),x) to_power m) `) ) implies for j being Element of NAT st j = k + 1 & j <= n holds
((0. X),x) to_power ((k + 1) + m) = (((0. X),x) to_power (k + 1)) \ ((((0. X),x) to_power m) `) )
assume A1: for j being Element of NAT st j = k & j <= n holds
((0. X),x) to_power (j + m) = (((0. X),x) to_power j) \ ((((0. X),x) to_power m) `) ; ::_thesis: for j being Element of NAT st j = k + 1 & j <= n holds
((0. X),x) to_power ((k + 1) + m) = (((0. X),x) to_power (k + 1)) \ ((((0. X),x) to_power m) `)
let j be Element of NAT ; ::_thesis: ( j = k + 1 & j <= n implies ((0. X),x) to_power ((k + 1) + m) = (((0. X),x) to_power (k + 1)) \ ((((0. X),x) to_power m) `) )
assume ( j = k + 1 & j <= n ) ; ::_thesis: ((0. X),x) to_power ((k + 1) + m) = (((0. X),x) to_power (k + 1)) \ ((((0. X),x) to_power m) `)
then A2: k <= n by NAT_1:13;
((0. X),x) to_power ((k + m) + 1) = (((0. X),x) to_power (k + m)) \ x by Th4
.= ((((0. X),x) to_power k) \ ((((0. X),x) to_power m) `)) \ x by A1, A2
.= ((((0. X),x) to_power k) \ x) \ ((((0. X),x) to_power m) `) by BCIALG_1:7 ;
hence ((0. X),x) to_power ((k + 1) + m) = (((0. X),x) to_power (k + 1)) \ ((((0. X),x) to_power m) `) by Th4; ::_thesis: verum
end;
then A3: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
((0. X),x) to_power (0 + m) = ((((0. X),x) to_power m) `) ` by Th12;
then A4: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3);
hence ((0. X),x) to_power (n + m) = (((0. X),x) to_power n) \ ((((0. X),x) to_power m) `) ; ::_thesis: verum
end;
theorem :: BCIALG_2:14
for X being BCI-algebra
for x being Element of X
for m, n being Element of NAT holds (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n)
proof
let X be BCI-algebra; ::_thesis: for x being Element of X
for m, n being Element of NAT holds (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n)
let x be Element of X; ::_thesis: for m, n being Element of NAT holds (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n)
let m, n be Element of NAT ; ::_thesis: (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n)
(((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) \ ((((0. X),x) to_power n) `)) ` by Th13
.= ((((0. X),x) to_power m) `) \ (((((0. X),x) to_power n) `) `) by BCIALG_1:9 ;
hence (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n) by Th12; ::_thesis: verum
end;
theorem :: BCIALG_2:15
for X being BCI-algebra
for x being Element of X
for m, n being Element of NAT holds (((0. X),(((0. X),x) to_power m)) to_power n) ` = ((0. X),x) to_power (m * n)
proof
let X be BCI-algebra; ::_thesis: for x being Element of X
for m, n being Element of NAT holds (((0. X),(((0. X),x) to_power m)) to_power n) ` = ((0. X),x) to_power (m * n)
let x be Element of X; ::_thesis: for m, n being Element of NAT holds (((0. X),(((0. X),x) to_power m)) to_power n) ` = ((0. X),x) to_power (m * n)
let m, n be Element of NAT ; ::_thesis: (((0. X),(((0. X),x) to_power m)) to_power n) ` = ((0. X),x) to_power (m * n)
defpred S1[ set ] means for j being Element of NAT st j = $1 & j <= n holds
(((0. X),(((0. X),x) to_power m)) to_power j) ` = ((0. X),x) to_power (m * j);
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_j_being_Element_of_NAT_st_j_=_k_&_j_<=_n_holds_
(((0._X),(((0._X),x)_to_power_m))_to_power_j)_`_=_((0._X),x)_to_power_(m_*_j)_)_holds_
for_j_being_Element_of_NAT_st_j_=_k_+_1_&_j_<=_n_holds_
(((0._X),(((0._X),x)_to_power_m))_to_power_(k_+_1))_`_=_((0._X),x)_to_power_(m_*_(k_+_1))
let k be Element of NAT ; ::_thesis: ( ( for j being Element of NAT st j = k & j <= n holds
(((0. X),(((0. X),x) to_power m)) to_power j) ` = ((0. X),x) to_power (m * j) ) implies for j being Element of NAT st j = k + 1 & j <= n holds
(((0. X),(((0. X),x) to_power m)) to_power (k + 1)) ` = ((0. X),x) to_power (m * (k + 1)) )
assume A1: for j being Element of NAT st j = k & j <= n holds
(((0. X),(((0. X),x) to_power m)) to_power j) ` = ((0. X),x) to_power (m * j) ; ::_thesis: for j being Element of NAT st j = k + 1 & j <= n holds
(((0. X),(((0. X),x) to_power m)) to_power (k + 1)) ` = ((0. X),x) to_power (m * (k + 1))
let j be Element of NAT ; ::_thesis: ( j = k + 1 & j <= n implies (((0. X),(((0. X),x) to_power m)) to_power (k + 1)) ` = ((0. X),x) to_power (m * (k + 1)) )
assume ( j = k + 1 & j <= n ) ; ::_thesis: (((0. X),(((0. X),x) to_power m)) to_power (k + 1)) ` = ((0. X),x) to_power (m * (k + 1))
then A2: k <= n by NAT_1:13;
(((0. X),(((0. X),x) to_power m)) to_power (k + 1)) ` = ((((0. X),(((0. X),x) to_power m)) to_power k) \ (((0. X),x) to_power m)) ` by Th4
.= ((((0. X),(((0. X),x) to_power m)) to_power k) `) \ ((((0. X),x) to_power m) `) by BCIALG_1:9
.= (((0. X),x) to_power (m * k)) \ ((((0. X),x) to_power m) `) by A1, A2
.= ((0. X),x) to_power ((m * k) + m) by Th13 ;
hence (((0. X),(((0. X),x) to_power m)) to_power (k + 1)) ` = ((0. X),x) to_power (m * (k + 1)) ; ::_thesis: verum
end;
then A3: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
(((0. X),(((0. X),x) to_power m)) to_power 0) ` = (0. X) ` by Th1
.= 0. X by BCIALG_1:def_5 ;
then A4: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3);
hence (((0. X),(((0. X),x) to_power m)) to_power n) ` = ((0. X),x) to_power (m * n) ; ::_thesis: verum
end;
theorem :: BCIALG_2:16
for X being BCI-algebra
for x being Element of X
for m, n being Element of NAT st ((0. X),x) to_power m = 0. X holds
((0. X),x) to_power (m * n) = 0. X
proof
let X be BCI-algebra; ::_thesis: for x being Element of X
for m, n being Element of NAT st ((0. X),x) to_power m = 0. X holds
((0. X),x) to_power (m * n) = 0. X
let x be Element of X; ::_thesis: for m, n being Element of NAT st ((0. X),x) to_power m = 0. X holds
((0. X),x) to_power (m * n) = 0. X
let m, n be Element of NAT ; ::_thesis: ( ((0. X),x) to_power m = 0. X implies ((0. X),x) to_power (m * n) = 0. X )
defpred S1[ set ] means for j being Element of NAT st j = $1 & j <= n holds
((0. X),x) to_power (m * j) = 0. X;
assume A1: ((0. X),x) to_power m = 0. X ; ::_thesis: ((0. X),x) to_power (m * n) = 0. X
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_j_being_Element_of_NAT_st_j_=_k_&_j_<=_n_holds_
((0._X),x)_to_power_(m_*_j)_=_0._X_)_holds_
for_j_being_Element_of_NAT_st_j_=_k_+_1_&_j_<=_n_holds_
((0._X),x)_to_power_(m_*_(k_+_1))_=_0._X
let k be Element of NAT ; ::_thesis: ( ( for j being Element of NAT st j = k & j <= n holds
((0. X),x) to_power (m * j) = 0. X ) implies for j being Element of NAT st j = k + 1 & j <= n holds
((0. X),x) to_power (m * (k + 1)) = 0. X )
assume A2: for j being Element of NAT st j = k & j <= n holds
((0. X),x) to_power (m * j) = 0. X ; ::_thesis: for j being Element of NAT st j = k + 1 & j <= n holds
((0. X),x) to_power (m * (k + 1)) = 0. X
let j be Element of NAT ; ::_thesis: ( j = k + 1 & j <= n implies ((0. X),x) to_power (m * (k + 1)) = 0. X )
assume ( j = k + 1 & j <= n ) ; ::_thesis: ((0. X),x) to_power (m * (k + 1)) = 0. X
then A3: k <= n by NAT_1:13;
((0. X),x) to_power (m * (k + 1)) = ((0. X),x) to_power ((m * k) + m)
.= ((((0. X),x) to_power (m * k)),x) to_power m by Th10
.= ((0. X),x) to_power m by A2, A3 ;
hence ((0. X),x) to_power (m * (k + 1)) = 0. X by A1; ::_thesis: verum
end;
then A4: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A5: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A4);
hence ((0. X),x) to_power (m * n) = 0. X ; ::_thesis: verum
end;
theorem :: BCIALG_2:17
for X being BCI-algebra
for x, y being Element of X
for n being Element of NAT st x \ y = x holds
(x,y) to_power n = x
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X
for n being Element of NAT st x \ y = x holds
(x,y) to_power n = x
let x, y be Element of X; ::_thesis: for n being Element of NAT st x \ y = x holds
(x,y) to_power n = x
let n be Element of NAT ; ::_thesis: ( x \ y = x implies (x,y) to_power n = x )
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(x,y) to_power m = x;
assume A1: x \ y = x ; ::_thesis: (x,y) to_power n = x
now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_
(x,y)_to_power_m_=_x_)_holds_
for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_
(x,y)_to_power_(k_+_1)_=_x
let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds
(x,y) to_power m = x ) implies for m being Element of NAT st m = k + 1 & m <= n holds
(x,y) to_power (k + 1) = x )
assume A2: for m being Element of NAT st m = k & m <= n holds
(x,y) to_power m = x ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds
(x,y) to_power (k + 1) = x
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (x,y) to_power (k + 1) = x )
A3: (x,y) to_power (k + 1) = ((x,y) to_power k) \ y by Th4;
assume ( m = k + 1 & m <= n ) ; ::_thesis: (x,y) to_power (k + 1) = x
then k <= n by NAT_1:13;
hence (x,y) to_power (k + 1) = x by A1, A2, A3; ::_thesis: verum
end;
then A4: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A5: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A4);
hence (x,y) to_power n = x ; ::_thesis: verum
end;
theorem :: BCIALG_2:18
for X being BCI-algebra
for x, y being Element of X
for n being Element of NAT holds ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X
for n being Element of NAT holds ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)
let x, y be Element of X; ::_thesis: for n being Element of NAT holds ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)
let n be Element of NAT ; ::_thesis: ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
((0. X),(x \ y)) to_power m = (((0. X),x) to_power m) \ (((0. X),y) to_power m);
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: for m being Element of NAT st m = k & m <= n holds
((0. X),(x \ y)) to_power m = (((0. X),x) to_power m) \ (((0. X),y) to_power m) ; ::_thesis: S1[k + 1]
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies ((0. X),(x \ y)) to_power m = (((0. X),x) to_power m) \ (((0. X),y) to_power m) )
assume that
A3: m = k + 1 and
A4: m <= n ; ::_thesis: ((0. X),(x \ y)) to_power m = (((0. X),x) to_power m) \ (((0. X),y) to_power m)
k <= n by A3, A4, NAT_1:13;
then ((0. X),(x \ y)) to_power k = (((0. X),x) to_power k) \ (((0. X),y) to_power k) by A2;
then ((0. X),(x \ y)) to_power (k + 1) = ((((0. X),x) to_power k) \ (((0. X),y) to_power k)) \ (x \ y) by Th4
.= ((((0. X),x) to_power k) \ (x \ y)) \ (((0. X),y) to_power k) by BCIALG_1:7
.= ((((x \ y) `),x) to_power k) \ (((0. X),y) to_power k) by Th7
.= ((((x `) \ (y `)),x) to_power k) \ (((0. X),y) to_power k) by BCIALG_1:9
.= ((((x `),x) to_power k) \ (y `)) \ (((0. X),y) to_power k) by Th7
.= ((((x `),x) to_power k) \ (((0. X),y) to_power k)) \ (y `) by BCIALG_1:7
.= (((((0. X),x) to_power k) \ x) \ (((0. X),y) to_power k)) \ (y `) by Th7 ;
then ((0. X),(x \ y)) to_power (k + 1) = ((((0. X),x) to_power (k + 1)) \ (((0. X),y) to_power k)) \ (y `) by Th4
.= ((((0. X),x) to_power (k + 1)) \ (y `)) \ (((0. X),y) to_power k) by BCIALG_1:7
.= ((((y `) `),x) to_power (k + 1)) \ (((0. X),y) to_power k) by Th7
.= ((((y `) `) \ (((0. X),y) to_power k)),x) to_power (k + 1) by Th7
.= ((((((0. X),y) to_power k) `) \ (y `)),x) to_power (k + 1) by BCIALG_1:7
.= ((((((0. X),y) to_power k) \ y) `),x) to_power (k + 1) by BCIALG_1:9
.= (((((0. X),y) to_power (k + 1)) `),x) to_power (k + 1) by Th4 ;
hence ((0. X),(x \ y)) to_power m = (((0. X),x) to_power m) \ (((0. X),y) to_power m) by A3, Th7; ::_thesis: verum
end;
(0. X) ` = 0. X by BCIALG_1:def_5;
then ((0. X),(x \ y)) to_power 0 = (0. X) ` by Th1;
then ((0. X),(x \ y)) to_power 0 = (((0. X),x) to_power 0) \ (0. X) by Th1;
then A5: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A1);
hence ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n) ; ::_thesis: verum
end;
theorem :: BCIALG_2:19
for X being BCI-algebra
for x, y, z being Element of X
for n being Element of NAT st x <= y holds
(x,z) to_power n <= (y,z) to_power n
proof
let X be BCI-algebra; ::_thesis: for x, y, z being Element of X
for n being Element of NAT st x <= y holds
(x,z) to_power n <= (y,z) to_power n
let x, y, z be Element of X; ::_thesis: for n being Element of NAT st x <= y holds
(x,z) to_power n <= (y,z) to_power n
let n be Element of NAT ; ::_thesis: ( x <= y implies (x,z) to_power n <= (y,z) to_power n )
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(x,z) to_power m <= (y,z) to_power m;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: for m being Element of NAT st m = k & m <= n holds
(x,z) to_power m <= (y,z) to_power m ; ::_thesis: S1[k + 1]
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (x,z) to_power m <= (y,z) to_power m )
assume that
A3: m = k + 1 and
A4: m <= n ; ::_thesis: (x,z) to_power m <= (y,z) to_power m
k <= n by A3, A4, NAT_1:13;
then (x,z) to_power k <= (y,z) to_power k by A2;
then ((x,z) to_power k) \ z <= ((y,z) to_power k) \ z by BCIALG_1:5;
then (x,z) to_power (k + 1) <= ((y,z) to_power k) \ z by Th4;
hence (x,z) to_power m <= (y,z) to_power m by A3, Th4; ::_thesis: verum
end;
assume x <= y ; ::_thesis: (x,z) to_power n <= (y,z) to_power n
then (x,z) to_power 0 <= y by Th1;
then A5: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A1);
hence (x,z) to_power n <= (y,z) to_power n ; ::_thesis: verum
end;
theorem :: BCIALG_2:20
for X being BCI-algebra
for x, y, z being Element of X
for n being Element of NAT st x <= y holds
(z,y) to_power n <= (z,x) to_power n
proof
let X be BCI-algebra; ::_thesis: for x, y, z being Element of X
for n being Element of NAT st x <= y holds
(z,y) to_power n <= (z,x) to_power n
let x, y, z be Element of X; ::_thesis: for n being Element of NAT st x <= y holds
(z,y) to_power n <= (z,x) to_power n
let n be Element of NAT ; ::_thesis: ( x <= y implies (z,y) to_power n <= (z,x) to_power n )
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(z,y) to_power m <= (z,x) to_power m;
assume A1: x <= y ; ::_thesis: (z,y) to_power n <= (z,x) to_power n
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: for m being Element of NAT st m = k & m <= n holds
(z,y) to_power m <= (z,x) to_power m ; ::_thesis: S1[k + 1]
((z,x) to_power k) \ y <= ((z,x) to_power k) \ x by A1, BCIALG_1:5;
then ((z,x) to_power k) \ y <= (z,x) to_power (k + 1) by Th4;
then A4: (((z,x) to_power k) \ y) \ ((z,x) to_power (k + 1)) = 0. X by BCIALG_1:def_11;
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (z,y) to_power m <= (z,x) to_power m )
assume that
A5: m = k + 1 and
A6: m <= n ; ::_thesis: (z,y) to_power m <= (z,x) to_power m
k <= n by A5, A6, NAT_1:13;
then (z,y) to_power k <= (z,x) to_power k by A3;
then ((z,y) to_power k) \ y <= ((z,x) to_power k) \ y by BCIALG_1:5;
then (z,y) to_power (k + 1) <= ((z,x) to_power k) \ y by Th4;
then ((z,y) to_power (k + 1)) \ (((z,x) to_power k) \ y) = 0. X by BCIALG_1:def_11;
then ((z,y) to_power (k + 1)) \ ((z,x) to_power (k + 1)) = 0. X by A4, BCIALG_1:3;
hence (z,y) to_power m <= (z,x) to_power m by A5, BCIALG_1:def_11; ::_thesis: verum
end;
z \ z = 0. X by BCIALG_1:def_5;
then z <= z by BCIALG_1:def_11;
then (z,y) to_power 0 <= z by Th1;
then A7: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A2);
hence (z,y) to_power n <= (z,x) to_power n ; ::_thesis: verum
end;
theorem :: BCIALG_2:21
for X being BCI-algebra
for x, z, y being Element of X
for n being Element of NAT holds ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y
proof
let X be BCI-algebra; ::_thesis: for x, z, y being Element of X
for n being Element of NAT holds ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y
let x, z, y be Element of X; ::_thesis: for n being Element of NAT holds ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y
let n be Element of NAT ; ::_thesis: ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
((x,z) to_power m) \ ((y,z) to_power m) <= x \ y;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: for m being Element of NAT st m = k & m <= n holds
((x,z) to_power m) \ ((y,z) to_power m) <= x \ y ; ::_thesis: S1[k + 1]
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies ((x,z) to_power m) \ ((y,z) to_power m) <= x \ y )
assume that
A3: m = k + 1 and
A4: m <= n ; ::_thesis: ((x,z) to_power m) \ ((y,z) to_power m) <= x \ y
k <= n by A3, A4, NAT_1:13;
then ((x,z) to_power k) \ ((y,z) to_power k) <= x \ y by A2;
then (((x,z) to_power k) \ ((y,z) to_power k)) \ (x \ y) = 0. X by BCIALG_1:def_11;
then (((x,z) to_power k) \ (x \ y)) \ ((y,z) to_power k) = 0. X by BCIALG_1:7;
then ((((x,z) to_power k) \ (x \ y)) \ z) \ (((y,z) to_power k) \ z) = 0. X by BCIALG_1:4;
then ((((x,z) to_power k) \ z) \ (x \ y)) \ (((y,z) to_power k) \ z) = 0. X by BCIALG_1:7;
then (((x,z) to_power (k + 1)) \ (x \ y)) \ (((y,z) to_power k) \ z) = 0. X by Th4;
then (((x,z) to_power (k + 1)) \ (x \ y)) \ ((y,z) to_power (k + 1)) = 0. X by Th4;
then (((x,z) to_power (k + 1)) \ ((y,z) to_power (k + 1))) \ (x \ y) = 0. X by BCIALG_1:7;
hence ((x,z) to_power m) \ ((y,z) to_power m) <= x \ y by A3, BCIALG_1:def_11; ::_thesis: verum
end;
(x \ y) \ (x \ y) = 0. X by BCIALG_1:def_5;
then x \ y <= x \ y by BCIALG_1:def_11;
then ((x,z) to_power 0) \ y <= x \ y by Th1;
then A5: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A1);
hence ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y ; ::_thesis: verum
end;
theorem :: BCIALG_2:22
for X being BCI-algebra
for x, y being Element of X
for n being Element of NAT holds (((x,(x \ y)) to_power n),(y \ x)) to_power n <= x
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X
for n being Element of NAT holds (((x,(x \ y)) to_power n),(y \ x)) to_power n <= x
let x, y be Element of X; ::_thesis: for n being Element of NAT holds (((x,(x \ y)) to_power n),(y \ x)) to_power n <= x
let n be Element of NAT ; ::_thesis: (((x,(x \ y)) to_power n),(y \ x)) to_power n <= x
defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds
(((x,(x \ y)) to_power m),(y \ x)) to_power m <= x;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: for m being Element of NAT st m = k & m <= n holds
(((x,(x \ y)) to_power m),(y \ x)) to_power m <= x ; ::_thesis: S1[k + 1]
let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (((x,(x \ y)) to_power m),(y \ x)) to_power m <= x )
assume that
A3: m = k + 1 and
A4: m <= n ; ::_thesis: (((x,(x \ y)) to_power m),(y \ x)) to_power m <= x
k <= n by A3, A4, NAT_1:13;
then (((x,(x \ y)) to_power k),(y \ x)) to_power k <= x by A2;
then ((((x,(x \ y)) to_power k),(y \ x)) to_power k) \ x = 0. X by BCIALG_1:def_11;
then (((((x,(x \ y)) to_power k) \ x),(y \ x)) to_power k) \ (y \ x) = (y \ x) ` by Th7;
then (((((x,(x \ y)) to_power k) \ x),(y \ x)) to_power (k + 1)) \ (x \ y) = ((y \ x) `) \ (x \ y) by Th4;
then (((((x,(x \ y)) to_power k) \ x) \ (x \ y)),(y \ x)) to_power (k + 1) = ((y \ x) `) \ (x \ y) by Th7;
then (((((x,(x \ y)) to_power k) \ (x \ y)) \ x),(y \ x)) to_power (k + 1) = ((y \ x) `) \ (x \ y) by BCIALG_1:7;
then ((((x,(x \ y)) to_power (k + 1)) \ x),(y \ x)) to_power (k + 1) = ((y \ x) `) \ (x \ y) by Th4;
then ((((x,(x \ y)) to_power (k + 1)) \ x),(y \ x)) to_power (k + 1) = ((y \ y) \ (y \ x)) \ (x \ y) by BCIALG_1:def_5;
then ((((x,(x \ y)) to_power (k + 1)) \ x),(y \ x)) to_power (k + 1) = 0. X by BCIALG_1:1;
then ((((x,(x \ y)) to_power (k + 1)),(y \ x)) to_power (k + 1)) \ x = 0. X by Th7;
hence (((x,(x \ y)) to_power m),(y \ x)) to_power m <= x by A3, BCIALG_1:def_11; ::_thesis: verum
end;
x \ x = 0. X by BCIALG_1:def_5;
then x <= x by BCIALG_1:def_11;
then (x,(y \ x)) to_power 0 <= x by Th1;
then A5: S1[ 0 ] by Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A1);
hence (((x,(x \ y)) to_power n),(y \ x)) to_power n <= x ; ::_thesis: verum
end;
notation
let X be BCI-algebra;
let a be Element of X;
synonym minimal a for atom ;
end;
definition
let X be BCI-algebra;
let a be Element of X;
attra is positive means :Def2: :: BCIALG_2:def 2
0. X <= a;
attra is least means :: BCIALG_2:def 3
for x being Element of X holds a <= x;
attra is maximal means :Def4: :: BCIALG_2:def 4
for x being Element of X st a <= x holds
x = a;
attra is greatest means :Def5: :: BCIALG_2:def 5
for x being Element of X holds x <= a;
end;
:: deftheorem Def2 defines positive BCIALG_2:def_2_:_
for X being BCI-algebra
for a being Element of X holds
( a is positive iff 0. X <= a );
:: deftheorem defines least BCIALG_2:def_3_:_
for X being BCI-algebra
for a being Element of X holds
( a is least iff for x being Element of X holds a <= x );
:: deftheorem Def4 defines maximal BCIALG_2:def_4_:_
for X being BCI-algebra
for a being Element of X holds
( a is maximal iff for x being Element of X st a <= x holds
x = a );
:: deftheorem Def5 defines greatest BCIALG_2:def_5_:_
for X being BCI-algebra
for a being Element of X holds
( a is greatest iff for x being Element of X holds x <= a );
Lm1: for X being BCI-algebra
for a being Element of X holds
( a is minimal iff for x being Element of X st x <= a holds
x = a )
proof
let X be BCI-algebra; ::_thesis: for a being Element of X holds
( a is minimal iff for x being Element of X st x <= a holds
x = a )
let a be Element of X; ::_thesis: ( a is minimal iff for x being Element of X st x <= a holds
x = a )
thus ( a is minimal implies for x being Element of X st x <= a holds
x = a ) ::_thesis: ( ( for x being Element of X st x <= a holds
x = a ) implies a is minimal )
proof
assume A1: a is minimal ; ::_thesis: for x being Element of X st x <= a holds
x = a
let x be Element of X; ::_thesis: ( x <= a implies x = a )
assume x <= a ; ::_thesis: x = a
then x \ a = 0. X by BCIALG_1:def_11;
hence x = a by A1, BCIALG_1:def_14; ::_thesis: verum
end;
assume A2: for x being Element of X st x <= a holds
x = a ; ::_thesis: a is minimal
now__::_thesis:_for_y_being_Element_of_X_st_y_\_a_=_0._X_holds_
y_=_a
let y be Element of X; ::_thesis: ( y \ a = 0. X implies y = a )
assume y \ a = 0. X ; ::_thesis: y = a
then y <= a by BCIALG_1:def_11;
hence y = a by A2; ::_thesis: verum
end;
hence a is minimal by BCIALG_1:def_14; ::_thesis: verum
end;
Lm2: for X being BCI-algebra holds 0. X is positive
proof
let X be BCI-algebra; ::_thesis: 0. X is positive
(0. X) ` = 0. X by BCIALG_1:2;
then 0. X <= 0. X by BCIALG_1:def_11;
hence 0. X is positive by Def2; ::_thesis: verum
end;
registration
let X be BCI-algebra;
cluster positive for Element of the carrier of X;
existence
ex b1 being Element of X st b1 is positive
proof
take 0. X ; ::_thesis: 0. X is positive
thus 0. X is positive by Lm2; ::_thesis: verum
end;
end;
Lm3: for X being BCI-algebra holds 0. X is minimal
proof
let X be BCI-algebra; ::_thesis: 0. X is minimal
for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X by BCIALG_1:2;
hence 0. X is minimal by BCIALG_1:def_14; ::_thesis: verum
end;
registration
let X be BCI-algebra;
cluster 0. X -> minimal positive ;
coherence
( 0. X is positive & 0. X is minimal ) by Lm2, Lm3;
end;
theorem :: BCIALG_2:23
for X being BCI-algebra
for a being Element of X holds
( a is minimal iff for x being Element of X holds a \ x = (x `) \ (a `) )
proof
let X be BCI-algebra; ::_thesis: for a being Element of X holds
( a is minimal iff for x being Element of X holds a \ x = (x `) \ (a `) )
let a be Element of X; ::_thesis: ( a is minimal iff for x being Element of X holds a \ x = (x `) \ (a `) )
thus ( a is minimal implies for x being Element of X holds a \ x = (x `) \ (a `) ) ::_thesis: ( ( for x being Element of X holds a \ x = (x `) \ (a `) ) implies a is minimal )
proof
assume A1: a is minimal ; ::_thesis: for x being Element of X holds a \ x = (x `) \ (a `)
let x be Element of X; ::_thesis: a \ x = (x `) \ (a `)
(x \ (x \ a)) \ a = 0. X by BCIALG_1:1;
then x \ (x \ a) <= a by BCIALG_1:def_11;
then A2: (a \ x) \ ((x `) \ (a `)) = ((x \ (x \ a)) \ x) \ ((x `) \ (a `)) by A1, Lm1
.= ((x \ x) \ (x \ a)) \ ((x `) \ (a `)) by BCIALG_1:7
.= ((x \ a) `) \ ((x `) \ (a `)) by BCIALG_1:def_5
.= ((x \ a) `) \ ((x \ a) `) by BCIALG_1:9
.= 0. X by BCIALG_1:def_5 ;
((x `) \ (a `)) \ (a \ x) = 0. X by BCIALG_1:1;
hence a \ x = (x `) \ (a `) by A2, BCIALG_1:def_7; ::_thesis: verum
end;
thus ( ( for x being Element of X holds a \ x = (x `) \ (a `) ) implies a is minimal ) ::_thesis: verum
proof
assume A3: for x being Element of X holds a \ x = (x `) \ (a `) ; ::_thesis: a is minimal
now__::_thesis:_for_x_being_Element_of_X_st_x_<=_a_holds_
a_=_x
let x be Element of X; ::_thesis: ( x <= a implies a = x )
assume x <= a ; ::_thesis: a = x
then A4: x \ a = 0. X by BCIALG_1:def_11;
a \ x = (x `) \ (a `) by A3;
then a \ x = (0. X) ` by A4, BCIALG_1:9;
then a \ x = 0. X by BCIALG_1:def_5;
hence a = x by A4, BCIALG_1:def_7; ::_thesis: verum
end;
hence a is minimal by Lm1; ::_thesis: verum
end;
end;
theorem :: BCIALG_2:24
for X being BCI-algebra
for x being Element of X holds
( x ` is minimal iff for y being Element of X st y <= x holds
x ` = y ` )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x ` is minimal iff for y being Element of X st y <= x holds
x ` = y ` )
let x be Element of X; ::_thesis: ( x ` is minimal iff for y being Element of X st y <= x holds
x ` = y ` )
thus ( x ` is minimal implies for y being Element of X st y <= x holds
x ` = y ` ) ::_thesis: ( ( for y being Element of X st y <= x holds
x ` = y ` ) implies x ` is minimal )
proof
assume A1: x ` is minimal ; ::_thesis: for y being Element of X st y <= x holds
x ` = y `
let y be Element of X; ::_thesis: ( y <= x implies x ` = y ` )
assume y <= x ; ::_thesis: x ` = y `
then y \ x = 0. X by BCIALG_1:def_11;
then (y \ x) ` = 0. X by BCIALG_1:def_5;
then (y `) \ (x `) = 0. X by BCIALG_1:9;
then y ` <= x ` by BCIALG_1:def_11;
hence x ` = y ` by A1, Lm1; ::_thesis: verum
end;
thus ( ( for y being Element of X st y <= x holds
x ` = y ` ) implies x ` is minimal ) ::_thesis: verum
proof
assume A2: for y being Element of X st y <= x holds
x ` = y ` ; ::_thesis: x ` is minimal
now__::_thesis:_for_xx_being_Element_of_X_st_xx_<=_x_`_holds_
xx_=_x_`
let xx be Element of X; ::_thesis: ( xx <= x ` implies xx = x ` )
assume xx <= x ` ; ::_thesis: xx = x `
then A3: xx \ (x `) = 0. X by BCIALG_1:def_11;
then (xx \ (x `)) ` = 0. X by BCIALG_1:def_5;
then (xx `) \ ((x `) `) = 0. X by BCIALG_1:9;
then ((xx `) \ ((x `) `)) ` = 0. X by BCIALG_1:def_5;
then ((xx `) `) \ (((x `) `) `) = 0. X by BCIALG_1:9;
then ((xx `) `) \ (x `) = 0. X by BCIALG_1:8;
then ((xx `) \ x) ` = 0. X by BCIALG_1:9;
then ((x `) \ xx) ` = 0. X by BCIALG_1:7;
then (xx \ xx) \ ((x `) \ xx) = 0. X by BCIALG_1:def_5;
then (xx \ (x `)) ` = 0. X by BCIALG_1:def_3;
then (xx `) \ ((x `) `) = 0. X by BCIALG_1:9;
then ((xx `) \ x) \ (((x `) `) \ x) = 0. X by BCIALG_1:4;
then ((xx `) \ x) \ (0. X) = 0. X by BCIALG_1:1;
then (xx `) \ x = 0. X by BCIALG_1:2;
then xx ` <= x by BCIALG_1:def_11;
then (xx `) ` = x ` by A2;
then 0. X = (x `) \ xx by BCIALG_1:1;
hence xx = x ` by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence x ` is minimal by Lm1; ::_thesis: verum
end;
end;
theorem :: BCIALG_2:25
for X being BCI-algebra
for x being Element of X holds
( x ` is minimal iff for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x ` is minimal iff for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) )
let x be Element of X; ::_thesis: ( x ` is minimal iff for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) )
thus ( x ` is minimal implies for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ) ::_thesis: ( ( for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ) implies x ` is minimal )
proof
assume A1: x ` is minimal ; ::_thesis: for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `)
let y, z be Element of X; ::_thesis: (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `)
((y `) \ (x \ y)) \ (x `) = 0. X by BCIALG_1:def_3;
then A2: (y `) \ (x \ y) <= x ` by BCIALG_1:def_11;
(((x \ z) \ (y \ z)) `) ` = (((x \ z) `) \ ((y \ z) `)) ` by BCIALG_1:9
.= (((x `) \ (z `)) \ ((y \ z) `)) ` by BCIALG_1:9 ;
then (((x \ z) \ (y \ z)) `) ` = ((((y `) \ (x \ y)) \ (z `)) \ ((y \ z) `)) ` by A1, A2, Lm1
.= ((((y `) \ (z `)) \ (x \ y)) \ ((y \ z) `)) ` by BCIALG_1:7
.= ((((y \ z) `) \ (x \ y)) \ ((y \ z) `)) ` by BCIALG_1:9
.= ((((y \ z) `) \ ((y \ z) `)) \ (x \ y)) ` by BCIALG_1:7
.= ((x \ y) `) ` by BCIALG_1:def_5
.= ((x `) \ (y `)) ` by BCIALG_1:9
.= (((y `) `) \ x) ` by BCIALG_1:7
.= (((y `) `) `) \ (x `) by BCIALG_1:9
.= (y `) \ (x `) by BCIALG_1:8 ;
hence (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ; ::_thesis: verum
end;
thus ( ( for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ) implies x ` is minimal ) ::_thesis: verum
proof
assume A3: for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ; ::_thesis: x ` is minimal
now__::_thesis:_for_x1_being_Element_of_X_st_x1_<=_x_`_holds_
x1_=_x_`
let x1 be Element of X; ::_thesis: ( x1 <= x ` implies x1 = x ` )
assume x1 <= x ` ; ::_thesis: x1 = x `
then A4: x1 \ (x `) = 0. X by BCIALG_1:def_11;
then ((x1 `) \ (x `)) \ ((x1 `) \ x1) = 0. X by BCIALG_1:4;
then ((((x \ (0. X)) \ (x1 \ (0. X))) `) `) \ ((x1 `) \ x1) = 0. X by A3;
then (((x1 `) \ x1) `) \ (((x \ (0. X)) \ (x1 \ (0. X))) `) = 0. X by BCIALG_1:7;
then (((x1 `) \ x1) `) \ ((x \ (x1 \ (0. X))) `) = 0. X by BCIALG_1:2;
then (((x1 `) \ x1) `) \ ((x \ x1) `) = 0. X by BCIALG_1:2;
then (((x1 `) `) \ (x1 `)) \ ((x \ x1) `) = 0. X by BCIALG_1:9;
then (((x1 `) `) \ (x1 `)) \ ((x `) \ (x1 `)) = 0. X by BCIALG_1:9;
then (((x1 `) `) \ (x `)) ` = 0. X by BCIALG_1:def_3;
then (((x1 `) `) `) \ ((x `) `) = 0. X by BCIALG_1:9;
then (x1 `) \ ((x `) `) = 0. X by BCIALG_1:8;
then (((x `) `) `) \ x1 = 0. X by BCIALG_1:7;
then (x `) \ x1 = 0. X by BCIALG_1:8;
hence x1 = x ` by A4, BCIALG_1:def_7; ::_thesis: verum
end;
hence x ` is minimal by Lm1; ::_thesis: verum
end;
end;
theorem :: BCIALG_2:26
for X being BCI-algebra st 0. X is maximal holds
for a being Element of X holds a is minimal
proof
let X be BCI-algebra; ::_thesis: ( 0. X is maximal implies for a being Element of X holds a is minimal )
assume A1: 0. X is maximal ; ::_thesis: for a being Element of X holds a is minimal
let a be Element of X; ::_thesis: a is minimal
now__::_thesis:_for_x_being_Element_of_X_st_x_<=_a_holds_
x_=_a
let x be Element of X; ::_thesis: ( x <= a implies x = a )
assume x <= a ; ::_thesis: x = a
then A2: x \ a = 0. X by BCIALG_1:def_11;
then (a \ x) ` = 0. X by BCIALG_1:6;
then 0. X <= a \ x by BCIALG_1:def_11;
then 0. X = a \ x by A1, Def4;
hence x = a by A2, BCIALG_1:def_7; ::_thesis: verum
end;
hence a is minimal by Lm1; ::_thesis: verum
end;
theorem :: BCIALG_2:27
for X being BCI-algebra st ex x being Element of X st x is greatest holds
for a being Element of X holds a is positive
proof
let X be BCI-algebra; ::_thesis: ( ex x being Element of X st x is greatest implies for a being Element of X holds a is positive )
given x being Element of X such that A1: x is greatest ; ::_thesis: for a being Element of X holds a is positive
let a be Element of X; ::_thesis: a is positive
a <= x by A1, Def5;
then a \ x = 0. X by BCIALG_1:def_11;
then A2: (a \ x) ` = 0. X by BCIALG_1:def_5;
0. X <= x by A1, Def5;
then x ` = 0. X by BCIALG_1:def_11;
then (a `) \ (0. X) = 0. X by A2, BCIALG_1:9;
then a ` = 0. X by BCIALG_1:2;
then 0. X <= a by BCIALG_1:def_11;
hence a is positive by Def2; ::_thesis: verum
end;
theorem Th28: :: BCIALG_2:28
for X being BCI-algebra
for x being Element of X holds x \ ((x `) `) is positive Element of X
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds x \ ((x `) `) is positive Element of X
let x be Element of X; ::_thesis: x \ ((x `) `) is positive Element of X
(x \ ((x `) `)) ` = (x `) \ (((x `) `) `) by BCIALG_1:9
.= (x `) \ (x `) by BCIALG_1:8
.= 0. X by BCIALG_1:def_5 ;
then 0. X <= x \ ((x `) `) by BCIALG_1:def_11;
hence x \ ((x `) `) is positive Element of X by Def2; ::_thesis: verum
end;
theorem :: BCIALG_2:29
for X being BCI-algebra
for a being Element of X holds
( a is minimal iff (a `) ` = a )
proof
let X be BCI-algebra; ::_thesis: for a being Element of X holds
( a is minimal iff (a `) ` = a )
let a be Element of X; ::_thesis: ( a is minimal iff (a `) ` = a )
thus ( a is minimal implies (a `) ` = a ) ::_thesis: ( (a `) ` = a implies a is minimal )
proof
((a `) `) \ a = 0. X by BCIALG_1:1;
then A1: (a `) ` <= a by BCIALG_1:def_11;
assume a is minimal ; ::_thesis: (a `) ` = a
hence (a `) ` = a by A1, Lm1; ::_thesis: verum
end;
assume A2: (a `) ` = a ; ::_thesis: a is minimal
now__::_thesis:_for_x_being_Element_of_X_st_x_<=_a_holds_
x_=_a
let x be Element of X; ::_thesis: ( x <= a implies x = a )
assume x <= a ; ::_thesis: x = a
then A3: x \ a = 0. X by BCIALG_1:def_11;
a \ x = (x `) \ (a `) by A2, BCIALG_1:7;
then a \ x = (0. X) ` by A3, BCIALG_1:9;
then a \ x = 0. X by BCIALG_1:def_5;
hence x = a by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence a is minimal by Lm1; ::_thesis: verum
end;
theorem Th30: :: BCIALG_2:30
for X being BCI-algebra
for a being Element of X holds
( a is minimal iff ex x being Element of X st a = x ` )
proof
let X be BCI-algebra; ::_thesis: for a being Element of X holds
( a is minimal iff ex x being Element of X st a = x ` )
let a be Element of X; ::_thesis: ( a is minimal iff ex x being Element of X st a = x ` )
thus ( a is minimal implies ex x being Element of X st a = x ` ) ::_thesis: ( ex x being Element of X st a = x ` implies a is minimal )
proof
assume A1: a is minimal ; ::_thesis: ex x being Element of X st a = x `
take x = a ` ; ::_thesis: a = x `
(x `) \ a = 0. X by BCIALG_1:1;
then x ` <= a by BCIALG_1:def_11;
hence a = x ` by A1, Lm1; ::_thesis: verum
end;
given x being Element of X such that A2: a = x ` ; ::_thesis: a is minimal
now__::_thesis:_for_y_being_Element_of_X_st_y_<=_a_holds_
a_=_y
let y be Element of X; ::_thesis: ( y <= a implies a = y )
assume y <= a ; ::_thesis: a = y
then A3: y \ a = 0. X by BCIALG_1:def_11;
then a \ y = ((y \ (x `)) \ y) \ x by A2, BCIALG_1:7;
then a \ y = ((y \ y) \ (x `)) \ x by BCIALG_1:7;
then a \ y = ((x `) `) \ x by BCIALG_1:def_5;
then a \ y = 0. X by BCIALG_1:1;
hence a = y by A3, BCIALG_1:def_7; ::_thesis: verum
end;
hence a is minimal by Lm1; ::_thesis: verum
end;
definition
let X be BCI-algebra;
let x be Element of X;
attrx is nilpotent means :Def6: :: BCIALG_2:def 6
ex k being non empty Element of NAT st ((0. X),x) to_power k = 0. X;
end;
:: deftheorem Def6 defines nilpotent BCIALG_2:def_6_:_
for X being BCI-algebra
for x being Element of X holds
( x is nilpotent iff ex k being non empty Element of NAT st ((0. X),x) to_power k = 0. X );
definition
let X be BCI-algebra;
attrX is nilpotent means :: BCIALG_2:def 7
for x being Element of X holds x is nilpotent ;
end;
:: deftheorem defines nilpotent BCIALG_2:def_7_:_
for X being BCI-algebra holds
( X is nilpotent iff for x being Element of X holds x is nilpotent );
definition
let X be BCI-algebra;
let x be Element of X;
assume A1: x is nilpotent ;
func ord x -> non empty Element of NAT means :Def8: :: BCIALG_2:def 8
( ((0. X),x) to_power it = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
it <= m ) );
existence
ex b1 being non empty Element of NAT st
( ((0. X),x) to_power b1 = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
b1 <= m ) )
proof
defpred S1[ Nat] means ex w being Element of NAT st
( w = $1 & ((0. X),x) to_power w = 0. X & w <> 0 );
ex k being non empty Element of NAT st ((0. X),x) to_power k = 0. X by A1, Def6;
then A2: ex n being Nat st S1[n] ;
consider k being Nat such that
A3: S1[k] and
A4: for n being Nat st S1[n] holds
k <= n from NAT_1:sch_5(A2);
reconsider k = k as non empty Element of NAT by A3;
take k ; ::_thesis: ( ((0. X),x) to_power k = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
k <= m ) )
thus ( ((0. X),x) to_power k = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
k <= m ) ) by A3, A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty Element of NAT st ((0. X),x) to_power b1 = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
b1 <= m ) & ((0. X),x) to_power b2 = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
b2 <= m ) holds
b1 = b2
proof
let n1, n2 be non empty Element of NAT ; ::_thesis: ( ((0. X),x) to_power n1 = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
n1 <= m ) & ((0. X),x) to_power n2 = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
n2 <= m ) implies n1 = n2 )
assume ( ((0. X),x) to_power n1 = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
n1 <= m ) & ((0. X),x) to_power n2 = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
n2 <= m ) ) ; ::_thesis: n1 = n2
then ( n1 <= n2 & n2 <= n1 ) ;
hence n1 = n2 by XXREAL_0:1; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem Def8 defines ord BCIALG_2:def_8_:_
for X being BCI-algebra
for x being Element of X st x is nilpotent holds
for b3 being non empty Element of NAT holds
( b3 = ord x iff ( ((0. X),x) to_power b3 = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
b3 <= m ) ) );
registration
let X be BCI-algebra;
cluster 0. X -> nilpotent ;
coherence
0. X is nilpotent
proof
((0. X),(0. X)) to_power 1 = 0. X by Th6;
hence 0. X is nilpotent by Def6; ::_thesis: verum
end;
end;
theorem :: BCIALG_2:31
for X being BCI-algebra
for x being Element of X holds
( x is positive Element of X iff ( x is nilpotent & ord x = 1 ) )
proof
let X be BCI-algebra; ::_thesis: for x being Element of X holds
( x is positive Element of X iff ( x is nilpotent & ord x = 1 ) )
let x be Element of X; ::_thesis: ( x is positive Element of X iff ( x is nilpotent & ord x = 1 ) )
thus ( x is positive Element of X implies ( x is nilpotent & ord x = 1 ) ) ::_thesis: ( x is nilpotent & ord x = 1 implies x is positive Element of X )
proof
assume x is positive Element of X ; ::_thesis: ( x is nilpotent & ord x = 1 )
then 0. X <= x by Def2;
then A1: x ` = 0. X by BCIALG_1:def_11;
thus A2: x is nilpotent ::_thesis: ord x = 1
proof
set k = 1;
take 1 ; :: according to BCIALG_2:def_6 ::_thesis: ((0. X),x) to_power 1 = 0. X
thus ((0. X),x) to_power 1 = 0. X by A1, Th2; ::_thesis: verum
end;
thus ord x = 1 ::_thesis: verum
proof
set k = 1;
reconsider k = 1 as non empty Element of NAT ;
( ((0. X),x) to_power k = 0. X & ( for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
k <= m ) ) by A1, Th2, NAT_1:14;
hence ord x = 1 by A2, Def8; ::_thesis: verum
end;
end;
assume ( x is nilpotent & ord x = 1 ) ; ::_thesis: x is positive Element of X
then ((0. X),x) to_power 1 = 0. X by Def8;
then x ` = 0. X by Th2;
then 0. X <= x by BCIALG_1:def_11;
hence x is positive Element of X by Def2; ::_thesis: verum
end;
theorem :: BCIALG_2:32
for X being BCI-algebra holds
( X is BCK-algebra iff for x being Element of X holds
( ord x = 1 & x is nilpotent ) )
proof
let X be BCI-algebra; ::_thesis: ( X is BCK-algebra iff for x being Element of X holds
( ord x = 1 & x is nilpotent ) )
thus ( X is BCK-algebra implies for x being Element of X holds
( ord x = 1 & x is nilpotent ) ) ::_thesis: ( ( for x being Element of X holds
( ord x = 1 & x is nilpotent ) ) implies X is BCK-algebra )
proof
set k = 1;
assume A1: X is BCK-algebra ; ::_thesis: for x being Element of X holds
( ord x = 1 & x is nilpotent )
let x be Element of X; ::_thesis: ( ord x = 1 & x is nilpotent )
A2: x ` = 0. X by A1, BCIALG_1:def_8;
then ((0. X),x) to_power 1 = 0. X by Th2;
then A3: x is nilpotent by Def6;
reconsider k = 1 as non empty Element of NAT ;
A4: for m being Element of NAT st ((0. X),x) to_power m = 0. X & m <> 0 holds
k <= m by NAT_1:14;
((0. X),x) to_power k = 0. X by A2, Th2;
hence ( ord x = 1 & x is nilpotent ) by A3, A4, Def8; ::_thesis: verum
end;
assume A5: for x being Element of X holds
( ord x = 1 & x is nilpotent ) ; ::_thesis: X is BCK-algebra
now__::_thesis:_for_x_being_Element_of_X_holds_x_`_=_0._X
let x be Element of X; ::_thesis: x ` = 0. X
( ord x = 1 & x is nilpotent ) by A5;
then ((0. X),x) to_power 1 = 0. X by Def8;
hence x ` = 0. X by Th2; ::_thesis: verum
end;
hence X is BCK-algebra by BCIALG_1:def_8; ::_thesis: verum
end;
theorem :: BCIALG_2:33
for X being BCI-algebra
for x being Element of X
for n being Element of NAT holds ((0. X),(x `)) to_power n is minimal
proof
let X be BCI-algebra; ::_thesis: for x being Element of X
for n being Element of NAT holds ((0. X),(x `)) to_power n is minimal
let x be Element of X; ::_thesis: for n being Element of NAT holds ((0. X),(x `)) to_power n is minimal
let n be Element of NAT ; ::_thesis: ((0. X),(x `)) to_power n is minimal
((0. X),(x `)) to_power n = (((0. X),x) to_power n) ` by Th9;
hence ((0. X),(x `)) to_power n is minimal by Th30; ::_thesis: verum
end;
theorem :: BCIALG_2:34
for X being BCI-algebra
for x being Element of X st x is nilpotent holds
ord x = ord (x `)
proof
let X be BCI-algebra; ::_thesis: for x being Element of X st x is nilpotent holds
ord x = ord (x `)
let x be Element of X; ::_thesis: ( x is nilpotent implies ord x = ord (x `) )
assume A1: x is nilpotent ; ::_thesis: ord x = ord (x `)
then consider k being non empty Element of NAT such that
A2: ((0. X),x) to_power k = 0. X by Def6;
A3: x ` is nilpotent
proof
take k ; :: according to BCIALG_2:def_6 ::_thesis: ((0. X),(x `)) to_power k = 0. X
((0. X),(x `)) to_power k = (((0. X),x) to_power k) ` by Th9
.= 0. X by A2, BCIALG_1:def_5 ;
hence ((0. X),(x `)) to_power k = 0. X ; ::_thesis: verum
end;
set k = ord x;
A4: now__::_thesis:_for_m_being_Element_of_NAT_st_((0._X),(x_`))_to_power_m_=_0._X_&_m_<>_0_holds_
ord_x_<=_m
let m be Element of NAT ; ::_thesis: ( ((0. X),(x `)) to_power m = 0. X & m <> 0 implies ord x <= m )
assume that
A5: ((0. X),(x `)) to_power m = 0. X and
A6: m <> 0 ; ::_thesis: ord x <= m
(((0. X),x) to_power m) ` = 0. X by A5, Th9;
then ((((0. X),x) to_power m) `) ` = 0. X by BCIALG_1:def_5;
then ((0. X),x) to_power m = 0. X by Th12;
hence ord x <= m by A1, A6, Def8; ::_thesis: verum
end;
((0. X),(x `)) to_power (ord x) = (((0. X),x) to_power (ord x)) ` by Th9
.= (0. X) ` by A1, Def8
.= 0. X by BCIALG_1:def_5 ;
hence ord x = ord (x `) by A3, A4, Def8; ::_thesis: verum
end;
begin
definition
let X be BCI-algebra;
mode Congruence of X -> Equivalence_Relation of X means :Def9: :: BCIALG_2:def 9
for x, y, u, v being Element of X st [x,y] in it & [u,v] in it holds
[(x \ u),(y \ v)] in it;
existence
ex b1 being Equivalence_Relation of X st
for x, y, u, v being Element of X st [x,y] in b1 & [u,v] in b1 holds
[(x \ u),(y \ v)] in b1
proof
reconsider P = id the carrier of X as Equivalence_Relation of X ;
take P ; ::_thesis: for x, y, u, v being Element of X st [x,y] in P & [u,v] in P holds
[(x \ u),(y \ v)] in P
let x, y, u, v be Element of X; ::_thesis: ( [x,y] in P & [u,v] in P implies [(x \ u),(y \ v)] in P )
assume ( [x,y] in P & [u,v] in P ) ; ::_thesis: [(x \ u),(y \ v)] in P
then ( x = y & u = v ) by RELAT_1:def_10;
hence [(x \ u),(y \ v)] in P by RELAT_1:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines Congruence BCIALG_2:def_9_:_
for X being BCI-algebra
for b2 being Equivalence_Relation of X holds
( b2 is Congruence of X iff for x, y, u, v being Element of X st [x,y] in b2 & [u,v] in b2 holds
[(x \ u),(y \ v)] in b2 );
definition
let X be BCI-algebra;
mode L-congruence of X -> Equivalence_Relation of X means :Def10: :: BCIALG_2:def 10
for x, y being Element of X st [x,y] in it holds
for u being Element of X holds [(u \ x),(u \ y)] in it;
existence
ex b1 being Equivalence_Relation of X st
for x, y being Element of X st [x,y] in b1 holds
for u being Element of X holds [(u \ x),(u \ y)] in b1
proof
reconsider P = id the carrier of X as Equivalence_Relation of X ;
take P ; ::_thesis: for x, y being Element of X st [x,y] in P holds
for u being Element of X holds [(u \ x),(u \ y)] in P
let x, y be Element of X; ::_thesis: ( [x,y] in P implies for u being Element of X holds [(u \ x),(u \ y)] in P )
assume A1: [x,y] in P ; ::_thesis: for u being Element of X holds [(u \ x),(u \ y)] in P
let u be Element of X; ::_thesis: [(u \ x),(u \ y)] in P
u \ x = u \ y by A1, RELAT_1:def_10;
hence [(u \ x),(u \ y)] in P by RELAT_1:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines L-congruence BCIALG_2:def_10_:_
for X being BCI-algebra
for b2 being Equivalence_Relation of X holds
( b2 is L-congruence of X iff for x, y being Element of X st [x,y] in b2 holds
for u being Element of X holds [(u \ x),(u \ y)] in b2 );
definition
let X be BCI-algebra;
mode R-congruence of X -> Equivalence_Relation of X means :Def11: :: BCIALG_2:def 11
for x, y being Element of X st [x,y] in it holds
for u being Element of X holds [(x \ u),(y \ u)] in it;
existence
ex b1 being Equivalence_Relation of X st
for x, y being Element of X st [x,y] in b1 holds
for u being Element of X holds [(x \ u),(y \ u)] in b1
proof
reconsider P = id the carrier of X as Equivalence_Relation of X ;
take P ; ::_thesis: for x, y being Element of X st [x,y] in P holds
for u being Element of X holds [(x \ u),(y \ u)] in P
let x, y be Element of X; ::_thesis: ( [x,y] in P implies for u being Element of X holds [(x \ u),(y \ u)] in P )
assume A1: [x,y] in P ; ::_thesis: for u being Element of X holds [(x \ u),(y \ u)] in P
let u be Element of X; ::_thesis: [(x \ u),(y \ u)] in P
x \ u = y \ u by A1, RELAT_1:def_10;
hence [(x \ u),(y \ u)] in P by RELAT_1:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines R-congruence BCIALG_2:def_11_:_
for X being BCI-algebra
for b2 being Equivalence_Relation of X holds
( b2 is R-congruence of X iff for x, y being Element of X st [x,y] in b2 holds
for u being Element of X holds [(x \ u),(y \ u)] in b2 );
definition
let X be BCI-algebra;
let A be Ideal of X;
mode I-congruence of X,A -> Relation of X means :Def12: :: BCIALG_2:def 12
for x, y being Element of X holds
( [x,y] in it iff ( x \ y in A & y \ x in A ) );
existence
ex b1 being Relation of X st
for x, y being Element of X holds
( [x,y] in b1 iff ( x \ y in A & y \ x in A ) )
proof
defpred S1[ set , set ] means ex x, y being Element of X st
( x = $1 & y = $2 & x \ y in A & y \ x in A );
consider P being Relation of X such that
A1: for x2, y2 being set holds
( [x2,y2] in P iff ( x2 in the carrier of X & y2 in the carrier of X & S1[x2,y2] ) ) from RELSET_1:sch_1();
take P ; ::_thesis: for x, y being Element of X holds
( [x,y] in P iff ( x \ y in A & y \ x in A ) )
let x2, y2 be Element of X; ::_thesis: ( [x2,y2] in P iff ( x2 \ y2 in A & y2 \ x2 in A ) )
( [x2,y2] in P implies ex x1, y1 being Element of X st
( x1 = x2 & y1 = y2 & x1 \ y1 in A & y1 \ x1 in A ) ) by A1;
hence ( [x2,y2] in P implies ( x2 \ y2 in A & y2 \ x2 in A ) ) ; ::_thesis: ( x2 \ y2 in A & y2 \ x2 in A implies [x2,y2] in P )
thus ( x2 \ y2 in A & y2 \ x2 in A implies [x2,y2] in P ) by A1; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines I-congruence BCIALG_2:def_12_:_
for X being BCI-algebra
for A being Ideal of X
for b3 being Relation of X holds
( b3 is I-congruence of X,A iff for x, y being Element of X holds
( [x,y] in b3 iff ( x \ y in A & y \ x in A ) ) );
registration
let X be BCI-algebra;
let A be Ideal of X;
cluster -> total symmetric transitive for I-congruence of X,A;
coherence
for b1 being I-congruence of X,A holds
( b1 is total & b1 is symmetric & b1 is transitive )
proof
for RI being I-congruence of X,A holds RI is Equivalence_Relation of X
proof
let RI be I-congruence of X,A; ::_thesis: RI is Equivalence_Relation of X
reconsider RI = RI as Relation of X ;
for x being set st x in the carrier of X holds
[x,x] in RI
proof
let x be set ; ::_thesis: ( x in the carrier of X implies [x,x] in RI )
assume x in the carrier of X ; ::_thesis: [x,x] in RI
then reconsider x = x as Element of X ;
0. X in A by BCIALG_1:def_18;
then x \ x in A by BCIALG_1:def_5;
hence [x,x] in RI by Def12; ::_thesis: verum
end;
then RI is_reflexive_in the carrier of X by RELAT_2:def_1;
then A1: field RI = the carrier of X by ORDERS_1:13;
for x, y, z being set st [x,y] in RI & [y,z] in RI holds
[x,z] in RI
proof
let x, y, z be set ; ::_thesis: ( [x,y] in RI & [y,z] in RI implies [x,z] in RI )
assume that
A2: [x,y] in RI and
A3: [y,z] in RI ; ::_thesis: [x,z] in RI
reconsider x = x, y = y, z = z as Element of X by A2, A3, ZFMISC_1:87;
((z \ x) \ (y \ x)) \ (z \ y) = 0. X by BCIALG_1:def_3;
then A4: ((z \ x) \ (y \ x)) \ (z \ y) in A by BCIALG_1:def_18;
((x \ z) \ (x \ y)) \ (y \ z) = 0. X by BCIALG_1:1;
then A5: ((x \ z) \ (x \ y)) \ (y \ z) in A by BCIALG_1:def_18;
y \ z in A by A3, Def12;
then A6: (x \ z) \ (x \ y) in A by A5, BCIALG_1:def_18;
z \ y in A by A3, Def12;
then A7: (z \ x) \ (y \ x) in A by A4, BCIALG_1:def_18;
y \ x in A by A2, Def12;
then A8: z \ x in A by A7, BCIALG_1:def_18;
x \ y in A by A2, Def12;
then x \ z in A by A6, BCIALG_1:def_18;
hence [x,z] in RI by A8, Def12; ::_thesis: verum
end;
then A9: RI is transitive by RELAT_2:31;
for x, y being set st x in the carrier of X & y in the carrier of X & [x,y] in RI holds
[y,x] in RI
proof
let x, y be set ; ::_thesis: ( x in the carrier of X & y in the carrier of X & [x,y] in RI implies [y,x] in RI )
assume that
A10: ( x in the carrier of X & y in the carrier of X ) and
A11: [x,y] in RI ; ::_thesis: [y,x] in RI
reconsider x = x, y = y as Element of X by A10;
( x \ y in A & y \ x in A ) by A11, Def12;
hence [y,x] in RI by Def12; ::_thesis: verum
end;
then RI is_symmetric_in the carrier of X by RELAT_2:def_3;
then RI is symmetric by A1, RELAT_2:def_11;
hence RI is Equivalence_Relation of X by A1, A9, EQREL_1:9; ::_thesis: verum
end;
hence for b1 being I-congruence of X,A holds
( b1 is total & b1 is symmetric & b1 is transitive ) ; ::_thesis: verum
end;
end;
definition
let X be BCI-algebra;
func IConSet X -> set means :Def13: :: BCIALG_2:def 13
for A1 being set holds
( A1 in it iff ex I being Ideal of X st A1 is I-congruence of X,I );
existence
ex b1 being set st
for A1 being set holds
( A1 in b1 iff ex I being Ideal of X st A1 is I-congruence of X,I )
proof
defpred S1[ set ] means ex I being Ideal of X st $1 is I-congruence of X,I;
consider Y being set such that
A1: for x being set holds
( x in Y iff ( x in bool [: the carrier of X, the carrier of X:] & S1[x] ) ) from XBOOLE_0:sch_1();
take Y ; ::_thesis: for A1 being set holds
( A1 in Y iff ex I being Ideal of X st A1 is I-congruence of X,I )
let x be set ; ::_thesis: ( x in Y iff ex I being Ideal of X st x is I-congruence of X,I )
thus ( x in Y implies ex I being Ideal of X st x is I-congruence of X,I ) by A1; ::_thesis: ( ex I being Ideal of X st x is I-congruence of X,I implies x in Y )
given I being Ideal of X such that A2: x is I-congruence of X,I ; ::_thesis: x in Y
thus x in Y by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for A1 being set holds
( A1 in b1 iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) & ( for A1 being set holds
( A1 in b2 iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex I being Ideal of X st $1 is I-congruence of X,I;
let A1, A2 be set ; ::_thesis: ( ( for A1 being set holds
( A1 in A1 iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) & ( for A1 being set holds
( A1 in A2 iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) implies A1 = A2 )
assume that
A3: for x being set holds
( x in A1 iff ex I being Ideal of X st x is I-congruence of X,I ) and
A4: for x being set holds
( x in A2 iff ex I being Ideal of X st x is I-congruence of X,I ) ; ::_thesis: A1 = A2
A5: for x being set holds
( x in A2 iff S1[x] ) by A4;
A6: for x being set holds
( x in A1 iff S1[x] ) by A3;
A1 = A2 from XBOOLE_0:sch_2(A6, A5);
hence A1 = A2 ; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines IConSet BCIALG_2:def_13_:_
for X being BCI-algebra
for b2 being set holds
( b2 = IConSet X iff for A1 being set holds
( A1 in b2 iff ex I being Ideal of X st A1 is I-congruence of X,I ) );
definition
let X be BCI-algebra;
func ConSet X -> set equals :: BCIALG_2:def 14
{ R where R is Congruence of X : verum } ;
coherence
{ R where R is Congruence of X : verum } is set ;
func LConSet X -> set equals :: BCIALG_2:def 15
{ R where R is L-congruence of X : verum } ;
coherence
{ R where R is L-congruence of X : verum } is set ;
func RConSet X -> set equals :: BCIALG_2:def 16
{ R where R is R-congruence of X : verum } ;
coherence
{ R where R is R-congruence of X : verum } is set ;
end;
:: deftheorem defines ConSet BCIALG_2:def_14_:_
for X being BCI-algebra holds ConSet X = { R where R is Congruence of X : verum } ;
:: deftheorem defines LConSet BCIALG_2:def_15_:_
for X being BCI-algebra holds LConSet X = { R where R is L-congruence of X : verum } ;
:: deftheorem defines RConSet BCIALG_2:def_16_:_
for X being BCI-algebra holds RConSet X = { R where R is R-congruence of X : verum } ;
theorem :: BCIALG_2:35
for X being BCI-algebra
for E being Congruence of X holds Class (E,(0. X)) is closed Ideal of X
proof
let X be BCI-algebra; ::_thesis: for E being Congruence of X holds Class (E,(0. X)) is closed Ideal of X
let E be Congruence of X; ::_thesis: Class (E,(0. X)) is closed Ideal of X
A1: now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_in_Class_(E,(0._X))_&_y_in_Class_(E,(0._X))_holds_
x_in_Class_(E,(0._X))
let x, y be Element of X; ::_thesis: ( x \ y in Class (E,(0. X)) & y in Class (E,(0. X)) implies x in Class (E,(0. X)) )
assume that
A2: x \ y in Class (E,(0. X)) and
A3: y in Class (E,(0. X)) ; ::_thesis: x in Class (E,(0. X))
A4: [x,x] in E by EQREL_1:5;
[(0. X),y] in E by A3, EQREL_1:18;
then [(x \ (0. X)),(x \ y)] in E by A4, Def9;
then [x,(x \ y)] in E by BCIALG_1:2;
then A5: [(x \ y),x] in E by EQREL_1:6;
[(0. X),(x \ y)] in E by A2, EQREL_1:18;
then [(0. X),x] in E by A5, EQREL_1:7;
hence x in Class (E,(0. X)) by EQREL_1:18; ::_thesis: verum
end;
A6: [(0. X),(0. X)] in E by EQREL_1:5;
then 0. X in Class (E,(0. X)) by EQREL_1:18;
then reconsider Rx = Class (E,(0. X)) as Ideal of X by A1, BCIALG_1:def_18;
now__::_thesis:_for_x_being_Element_of_Rx_holds_x_`_in_Class_(E,(0._X))
let x be Element of Rx; ::_thesis: x ` in Class (E,(0. X))
[(0. X),x] in E by EQREL_1:18;
then [((0. X) `),(x `)] in E by A6, Def9;
then [(0. X),(x `)] in E by BCIALG_1:def_5;
hence x ` in Class (E,(0. X)) by EQREL_1:18; ::_thesis: verum
end;
hence Class (E,(0. X)) is closed Ideal of X by BCIALG_1:def_19; ::_thesis: verum
end;
theorem Th36: :: BCIALG_2:36
for X being BCI-algebra
for R being Equivalence_Relation of X holds
( R is Congruence of X iff ( R is R-congruence of X & R is L-congruence of X ) )
proof
let X be BCI-algebra; ::_thesis: for R being Equivalence_Relation of X holds
( R is Congruence of X iff ( R is R-congruence of X & R is L-congruence of X ) )
let R be Equivalence_Relation of X; ::_thesis: ( R is Congruence of X iff ( R is R-congruence of X & R is L-congruence of X ) )
A1: field R = the carrier of X by EQREL_1:9;
then A2: R is_reflexive_in the carrier of X by RELAT_2:def_9;
thus ( R is Congruence of X implies ( R is R-congruence of X & R is L-congruence of X ) ) ::_thesis: ( R is R-congruence of X & R is L-congruence of X implies R is Congruence of X )
proof
assume A3: R is Congruence of X ; ::_thesis: ( R is R-congruence of X & R is L-congruence of X )
thus R is R-congruence of X ::_thesis: R is L-congruence of X
proof
let x, y be Element of X; :: according to BCIALG_2:def_11 ::_thesis: ( [x,y] in R implies for u being Element of X holds [(x \ u),(y \ u)] in R )
assume A4: [x,y] in R ; ::_thesis: for u being Element of X holds [(x \ u),(y \ u)] in R
let u be Element of X; ::_thesis: [(x \ u),(y \ u)] in R
[u,u] in R by A2, RELAT_2:def_1;
hence [(x \ u),(y \ u)] in R by A3, A4, Def9; ::_thesis: verum
end;
let x, y be Element of X; :: according to BCIALG_2:def_10 ::_thesis: ( [x,y] in R implies for u being Element of X holds [(u \ x),(u \ y)] in R )
assume A5: [x,y] in R ; ::_thesis: for u being Element of X holds [(u \ x),(u \ y)] in R
let u be Element of X; ::_thesis: [(u \ x),(u \ y)] in R
[u,u] in R by A2, RELAT_2:def_1;
hence [(u \ x),(u \ y)] in R by A3, A5, Def9; ::_thesis: verum
end;
assume A6: ( R is R-congruence of X & R is L-congruence of X ) ; ::_thesis: R is Congruence of X
A7: R is_transitive_in the carrier of X by A1, RELAT_2:def_16;
now__::_thesis:_for_x,_y,_u,_v_being_Element_of_X_st_[x,y]_in_R_&_[u,v]_in_R_holds_
[(x_\_u),(y_\_v)]_in_R
let x, y, u, v be Element of X; ::_thesis: ( [x,y] in R & [u,v] in R implies [(x \ u),(y \ v)] in R )
assume ( [x,y] in R & [u,v] in R ) ; ::_thesis: [(x \ u),(y \ v)] in R
then ( [(x \ u),(y \ u)] in R & [(y \ u),(y \ v)] in R ) by A6, Def10, Def11;
hence [(x \ u),(y \ v)] in R by A7, RELAT_2:def_8; ::_thesis: verum
end;
hence R is Congruence of X by Def9; ::_thesis: verum
end;
theorem Th37: :: BCIALG_2:37
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds RI is Congruence of X
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X
for RI being I-congruence of X,I holds RI is Congruence of X
let I be Ideal of X; ::_thesis: for RI being I-congruence of X,I holds RI is Congruence of X
let RI be I-congruence of X,I; ::_thesis: RI is Congruence of X
field RI = the carrier of X by EQREL_1:9;
then A1: RI is_transitive_in the carrier of X by RELAT_2:def_16;
now__::_thesis:_for_x,_y,_u,_v_being_Element_of_X_st_[x,y]_in_RI_&_[u,v]_in_RI_holds_
[(x_\_u),(y_\_v)]_in_RI
let x, y, u, v be Element of X; ::_thesis: ( [x,y] in RI & [u,v] in RI implies [(x \ u),(y \ v)] in RI )
assume that
A2: [x,y] in RI and
A3: [u,v] in RI ; ::_thesis: [(x \ u),(y \ v)] in RI
((y \ u) \ (y \ v)) \ (v \ u) = 0. X by BCIALG_1:1;
then A4: ((y \ u) \ (y \ v)) \ (v \ u) in I by BCIALG_1:def_18;
v \ u in I by A3, Def12;
then A5: (y \ u) \ (y \ v) in I by A4, BCIALG_1:def_18;
((y \ v) \ (y \ u)) \ (u \ v) = 0. X by BCIALG_1:1;
then A6: ((y \ v) \ (y \ u)) \ (u \ v) in I by BCIALG_1:def_18;
u \ v in I by A3, Def12;
then (y \ v) \ (y \ u) in I by A6, BCIALG_1:def_18;
then A7: [(y \ u),(y \ v)] in RI by A5, Def12;
((x \ u) \ (y \ u)) \ (x \ y) = 0. X by BCIALG_1:def_3;
then A8: ((x \ u) \ (y \ u)) \ (x \ y) in I by BCIALG_1:def_18;
((y \ u) \ (x \ u)) \ (y \ x) = 0. X by BCIALG_1:def_3;
then A9: ((y \ u) \ (x \ u)) \ (y \ x) in I by BCIALG_1:def_18;
y \ x in I by A2, Def12;
then A10: (y \ u) \ (x \ u) in I by A9, BCIALG_1:def_18;
x \ y in I by A2, Def12;
then (x \ u) \ (y \ u) in I by A8, BCIALG_1:def_18;
then [(x \ u),(y \ u)] in RI by A10, Def12;
hence [(x \ u),(y \ v)] in RI by A1, A7, RELAT_2:def_8; ::_thesis: verum
end;
hence RI is Congruence of X by Def9; ::_thesis: verum
end;
definition
let X be BCI-algebra;
let I be Ideal of X;
:: original: I-congruence
redefine mode I-congruence of X,I -> Congruence of X;
coherence
for b1 being I-congruence of X,I holds b1 is Congruence of X by Th37;
end;
theorem Th38: :: BCIALG_2:38
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds Class (RI,(0. X)) c= I
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X
for RI being I-congruence of X,I holds Class (RI,(0. X)) c= I
let I be Ideal of X; ::_thesis: for RI being I-congruence of X,I holds Class (RI,(0. X)) c= I
let RI be I-congruence of X,I; ::_thesis: Class (RI,(0. X)) c= I
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Class (RI,(0. X)) or x in I )
assume A1: x in Class (RI,(0. X)) ; ::_thesis: x in I
then consider y being set such that
A2: [y,x] in RI and
A3: y in {(0. X)} by RELAT_1:def_13;
reconsider x = x as Element of X by A1;
reconsider y = y as Element of X by A3, TARSKI:def_1;
y = 0. X by A3, TARSKI:def_1;
then x \ (0. X) in I by A2, Def12;
hence x in I by BCIALG_1:2; ::_thesis: verum
end;
theorem :: BCIALG_2:39
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds
( I is closed iff I = Class (RI,(0. X)) )
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X
for RI being I-congruence of X,I holds
( I is closed iff I = Class (RI,(0. X)) )
let I be Ideal of X; ::_thesis: for RI being I-congruence of X,I holds
( I is closed iff I = Class (RI,(0. X)) )
let RI be I-congruence of X,I; ::_thesis: ( I is closed iff I = Class (RI,(0. X)) )
thus ( I is closed implies I = Class (RI,(0. X)) ) ::_thesis: ( I = Class (RI,(0. X)) implies I is closed )
proof
assume A1: I is closed ; ::_thesis: I = Class (RI,(0. X))
thus I c= Class (RI,(0. X)) :: according to XBOOLE_0:def_10 ::_thesis: Class (RI,(0. X)) c= I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in I or x in Class (RI,(0. X)) )
assume A2: x in I ; ::_thesis: x in Class (RI,(0. X))
then reconsider x = x as Element of I ;
A3: x \ (0. X) in I by A2, BCIALG_1:2;
x ` in I by A1, BCIALG_1:def_19;
then ( 0. X in {(0. X)} & [(0. X),x] in RI ) by A3, Def12, TARSKI:def_1;
hence x in Class (RI,(0. X)) by RELAT_1:def_13; ::_thesis: verum
end;
thus Class (RI,(0. X)) c= I by Th38; ::_thesis: verum
end;
assume A4: I = Class (RI,(0. X)) ; ::_thesis: I is closed
now__::_thesis:_for_x_being_Element_of_I_holds_x_`_in_I
let x be Element of I; ::_thesis: x ` in I
ex y being set st
( [y,x] in RI & y in {(0. X)} ) by A4, RELAT_1:def_13;
then [(0. X),x] in RI by TARSKI:def_1;
hence x ` in I by Def12; ::_thesis: verum
end;
hence I is closed by BCIALG_1:def_19; ::_thesis: verum
end;
theorem Th40: :: BCIALG_2:40
for X being BCI-algebra
for x, y being Element of X
for E being Congruence of X st [x,y] in E holds
( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) )
proof
let X be BCI-algebra; ::_thesis: for x, y being Element of X
for E being Congruence of X st [x,y] in E holds
( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) )
let x, y be Element of X; ::_thesis: for E being Congruence of X st [x,y] in E holds
( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) )
let E be Congruence of X; ::_thesis: ( [x,y] in E implies ( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) ) )
assume A1: [x,y] in E ; ::_thesis: ( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) )
A2: field E = the carrier of X by EQREL_1:9;
then A3: E is_reflexive_in the carrier of X by RELAT_2:def_9;
then A4: [y,y] in E by RELAT_2:def_1;
E is_symmetric_in the carrier of X by A2, RELAT_2:def_11;
then [y,x] in E by A1, RELAT_2:def_3;
then [(y \ y),(x \ y)] in E by A4, Def9;
then A5: [(0. X),(x \ y)] in E by BCIALG_1:def_5;
[x,x] in E by A3, RELAT_2:def_1;
then [(x \ x),(y \ x)] in E by A1, Def9;
then ( 0. X in {(0. X)} & [(0. X),(y \ x)] in E ) by BCIALG_1:def_5, TARSKI:def_1;
hence ( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) ) by A5, RELAT_1:def_13; ::_thesis: verum
end;
theorem :: BCIALG_2:41
for X being BCI-algebra
for A, I being Ideal of X
for IA being I-congruence of X,A
for II being I-congruence of X,I st Class (IA,(0. X)) = Class (II,(0. X)) holds
IA = II
proof
let X be BCI-algebra; ::_thesis: for A, I being Ideal of X
for IA being I-congruence of X,A
for II being I-congruence of X,I st Class (IA,(0. X)) = Class (II,(0. X)) holds
IA = II
let A, I be Ideal of X; ::_thesis: for IA being I-congruence of X,A
for II being I-congruence of X,I st Class (IA,(0. X)) = Class (II,(0. X)) holds
IA = II
let IA be I-congruence of X,A; ::_thesis: for II being I-congruence of X,I st Class (IA,(0. X)) = Class (II,(0. X)) holds
IA = II
let II be I-congruence of X,I; ::_thesis: ( Class (IA,(0. X)) = Class (II,(0. X)) implies IA = II )
assume A1: Class (IA,(0. X)) = Class (II,(0. X)) ; ::_thesis: IA = II
let xx, yy be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [xx,yy] in IA or [xx,yy] in II ) & ( not [xx,yy] in II or [xx,yy] in IA ) )
thus ( [xx,yy] in IA implies [xx,yy] in II ) ::_thesis: ( not [xx,yy] in II or [xx,yy] in IA )
proof
assume A2: [xx,yy] in IA ; ::_thesis: [xx,yy] in II
then consider x, y being set such that
A3: [xx,yy] = [x,y] and
A4: ( x in the carrier of X & y in the carrier of X ) by RELSET_1:2;
reconsider x = x, y = y as Element of X by A4;
x \ y in II .: {(0. X)} by A1, A2, A3, Th40;
then ex z being set st
( [z,(x \ y)] in II & z in {(0. X)} ) by RELAT_1:def_13;
then [(0. X),(x \ y)] in II by TARSKI:def_1;
then (x \ y) \ (0. X) in I by Def12;
then A5: x \ y in I by BCIALG_1:2;
y \ x in II .: {(0. X)} by A1, A2, A3, Th40;
then ex z being set st
( [z,(y \ x)] in II & z in {(0. X)} ) by RELAT_1:def_13;
then [(0. X),(y \ x)] in II by TARSKI:def_1;
then (y \ x) \ (0. X) in I by Def12;
then y \ x in I by BCIALG_1:2;
hence [xx,yy] in II by A3, A5, Def12; ::_thesis: verum
end;
thus ( [xx,yy] in II implies [xx,yy] in IA ) ::_thesis: verum
proof
assume A6: [xx,yy] in II ; ::_thesis: [xx,yy] in IA
then consider x, y being set such that
A7: [xx,yy] = [x,y] and
A8: ( x in the carrier of X & y in the carrier of X ) by RELSET_1:2;
reconsider x = x, y = y as Element of X by A8;
x \ y in IA .: {(0. X)} by A1, A6, A7, Th40;
then ex z being set st
( [z,(x \ y)] in IA & z in {(0. X)} ) by RELAT_1:def_13;
then [(0. X),(x \ y)] in IA by TARSKI:def_1;
then (x \ y) \ (0. X) in A by Def12;
then A9: x \ y in A by BCIALG_1:2;
y \ x in IA .: {(0. X)} by A1, A6, A7, Th40;
then ex z being set st
( [z,(y \ x)] in IA & z in {(0. X)} ) by RELAT_1:def_13;
then [(0. X),(y \ x)] in IA by TARSKI:def_1;
then (y \ x) \ (0. X) in A by Def12;
then y \ x in A by BCIALG_1:2;
hence [xx,yy] in IA by A7, A9, Def12; ::_thesis: verum
end;
end;
theorem Th42: :: BCIALG_2:42
for X being BCI-algebra
for x, y, u being Element of X
for k being Element of NAT
for E being Congruence of X st [x,y] in E & u in Class (E,(0. X)) holds
[x,((y,u) to_power k)] in E
proof
let X be BCI-algebra; ::_thesis: for x, y, u being Element of X
for k being Element of NAT
for E being Congruence of X st [x,y] in E & u in Class (E,(0. X)) holds
[x,((y,u) to_power k)] in E
let x, y, u be Element of X; ::_thesis: for k being Element of NAT
for E being Congruence of X st [x,y] in E & u in Class (E,(0. X)) holds
[x,((y,u) to_power k)] in E
let k be Element of NAT ; ::_thesis: for E being Congruence of X st [x,y] in E & u in Class (E,(0. X)) holds
[x,((y,u) to_power k)] in E
let E be Congruence of X; ::_thesis: ( [x,y] in E & u in Class (E,(0. X)) implies [x,((y,u) to_power k)] in E )
assume that
A1: [x,y] in E and
A2: u in Class (E,(0. X)) ; ::_thesis: [x,((y,u) to_power k)] in E
defpred S1[ Element of NAT ] means [x,((y,u) to_power $1)] in E;
ex z being set st
( [z,u] in E & z in {(0. X)} ) by A2, RELAT_1:def_13;
then A3: [(0. X),u] in E by TARSKI:def_1;
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume [x,((y,u) to_power k)] in E ; ::_thesis: S1[k + 1]
then [(x \ (0. X)),(((y,u) to_power k) \ u)] in E by A3, Def9;
then [x,(((y,u) to_power k) \ u)] in E by BCIALG_1:2;
hence S1[k + 1] by Th4; ::_thesis: verum
end;
A5: S1[ 0 ] by A1, Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A4);
hence [x,((y,u) to_power k)] in E ; ::_thesis: verum
end;
theorem :: BCIALG_2:43
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X ex i, j, m, n being Element of NAT st (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n ) holds
for E being Congruence of X
for I being Ideal of X st I = Class (E,(0. X)) holds
E is I-congruence of X,I
proof
let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra
for x, y being Element of X ex i, j, m, n being Element of NAT st (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n ) implies for E being Congruence of X
for I being Ideal of X st I = Class (E,(0. X)) holds
E is I-congruence of X,I )
assume A1: for X being BCI-algebra
for x, y being Element of X ex i, j, m, n being Element of NAT st (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n ; ::_thesis: for E being Congruence of X
for I being Ideal of X st I = Class (E,(0. X)) holds
E is I-congruence of X,I
let E be Congruence of X; ::_thesis: for I being Ideal of X st I = Class (E,(0. X)) holds
E is I-congruence of X,I
let I be Ideal of X; ::_thesis: ( I = Class (E,(0. X)) implies E is I-congruence of X,I )
assume A2: I = Class (E,(0. X)) ; ::_thesis: E is I-congruence of X,I
now__::_thesis:_for_x,_y_being_Element_of_X_holds_
(_[x,y]_in_E_iff_(_x_\_y_in_I_&_y_\_x_in_I_)_)
let x, y be Element of X; ::_thesis: ( [x,y] in E iff ( x \ y in I & y \ x in I ) )
( x \ y in I & y \ x in I implies [x,y] in E )
proof
assume that
A3: x \ y in I and
A4: y \ x in I ; ::_thesis: [x,y] in E
ex z being set st
( [z,(y \ x)] in E & z in {(0. X)} ) by A2, A4, RELAT_1:def_13;
then A5: [(0. X),(y \ x)] in E by TARSKI:def_1;
ex z being set st
( [z,(x \ y)] in E & z in {(0. X)} ) by A2, A3, RELAT_1:def_13;
then A6: [(0. X),(x \ y)] in E by TARSKI:def_1;
consider i, j, m, n being Element of NAT such that
A7: (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n by A1;
A8: field E = the carrier of X by EQREL_1:9;
A9: E is_reflexive_in field E by RELAT_2:def_9;
then [x,x] in E by A8, RELAT_2:def_1;
then A10: [x,((x,(x \ y)) to_power i)] in E by A2, A3, Th42;
A11: [x,((((x,(x \ y)) to_power i),(y \ x)) to_power j)] in E
proof
defpred S1[ Element of NAT ] means [x,((((x,(x \ y)) to_power i),(y \ x)) to_power $1)] in E;
A12: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume [x,((((x,(x \ y)) to_power i),(y \ x)) to_power k)] in E ; ::_thesis: S1[k + 1]
then [(x \ (0. X)),(((((x,(x \ y)) to_power i),(y \ x)) to_power k) \ (y \ x))] in E by A5, Def9;
then [x,(((((x,(x \ y)) to_power i),(y \ x)) to_power k) \ (y \ x))] in E by BCIALG_1:2;
hence S1[k + 1] by Th4; ::_thesis: verum
end;
A13: S1[ 0 ] by A10, Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A12);
hence [x,((((x,(x \ y)) to_power i),(y \ x)) to_power j)] in E ; ::_thesis: verum
end;
[y,y] in E by A8, A9, RELAT_2:def_1;
then A14: [y,((y,(y \ x)) to_power m)] in E by A2, A4, Th42;
A15: [y,((((y,(y \ x)) to_power m),(x \ y)) to_power n)] in E
proof
defpred S1[ Element of NAT ] means [y,((((y,(y \ x)) to_power m),(x \ y)) to_power $1)] in E;
A16: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume [y,((((y,(y \ x)) to_power m),(x \ y)) to_power k)] in E ; ::_thesis: S1[k + 1]
then [(y \ (0. X)),(((((y,(y \ x)) to_power m),(x \ y)) to_power k) \ (x \ y))] in E by A6, Def9;
then [y,(((((y,(y \ x)) to_power m),(x \ y)) to_power k) \ (x \ y))] in E by BCIALG_1:2;
hence S1[k + 1] by Th4; ::_thesis: verum
end;
A17: S1[ 0 ] by A14, Th1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A17, A16);
hence [y,((((y,(y \ x)) to_power m),(x \ y)) to_power n)] in E ; ::_thesis: verum
end;
E is_symmetric_in field E by RELAT_2:def_11;
then ( E is_transitive_in field E & [((((x,(x \ y)) to_power i),(y \ x)) to_power j),y] in E ) by A7, A8, A15, RELAT_2:def_3, RELAT_2:def_16;
hence [x,y] in E by A8, A11, RELAT_2:def_8; ::_thesis: verum
end;
hence ( [x,y] in E iff ( x \ y in I & y \ x in I ) ) by A2, Th40; ::_thesis: verum
end;
hence E is I-congruence of X,I by Def12; ::_thesis: verum
end;
theorem :: BCIALG_2:44
for X being BCI-algebra holds IConSet X c= ConSet X
proof
let X be BCI-algebra; ::_thesis: IConSet X c= ConSet X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in IConSet X or x in ConSet X )
assume x in IConSet X ; ::_thesis: x in ConSet X
then ex I being Ideal of X st x is I-congruence of X,I by Def13;
hence x in ConSet X ; ::_thesis: verum
end;
theorem Th45: :: BCIALG_2:45
for X being BCI-algebra holds ConSet X c= LConSet X
proof
let X be BCI-algebra; ::_thesis: ConSet X c= LConSet X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ConSet X or x in LConSet X )
assume x in ConSet X ; ::_thesis: x in LConSet X
then ex R being Congruence of X st x = R ;
then x is L-congruence of X by Th36;
hence x in LConSet X ; ::_thesis: verum
end;
theorem Th46: :: BCIALG_2:46
for X being BCI-algebra holds ConSet X c= RConSet X
proof
let X be BCI-algebra; ::_thesis: ConSet X c= RConSet X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ConSet X or x in RConSet X )
assume x in ConSet X ; ::_thesis: x in RConSet X
then ex R being Congruence of X st x = R ;
then x is R-congruence of X by Th36;
hence x in RConSet X ; ::_thesis: verum
end;
theorem :: BCIALG_2:47
for X being BCI-algebra holds ConSet X = (LConSet X) /\ (RConSet X)
proof
let X be BCI-algebra; ::_thesis: ConSet X = (LConSet X) /\ (RConSet X)
( ConSet X c= LConSet X & ConSet X c= RConSet X ) by Th45, Th46;
hence ConSet X c= (LConSet X) /\ (RConSet X) by XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: (LConSet X) /\ (RConSet X) c= ConSet X
thus (LConSet X) /\ (RConSet X) c= ConSet X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LConSet X) /\ (RConSet X) or x in ConSet X )
assume A1: x in (LConSet X) /\ (RConSet X) ; ::_thesis: x in ConSet X
then x in RConSet X by XBOOLE_0:def_4;
then A2: ex R being R-congruence of X st x = R ;
x in LConSet X by A1, XBOOLE_0:def_4;
then ex L being L-congruence of X st x = L ;
then x is Congruence of X by A2, Th36;
hence x in ConSet X ; ::_thesis: verum
end;
end;
theorem :: BCIALG_2:48
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for E being Congruence of X st ( for LC being L-congruence of X holds LC is I-congruence of X,I ) holds
E = RI
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X
for RI being I-congruence of X,I
for E being Congruence of X st ( for LC being L-congruence of X holds LC is I-congruence of X,I ) holds
E = RI
let I be Ideal of X; ::_thesis: for RI being I-congruence of X,I
for E being Congruence of X st ( for LC being L-congruence of X holds LC is I-congruence of X,I ) holds
E = RI
let RI be I-congruence of X,I; ::_thesis: for E being Congruence of X st ( for LC being L-congruence of X holds LC is I-congruence of X,I ) holds
E = RI
let E be Congruence of X; ::_thesis: ( ( for LC being L-congruence of X holds LC is I-congruence of X,I ) implies E = RI )
assume A1: for LC being L-congruence of X holds LC is I-congruence of X,I ; ::_thesis: E = RI
let x1, y1 be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x1,y1] in E or [x1,y1] in RI ) & ( not [x1,y1] in RI or [x1,y1] in E ) )
E is L-congruence of X by Th36;
then A2: E is I-congruence of X,I by A1;
thus ( [x1,y1] in E implies [x1,y1] in RI ) ::_thesis: ( not [x1,y1] in RI or [x1,y1] in E )
proof
assume A3: [x1,y1] in E ; ::_thesis: [x1,y1] in RI
then consider x, y being set such that
A4: [x1,y1] = [x,y] and
A5: ( x in the carrier of X & y in the carrier of X ) by RELSET_1:2;
reconsider x = x, y = y as Element of X by A5;
y \ x in Class (E,(0. X)) by A3, A4, Th40;
then ex z being set st
( [z,(y \ x)] in E & z in {(0. X)} ) by RELAT_1:def_13;
then [(0. X),(y \ x)] in E by TARSKI:def_1;
then (y \ x) \ (0. X) in I by A2, Def12;
then A6: y \ x in I by BCIALG_1:2;
x \ y in Class (E,(0. X)) by A3, A4, Th40;
then ex z being set st
( [z,(x \ y)] in E & z in {(0. X)} ) by RELAT_1:def_13;
then [(0. X),(x \ y)] in E by TARSKI:def_1;
then (x \ y) \ (0. X) in I by A2, Def12;
then x \ y in I by BCIALG_1:2;
hence [x1,y1] in RI by A4, A6, Def12; ::_thesis: verum
end;
thus ( [x1,y1] in RI implies [x1,y1] in E ) ::_thesis: verum
proof
assume A7: [x1,y1] in RI ; ::_thesis: [x1,y1] in E
then consider x, y being set such that
A8: [x1,y1] = [x,y] and
A9: ( x in the carrier of X & y in the carrier of X ) by RELSET_1:2;
reconsider x = x, y = y as Element of X by A9;
( x \ y in I & y \ x in I ) by A7, A8, Def12;
hence [x1,y1] in E by A2, A8, Def12; ::_thesis: verum
end;
end;
theorem :: BCIALG_2:49
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for E being Congruence of X st ( for RC being R-congruence of X holds RC is I-congruence of X,I ) holds
E = RI
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X
for RI being I-congruence of X,I
for E being Congruence of X st ( for RC being R-congruence of X holds RC is I-congruence of X,I ) holds
E = RI
let I be Ideal of X; ::_thesis: for RI being I-congruence of X,I
for E being Congruence of X st ( for RC being R-congruence of X holds RC is I-congruence of X,I ) holds
E = RI
let RI be I-congruence of X,I; ::_thesis: for E being Congruence of X st ( for RC being R-congruence of X holds RC is I-congruence of X,I ) holds
E = RI
let E be Congruence of X; ::_thesis: ( ( for RC being R-congruence of X holds RC is I-congruence of X,I ) implies E = RI )
assume A1: for RC being R-congruence of X holds RC is I-congruence of X,I ; ::_thesis: E = RI
let x1, y1 be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x1,y1] in E or [x1,y1] in RI ) & ( not [x1,y1] in RI or [x1,y1] in E ) )
E is R-congruence of X by Th36;
then A2: E is I-congruence of X,I by A1;
thus ( [x1,y1] in E implies [x1,y1] in RI ) ::_thesis: ( not [x1,y1] in RI or [x1,y1] in E )
proof
assume A3: [x1,y1] in E ; ::_thesis: [x1,y1] in RI
then consider x, y being set such that
A4: [x1,y1] = [x,y] and
A5: ( x in the carrier of X & y in the carrier of X ) by RELSET_1:2;
reconsider x = x, y = y as Element of X by A5;
y \ x in Class (E,(0. X)) by A3, A4, Th40;
then ex z being set st
( [z,(y \ x)] in E & z in {(0. X)} ) by RELAT_1:def_13;
then [(0. X),(y \ x)] in E by TARSKI:def_1;
then (y \ x) \ (0. X) in I by A2, Def12;
then A6: y \ x in I by BCIALG_1:2;
x \ y in Class (E,(0. X)) by A3, A4, Th40;
then ex z being set st
( [z,(x \ y)] in E & z in {(0. X)} ) by RELAT_1:def_13;
then [(0. X),(x \ y)] in E by TARSKI:def_1;
then (x \ y) \ (0. X) in I by A2, Def12;
then x \ y in I by BCIALG_1:2;
hence [x1,y1] in RI by A4, A6, Def12; ::_thesis: verum
end;
thus ( [x1,y1] in RI implies [x1,y1] in E ) ::_thesis: verum
proof
assume A7: [x1,y1] in RI ; ::_thesis: [x1,y1] in E
then consider x, y being set such that
A8: [x1,y1] = [x,y] and
A9: ( x in the carrier of X & y in the carrier of X ) by RELSET_1:2;
reconsider x = x, y = y as Element of X by A9;
( x \ y in I & y \ x in I ) by A7, A8, Def12;
hence [x1,y1] in E by A2, A8, Def12; ::_thesis: verum
end;
end;
theorem :: BCIALG_2:50
for X being BCI-algebra
for LC being L-congruence of X holds Class (LC,(0. X)) is closed Ideal of X
proof
let X be BCI-algebra; ::_thesis: for LC being L-congruence of X holds Class (LC,(0. X)) is closed Ideal of X
let LC be L-congruence of X; ::_thesis: Class (LC,(0. X)) is closed Ideal of X
A1: now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_in_Class_(LC,(0._X))_&_y_in_Class_(LC,(0._X))_holds_
x_in_Class_(LC,(0._X))
let x, y be Element of X; ::_thesis: ( x \ y in Class (LC,(0. X)) & y in Class (LC,(0. X)) implies x in Class (LC,(0. X)) )
assume that
A2: x \ y in Class (LC,(0. X)) and
A3: y in Class (LC,(0. X)) ; ::_thesis: x in Class (LC,(0. X))
[(0. X),y] in LC by A3, EQREL_1:18;
then [(x \ (0. X)),(x \ y)] in LC by Def10;
then [x,(x \ y)] in LC by BCIALG_1:2;
then A4: [(x \ y),x] in LC by EQREL_1:6;
[(0. X),(x \ y)] in LC by A2, EQREL_1:18;
then [(0. X),x] in LC by A4, EQREL_1:7;
hence x in Class (LC,(0. X)) by EQREL_1:18; ::_thesis: verum
end;
[(0. X),(0. X)] in LC by EQREL_1:5;
then 0. X in Class (LC,(0. X)) by EQREL_1:18;
then reconsider Rx = Class (LC,(0. X)) as Ideal of X by A1, BCIALG_1:def_18;
now__::_thesis:_for_x_being_Element_of_Rx_holds_x_`_in_Class_(LC,(0._X))
let x be Element of Rx; ::_thesis: x ` in Class (LC,(0. X))
[(0. X),x] in LC by EQREL_1:18;
then [((0. X) `),(x `)] in LC by Def10;
then [(0. X),(x `)] in LC by BCIALG_1:def_5;
hence x ` in Class (LC,(0. X)) by EQREL_1:18; ::_thesis: verum
end;
hence Class (LC,(0. X)) is closed Ideal of X by BCIALG_1:def_19; ::_thesis: verum
end;
registration
let X be BCI-algebra;
let E be Congruence of X;
cluster Class E -> non empty ;
coherence
not Class E is empty
proof
Class (E,(0. X)) in Class E by EQREL_1:def_3;
hence not Class E is empty ; ::_thesis: verum
end;
end;
definition
let X be BCI-algebra;
let E be Congruence of X;
func EqClaOp E -> BinOp of (Class E) means :Def17: :: BCIALG_2:def 17
for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
it . (W1,W2) = Class (E,(x \ y));
existence
ex b1 being BinOp of (Class E) st
for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b1 . (W1,W2) = Class (E,(x \ y))
proof
defpred S1[ Element of Class E, Element of Class E, set ] means for x, y being Element of X st $1 = Class (E,x) & $2 = Class (E,y) holds
$3 = Class (E,(x \ y));
A1: for W1, W2 being Element of Class E ex V being Element of Class E st S1[W1,W2,V]
proof
let W1, W2 be Element of Class E; ::_thesis: ex V being Element of Class E st S1[W1,W2,V]
consider x1 being set such that
A2: x1 in the carrier of X and
A3: W1 = Class (E,x1) by EQREL_1:def_3;
consider y1 being set such that
A4: y1 in the carrier of X and
A5: W2 = Class (E,y1) by EQREL_1:def_3;
reconsider x1 = x1, y1 = y1 as Element of X by A2, A4;
reconsider C = Class (E,(x1 \ y1)) as Element of Class E by EQREL_1:def_3;
take C ; ::_thesis: S1[W1,W2,C]
now__::_thesis:_for_x,_y_being_Element_of_X_st_W1_=_Class_(E,x)_&_W2_=_Class_(E,y)_holds_
C_=_Class_(E,(x_\_y))
let x, y be Element of X; ::_thesis: ( W1 = Class (E,x) & W2 = Class (E,y) implies C = Class (E,(x \ y)) )
assume that
A6: W1 = Class (E,x) and
A7: W2 = Class (E,y) ; ::_thesis: C = Class (E,(x \ y))
y in Class (E,y1) by A5, A7, EQREL_1:23;
then A8: [y1,y] in E by EQREL_1:18;
x in Class (E,x1) by A3, A6, EQREL_1:23;
then [x1,x] in E by EQREL_1:18;
then [(x1 \ y1),(x \ y)] in E by A8, Def9;
then x \ y in Class (E,(x1 \ y1)) by EQREL_1:18;
hence C = Class (E,(x \ y)) by EQREL_1:23; ::_thesis: verum
end;
hence S1[W1,W2,C] ; ::_thesis: verum
end;
thus ex B being BinOp of (Class E) st
for W1, W2 being Element of Class E holds S1[W1,W2,B . (W1,W2)] from BINOP_1:sch_3(A1); ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Class E) st ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b1 . (W1,W2) = Class (E,(x \ y)) ) & ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b2 . (W1,W2) = Class (E,(x \ y)) ) holds
b1 = b2
proof
let o1, o2 be BinOp of (Class E); ::_thesis: ( ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
o1 . (W1,W2) = Class (E,(x \ y)) ) & ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
o2 . (W1,W2) = Class (E,(x \ y)) ) implies o1 = o2 )
assume A9: for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
o1 . (W1,W2) = Class (E,(x \ y)) ; ::_thesis: ( ex W1, W2 being Element of Class E ex x, y being Element of X st
( W1 = Class (E,x) & W2 = Class (E,y) & not o2 . (W1,W2) = Class (E,(x \ y)) ) or o1 = o2 )
assume A10: for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
o2 . (W1,W2) = Class (E,(x \ y)) ; ::_thesis: o1 = o2
now__::_thesis:_for_W1,_W2_being_Element_of_Class_E_holds_o1_._(W1,W2)_=_o2_._(W1,W2)
let W1, W2 be Element of Class E; ::_thesis: o1 . (W1,W2) = o2 . (W1,W2)
consider x being set such that
A11: x in the carrier of X and
A12: W1 = Class (E,x) by EQREL_1:def_3;
consider y being set such that
A13: y in the carrier of X and
A14: W2 = Class (E,y) by EQREL_1:def_3;
reconsider x = x, y = y as Element of X by A11, A13;
o1 . (W1,W2) = Class (E,(x \ y)) by A9, A12, A14;
hence o1 . (W1,W2) = o2 . (W1,W2) by A10, A12, A14; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def17 defines EqClaOp BCIALG_2:def_17_:_
for X being BCI-algebra
for E being Congruence of X
for b3 being BinOp of (Class E) holds
( b3 = EqClaOp E iff for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b3 . (W1,W2) = Class (E,(x \ y)) );
definition
let X be BCI-algebra;
let E be Congruence of X;
func zeroEqC E -> Element of Class E equals :: BCIALG_2:def 18
Class (E,(0. X));
coherence
Class (E,(0. X)) is Element of Class E by EQREL_1:def_3;
end;
:: deftheorem defines zeroEqC BCIALG_2:def_18_:_
for X being BCI-algebra
for E being Congruence of X holds zeroEqC E = Class (E,(0. X));
definition
let X be BCI-algebra;
let E be Congruence of X;
funcX ./. E -> BCIStr_0 equals :: BCIALG_2:def 19
BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #);
coherence
BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #) is BCIStr_0 ;
end;
:: deftheorem defines ./. BCIALG_2:def_19_:_
for X being BCI-algebra
for E being Congruence of X holds X ./. E = BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #);
registration
let X be BCI-algebra;
let E be Congruence of X;
clusterX ./. E -> non empty ;
coherence
not X ./. E is empty ;
end;
definition
let X be BCI-algebra;
let E be Congruence of X;
let W1, W2 be Element of Class E;
funcW1 \ W2 -> Element of Class E equals :: BCIALG_2:def 20
(EqClaOp E) . (W1,W2);
coherence
(EqClaOp E) . (W1,W2) is Element of Class E ;
end;
:: deftheorem defines \ BCIALG_2:def_20_:_
for X being BCI-algebra
for E being Congruence of X
for W1, W2 being Element of Class E holds W1 \ W2 = (EqClaOp E) . (W1,W2);
theorem Th51: :: BCIALG_2:51
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds X ./. RI is BCI-algebra
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X
for RI being I-congruence of X,I holds X ./. RI is BCI-algebra
let I be Ideal of X; ::_thesis: for RI being I-congruence of X,I holds X ./. RI is BCI-algebra
let RI be I-congruence of X,I; ::_thesis: X ./. RI is BCI-algebra
reconsider IT = X ./. RI as non empty BCIStr_0 ;
A1: now__::_thesis:_for_w1,_w2,_w3_being_Element_of_IT_holds_((w1_\_w2)_\_(w3_\_w2))_\_(w1_\_w3)_=_0._IT
let w1, w2, w3 be Element of IT; ::_thesis: ((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3) = 0. IT
w1 in the carrier of IT ;
then consider x1 being set such that
A2: x1 in the carrier of X and
A3: w1 = Class (RI,x1) by EQREL_1:def_3;
w3 in the carrier of IT ;
then consider z1 being set such that
A4: z1 in the carrier of X and
A5: w3 = Class (RI,z1) by EQREL_1:def_3;
w2 in the carrier of IT ;
then consider y1 being set such that
A6: y1 in the carrier of X and
A7: w2 = Class (RI,y1) by EQREL_1:def_3;
reconsider x1 = x1, y1 = y1, z1 = z1 as Element of X by A2, A6, A4;
A8: w3 \ w2 = Class (RI,(z1 \ y1)) by A7, A5, Def17;
w1 \ w2 = Class (RI,(x1 \ y1)) by A3, A7, Def17;
then A9: (w1 \ w2) \ (w3 \ w2) = Class (RI,((x1 \ y1) \ (z1 \ y1))) by A8, Def17;
w1 \ w3 = Class (RI,(x1 \ z1)) by A3, A5, Def17;
then ((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3) = Class (RI,(((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1))) by A9, Def17;
hence ((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3) = 0. IT by BCIALG_1:def_3; ::_thesis: verum
end;
A10: now__::_thesis:_for_w1,_w2,_w3_being_Element_of_IT_holds_((w1_\_w2)_\_w3)_\_((w1_\_w3)_\_w2)_=_0._IT
let w1, w2, w3 be Element of IT; ::_thesis: ((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2) = 0. IT
w1 in the carrier of IT ;
then consider x1 being set such that
A11: x1 in the carrier of X and
A12: w1 = Class (RI,x1) by EQREL_1:def_3;
w2 in the carrier of IT ;
then consider y1 being set such that
A13: y1 in the carrier of X and
A14: w2 = Class (RI,y1) by EQREL_1:def_3;
w3 in the carrier of IT ;
then consider z1 being set such that
A15: z1 in the carrier of X and
A16: w3 = Class (RI,z1) by EQREL_1:def_3;
reconsider x1 = x1, y1 = y1, z1 = z1 as Element of X by A11, A13, A15;
w1 \ w3 = Class (RI,(x1 \ z1)) by A12, A16, Def17;
then A17: (w1 \ w3) \ w2 = Class (RI,((x1 \ z1) \ y1)) by A14, Def17;
w1 \ w2 = Class (RI,(x1 \ y1)) by A12, A14, Def17;
then (w1 \ w2) \ w3 = Class (RI,((x1 \ y1) \ z1)) by A16, Def17;
then ((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2) = Class (RI,(((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1))) by A17, Def17;
hence ((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2) = 0. IT by BCIALG_1:def_4; ::_thesis: verum
end;
A18: now__::_thesis:_for_w1,_w2_being_Element_of_IT_st_w1_\_w2_=_0._IT_&_w2_\_w1_=_0._IT_holds_
w1_=_w2
let w1, w2 be Element of IT; ::_thesis: ( w1 \ w2 = 0. IT & w2 \ w1 = 0. IT implies w1 = w2 )
assume that
A19: w1 \ w2 = 0. IT and
A20: w2 \ w1 = 0. IT ; ::_thesis: w1 = w2
w1 in the carrier of IT ;
then consider x1 being set such that
A21: x1 in the carrier of X and
A22: w1 = Class (RI,x1) by EQREL_1:def_3;
w2 in the carrier of IT ;
then consider y1 being set such that
A23: y1 in the carrier of X and
A24: w2 = Class (RI,y1) by EQREL_1:def_3;
reconsider x1 = x1, y1 = y1 as Element of X by A21, A23;
w2 \ w1 = Class (RI,(y1 \ x1)) by A22, A24, Def17;
then 0. X in Class (RI,(y1 \ x1)) by A20, EQREL_1:23;
then [(y1 \ x1),(0. X)] in RI by EQREL_1:18;
then (y1 \ x1) \ (0. X) in I by Def12;
then A25: y1 \ x1 in I by BCIALG_1:2;
w1 \ w2 = Class (RI,(x1 \ y1)) by A22, A24, Def17;
then 0. X in Class (RI,(x1 \ y1)) by A19, EQREL_1:23;
then [(x1 \ y1),(0. X)] in RI by EQREL_1:18;
then (x1 \ y1) \ (0. X) in I by Def12;
then x1 \ y1 in I by BCIALG_1:2;
then [x1,y1] in RI by A25, Def12;
hence w1 = w2 by A22, A24, EQREL_1:35; ::_thesis: verum
end;
now__::_thesis:_for_w1_being_Element_of_IT_holds_w1_\_w1_=_0._IT
let w1 be Element of IT; ::_thesis: w1 \ w1 = 0. IT
w1 in the carrier of IT ;
then consider x1 being set such that
A26: x1 in the carrier of X and
A27: w1 = Class (RI,x1) by EQREL_1:def_3;
reconsider x1 = x1 as Element of X by A26;
w1 \ w1 = Class (RI,(x1 \ x1)) by A27, Def17;
hence w1 \ w1 = 0. IT by BCIALG_1:def_5; ::_thesis: verum
end;
hence X ./. RI is BCI-algebra by A1, A10, A18, BCIALG_1:def_3, BCIALG_1:def_4, BCIALG_1:def_5, BCIALG_1:def_7; ::_thesis: verum
end;
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 ) by Th51;
end;
theorem :: BCIALG_2:52
for X being BCI-algebra
for I being Ideal of X st I = BCK-part X holds
for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra
proof
let X be BCI-algebra; ::_thesis: for I being Ideal of X st I = BCK-part X holds
for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra
let I be Ideal of X; ::_thesis: ( I = BCK-part X implies for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra )
assume A1: I = BCK-part X ; ::_thesis: for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra
let RI be I-congruence of X,I; ::_thesis: X ./. RI is p-Semisimple BCI-algebra
set IT = X ./. RI;
for w1 being Element of (X ./. RI) holds (w1 `) ` = w1
proof
let w1 be Element of (X ./. RI); ::_thesis: (w1 `) ` = w1
w1 in the carrier of (X ./. RI) ;
then consider x1 being set such that
A2: x1 in the carrier of X and
A3: w1 = Class (RI,x1) by EQREL_1:def_3;
reconsider x1 = x1 as Element of X by A2;
w1 ` = Class (RI,(x1 `)) by A3, Def17;
then A4: (w1 `) ` = Class (RI,((x1 `) `)) by Def17;
x1 \ ((x1 `) `) is positive Element of X by Th28;
then 0. X <= x1 \ ((x1 `) `) by Def2;
then A5: x1 \ ((x1 `) `) in I by A1;
0. X in I by BCIALG_1:def_18;
then ((x1 `) `) \ x1 in I by BCIALG_1:1;
then [((x1 `) `),x1] in RI by A5, Def12;
hence (w1 `) ` = w1 by A3, A4, EQREL_1:35; ::_thesis: verum
end;
hence X ./. RI is p-Semisimple BCI-algebra by BCIALG_1:54; ::_thesis: verum
end;