environ
vocabularies HIDDEN, BINOP_1, CARD_1, FUNCOP_1, FUNCT_4, RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, FUNCT_7, SUBSET_1, FUNCT_1, ALGSTR_0, ARYTM_3, SUPINF_2, REALSET1, VECTSP_1, STRUCT_0, MESFUNC1, RLVECT_1, LATTICES, ARYTM_1, REALSET2, MEMBERED;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, REALSET1, FUNCOP_1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_7, MEMBERED, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1;
definitions RLVECT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, ENUMSET1, REALSET1, VECTSP_1, RELSET_1, XBOOLE_0, RLVECT_1, FUNCT_4, FUNCOP_1, CARD_1, XBOOLE_1, STRUCT_0, GROUP_1, ALGSTR_0, XTUPLE_0, SUBSET_1;
schemes FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, STRUCT_0, RLVECT_1, VECTSP_1, ORDINAL1, ALGSTR_0, ZFMISC_1, CARD_1;
constructors HIDDEN, RLVECT_1, BINOP_1, FUNCT_4, REALSET1, FUNCT_7, VECTSP_1, RELSET_1, MEMBERED, GROUP_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities TARSKI, REALSET1, BINOP_1, STRUCT_0, FUNCOP_1, ALGSTR_0, ORDINAL1;
expansions RLVECT_1, TARSKI, MEMBERED, VECTSP_1;
set x = In (0,2);
set y = In (1,2);
Lm1:
1 in 2
by CARD_1:50, TARSKI:def 2;
Lm2:
0 in 2
by CARD_1:50, TARSKI:def 2;
then Lm3:
In (0,2) = 0
by SUBSET_1:def 8;
Lm4:
In (1,2) = 1
by Lm1, SUBSET_1:def 8;
set Z = 2;
reconsider A = 2 as non trivial set by Lm1, Lm2, ZFMISC_1:def 10;
reconsider nd = In (0,2) as Element of A ;
Lm5:
dom ((1,1) .--> 0) = {[1,1]}
by FUNCOP_1:13;
Lm6:
dom ((1,0) .--> 1) = {[1,0]}
by FUNCOP_1:13;
Lm7:
dom ((0,1) .--> 1) = {[0,1]}
by FUNCOP_1:13;
Lm8:
add_2 . ((In (0,2)),(In (0,2))) = In (0,2)
Lm9:
add_2 . ((In (0,2)),(In (1,2))) = In (1,2)
Lm10:
add_2 . ((In (1,2)),(In (0,2))) = In (1,2)
Lm11:
add_2 . ((In (1,2)),(In (1,2))) = In (0,2)
Lm12:
dom ((1,1) .--> 1) = {[1,1]}
by FUNCOP_1:13;
Lm13:
dom ((1,0) .--> 0) = {[1,0]}
by FUNCOP_1:13;
Lm14:
dom ((0,1) .--> 0) = {[0,1]}
by FUNCOP_1:13;
Lm15:
mult_2 . ((In (0,2)),(In (0,2))) = In (0,2)
Lm16:
mult_2 . ((In (0,2)),(In (1,2))) = In (0,2)
Lm17:
mult_2 . ((In (1,2)),(In (0,2))) = In (0,2)
Lm18:
mult_2 . ((In (1,2)),(In (1,2))) = In (1,2)
set om = mult_2 ;
Lm19:
A \ {(In (0,2))} = {(In (1,2))}
by Lm3, Lm4, CARD_1:50, ZFMISC_1:17;
then Lm20:
[:(A \ {(In (0,2))}),(A \ {(In (0,2))}):] = {[(In (1,2)),(In (1,2))]}
by ZFMISC_1:29;
Lm21:
for t being set st t in [:(A \ {(In (0,2))}),(A \ {(In (0,2))}):] holds
mult_2 . t in A \ {(In (0,2))}
reconsider nm = In (1,2) as Element of A \ {nd} by Lm19, TARSKI:def 1;
reconsider od0 = add_2 as BinOp of A ;
reconsider om0 = mult_2 as BinOp of A ;
Lm22:
for a, b, d being Element of A holds add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))
reconsider dL = doubleLoopStr(# A,od0,om0,nm,nd #) as non empty doubleLoopStr ;
Lm23:
for a being Element of dL holds a + (0. dL) = a
Lm24:
for a, b, c being Element of dL holds (a + b) + c = a + (b + c)
by Lm22;
Lm25:
for a, b being Element of dL holds a + b = b + a
reconsider om1 = mult_2 as DnT of nd,A by Lm21, REALSET1:def 6;
Lm26:
for B being non empty set
for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm holds
addLoopStr(# B,P,e #) is AbGroup
Lm27:
for a, b, d being Element of dL holds
( a * (b + d) = (a * b) + (a * d) & (b + d) * a = (b * a) + (d * a) )
Lm28:
for B being non empty set
for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm & P = om1 ! (A,nd) holds
addLoopStr(# B,P,e #) is AbGroup
by Lm26;
deffunc H1( non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ) -> set = the carrier of $1;