Step | Hyp | Ref
| Expression |
1 | | archiabllem.g |
. . 3
β’ (π β π β oGrp) |
2 | | ogrpgrp 32208 |
. . 3
β’ (π β oGrp β π β Grp) |
3 | 1, 2 | syl 17 |
. 2
β’ (π β π β Grp) |
4 | | simplr 767 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β€) β§ π β β€) β π β β€) |
5 | 4 | zcnd 12663 |
. . . . . . . . . . . 12
β’ (((π β§ π β β€) β§ π β β€) β π β β) |
6 | | simpr 485 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β€) β§ π β β€) β π β β€) |
7 | 6 | zcnd 12663 |
. . . . . . . . . . . 12
β’ (((π β§ π β β€) β§ π β β€) β π β β) |
8 | 5, 7 | addcomd 11412 |
. . . . . . . . . . 11
β’ (((π β§ π β β€) β§ π β β€) β (π + π) = (π + π)) |
9 | 8 | oveq1d 7420 |
. . . . . . . . . 10
β’ (((π β§ π β β€) β§ π β β€) β ((π + π) Β· π) = ((π + π) Β· π)) |
10 | 3 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β β€) β§ π β β€) β π β Grp) |
11 | | archiabllem1.u |
. . . . . . . . . . . 12
β’ (π β π β π΅) |
12 | 11 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β β€) β§ π β β€) β π β π΅) |
13 | | archiabllem.b |
. . . . . . . . . . . 12
β’ π΅ = (Baseβπ) |
14 | | archiabllem.m |
. . . . . . . . . . . 12
β’ Β· =
(.gβπ) |
15 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(+gβπ) = (+gβπ) |
16 | 13, 14, 15 | mulgdir 18980 |
. . . . . . . . . . 11
β’ ((π β Grp β§ (π β β€ β§ π β β€ β§ π β π΅)) β ((π + π) Β· π) = ((π Β· π)(+gβπ)(π Β· π))) |
17 | 10, 4, 6, 12, 16 | syl13anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π β β€) β§ π β β€) β ((π + π) Β· π) = ((π Β· π)(+gβπ)(π Β· π))) |
18 | 13, 14, 15 | mulgdir 18980 |
. . . . . . . . . . 11
β’ ((π β Grp β§ (π β β€ β§ π β β€ β§ π β π΅)) β ((π + π) Β· π) = ((π Β· π)(+gβπ)(π Β· π))) |
19 | 10, 6, 4, 12, 18 | syl13anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π β β€) β§ π β β€) β ((π + π) Β· π) = ((π Β· π)(+gβπ)(π Β· π))) |
20 | 9, 17, 19 | 3eqtr3d 2780 |
. . . . . . . . 9
β’ (((π β§ π β β€) β§ π β β€) β ((π Β· π)(+gβπ)(π Β· π)) = ((π Β· π)(+gβπ)(π Β· π))) |
21 | 20 | adantllr 717 |
. . . . . . . 8
β’ ((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π β β€) β ((π Β· π)(+gβπ)(π Β· π)) = ((π Β· π)(+gβπ)(π Β· π))) |
22 | 21 | adantlr 713 |
. . . . . . 7
β’
(((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β§ π β β€) β ((π Β· π)(+gβπ)(π Β· π)) = ((π Β· π)(+gβπ)(π Β· π))) |
23 | 22 | adantr 481 |
. . . . . 6
β’
((((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β§ π β β€) β§ π§ = (π Β· π)) β ((π Β· π)(+gβπ)(π Β· π)) = ((π Β· π)(+gβπ)(π Β· π))) |
24 | | simpllr 774 |
. . . . . . 7
β’
((((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β§ π β β€) β§ π§ = (π Β· π)) β π¦ = (π Β· π)) |
25 | | simpr 485 |
. . . . . . 7
β’
((((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β§ π β β€) β§ π§ = (π Β· π)) β π§ = (π Β· π)) |
26 | 24, 25 | oveq12d 7423 |
. . . . . 6
β’
((((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β§ π β β€) β§ π§ = (π Β· π)) β (π¦(+gβπ)π§) = ((π Β· π)(+gβπ)(π Β· π))) |
27 | 25, 24 | oveq12d 7423 |
. . . . . 6
β’
((((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β§ π β β€) β§ π§ = (π Β· π)) β (π§(+gβπ)π¦) = ((π Β· π)(+gβπ)(π Β· π))) |
28 | 23, 26, 27 | 3eqtr4d 2782 |
. . . . 5
β’
((((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β§ π β β€) β§ π§ = (π Β· π)) β (π¦(+gβπ)π§) = (π§(+gβπ)π¦)) |
29 | | simplll 773 |
. . . . . 6
β’ ((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β π) |
30 | | simpr1r 1231 |
. . . . . . 7
β’ ((π β§ ((π¦ β π΅ β§ π§ β π΅) β§ π β β€ β§ π¦ = (π Β· π))) β π§ β π΅) |
31 | 30 | 3anassrs 1360 |
. . . . . 6
β’ ((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β π§ β π΅) |
32 | | archiabllem.0 |
. . . . . . 7
β’ 0 =
(0gβπ) |
33 | | archiabllem.e |
. . . . . . 7
β’ β€ =
(leβπ) |
34 | | archiabllem.t |
. . . . . . 7
β’ < =
(ltβπ) |
35 | | archiabllem.a |
. . . . . . 7
β’ (π β π β Archi) |
36 | | archiabllem1.p |
. . . . . . 7
β’ (π β 0 < π) |
37 | | archiabllem1.s |
. . . . . . 7
β’ ((π β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) |
38 | 13, 32, 33, 34, 14, 1, 35, 11, 36, 37 | archiabllem1b 32325 |
. . . . . 6
β’ ((π β§ π§ β π΅) β βπ β β€ π§ = (π Β· π)) |
39 | 29, 31, 38 | syl2anc 584 |
. . . . 5
β’ ((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β βπ β β€ π§ = (π Β· π)) |
40 | 28, 39 | r19.29a 3162 |
. . . 4
β’ ((((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β β€) β§ π¦ = (π Β· π)) β (π¦(+gβπ)π§) = (π§(+gβπ)π¦)) |
41 | 13, 32, 33, 34, 14, 1, 35, 11, 36, 37 | archiabllem1b 32325 |
. . . . 5
β’ ((π β§ π¦ β π΅) β βπ β β€ π¦ = (π Β· π)) |
42 | 41 | adantrr 715 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β βπ β β€ π¦ = (π Β· π)) |
43 | 40, 42 | r19.29a 3162 |
. . 3
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦(+gβπ)π§) = (π§(+gβπ)π¦)) |
44 | 43 | ralrimivva 3200 |
. 2
β’ (π β βπ¦ β π΅ βπ§ β π΅ (π¦(+gβπ)π§) = (π§(+gβπ)π¦)) |
45 | 13, 15 | isabl2 19652 |
. 2
β’ (π β Abel β (π β Grp β§ βπ¦ β π΅ βπ§ β π΅ (π¦(+gβπ)π§) = (π§(+gβπ)π¦))) |
46 | 3, 44, 45 | sylanbrc 583 |
1
β’ (π β π β Abel) |