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