Metamath Proof Explorer


Theorem cygablOLD

Description: Obsolete proof of cygabl as of 20-Jan-2024. A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion cygablOLD G CycGrp G Abel

Proof

Step Hyp Ref Expression
1 eqid Base G = Base G
2 eqid G = G
3 1 2 iscyg3 G CycGrp G Grp x Base G y Base G n y = n G x
4 eqidd G Grp x Base G y Base G n y = n G x Base G = Base G
5 eqidd G Grp x Base G y Base G n y = n G x + G = + G
6 simpll G Grp x Base G y Base G n y = n G x G Grp
7 eqeq1 y = a y = n G x a = n G x
8 7 rexbidv y = a n y = n G x n a = n G x
9 oveq1 n = m n G x = m G x
10 9 eqeq2d n = m a = n G x a = m G x
11 10 cbvrexv n a = n G x m a = m G x
12 8 11 bitrdi y = a n y = n G x m a = m G x
13 12 rspccv y Base G n y = n G x a Base G m a = m G x
14 13 adantl G Grp x Base G y Base G n y = n G x a Base G m a = m G x
15 eqeq1 y = b y = n G x b = n G x
16 15 rexbidv y = b n y = n G x n b = n G x
17 16 rspccv y Base G n y = n G x b Base G n b = n G x
18 17 adantl G Grp x Base G y Base G n y = n G x b Base G n b = n G x
19 reeanv m n a = m G x b = n G x m a = m G x n b = n G x
20 zcn m m
21 20 ad2antrl G Grp x Base G m n m
22 zcn n n
23 22 ad2antll G Grp x Base G m n n
24 21 23 addcomd G Grp x Base G m n m + n = n + m
25 24 oveq1d G Grp x Base G m n m + n G x = n + m G x
26 simpll G Grp x Base G m n G Grp
27 simprl G Grp x Base G m n m
28 simprr G Grp x Base G m n n
29 simplr G Grp x Base G m n x Base G
30 eqid + G = + G
31 1 2 30 mulgdir G Grp m n x Base G m + n G x = m G x + G n G x
32 26 27 28 29 31 syl13anc G Grp x Base G m n m + n G x = m G x + G n G x
33 1 2 30 mulgdir G Grp n m x Base G n + m G x = n G x + G m G x
34 26 28 27 29 33 syl13anc G Grp x Base G m n n + m G x = n G x + G m G x
35 25 32 34 3eqtr3d G Grp x Base G m n m G x + G n G x = n G x + G m G x
36 oveq12 a = m G x b = n G x a + G b = m G x + G n G x
37 oveq12 b = n G x a = m G x b + G a = n G x + G m G x
38 37 ancoms a = m G x b = n G x b + G a = n G x + G m G x
39 36 38 eqeq12d a = m G x b = n G x a + G b = b + G a m G x + G n G x = n G x + G m G x
40 35 39 syl5ibrcom G Grp x Base G m n a = m G x b = n G x a + G b = b + G a
41 40 rexlimdvva G Grp x Base G m n a = m G x b = n G x a + G b = b + G a
42 19 41 syl5bir G Grp x Base G m a = m G x n b = n G x a + G b = b + G a
43 42 adantr G Grp x Base G y Base G n y = n G x m a = m G x n b = n G x a + G b = b + G a
44 14 18 43 syl2and G Grp x Base G y Base G n y = n G x a Base G b Base G a + G b = b + G a
45 44 3impib G Grp x Base G y Base G n y = n G x a Base G b Base G a + G b = b + G a
46 4 5 6 45 isabld G Grp x Base G y Base G n y = n G x G Abel
47 46 r19.29an G Grp x Base G y Base G n y = n G x G Abel
48 3 47 sylbi G CycGrp G Abel