Step | Hyp | Ref
| Expression |
1 | | gexex.1 |
. . 3
β’ π = (BaseβπΊ) |
2 | | gexex.2 |
. . 3
β’ πΈ = (gExβπΊ) |
3 | | gexex.3 |
. . 3
β’ π = (odβπΊ) |
4 | | simpll 766 |
. . 3
β’ (((πΊ β Abel β§ πΈ β β) β§ (π₯ β π β§ (πβπ₯) = sup(ran π, β, < ))) β πΊ β Abel) |
5 | | simplr 768 |
. . 3
β’ (((πΊ β Abel β§ πΈ β β) β§ (π₯ β π β§ (πβπ₯) = sup(ran π, β, < ))) β πΈ β β) |
6 | | simprl 770 |
. . 3
β’ (((πΊ β Abel β§ πΈ β β) β§ (π₯ β π β§ (πβπ₯) = sup(ran π, β, < ))) β π₯ β π) |
7 | 1, 3 | odf 19326 |
. . . . . . 7
β’ π:πβΆβ0 |
8 | | frn 6680 |
. . . . . . 7
β’ (π:πβΆβ0 β ran π β
β0) |
9 | 7, 8 | ax-mp 5 |
. . . . . 6
β’ ran π β
β0 |
10 | | nn0ssz 12529 |
. . . . . 6
β’
β0 β β€ |
11 | 9, 10 | sstri 3958 |
. . . . 5
β’ ran π β
β€ |
12 | | nnz 12527 |
. . . . . . . 8
β’ (πΈ β β β πΈ β
β€) |
13 | 12 | adantl 483 |
. . . . . . 7
β’ ((πΊ β Abel β§ πΈ β β) β πΈ β
β€) |
14 | | ablgrp 19574 |
. . . . . . . . . . . 12
β’ (πΊ β Abel β πΊ β Grp) |
15 | 14 | adantr 482 |
. . . . . . . . . . 11
β’ ((πΊ β Abel β§ πΈ β β) β πΊ β Grp) |
16 | 1, 2, 3 | gexod 19375 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ π₯ β π) β (πβπ₯) β₯ πΈ) |
17 | 15, 16 | sylan 581 |
. . . . . . . . . 10
β’ (((πΊ β Abel β§ πΈ β β) β§ π₯ β π) β (πβπ₯) β₯ πΈ) |
18 | 1, 3 | odcl 19325 |
. . . . . . . . . . . . 13
β’ (π₯ β π β (πβπ₯) β
β0) |
19 | 18 | adantl 483 |
. . . . . . . . . . . 12
β’ (((πΊ β Abel β§ πΈ β β) β§ π₯ β π) β (πβπ₯) β
β0) |
20 | 19 | nn0zd 12532 |
. . . . . . . . . . 11
β’ (((πΊ β Abel β§ πΈ β β) β§ π₯ β π) β (πβπ₯) β β€) |
21 | | simplr 768 |
. . . . . . . . . . 11
β’ (((πΊ β Abel β§ πΈ β β) β§ π₯ β π) β πΈ β β) |
22 | | dvdsle 16199 |
. . . . . . . . . . 11
β’ (((πβπ₯) β β€ β§ πΈ β β) β ((πβπ₯) β₯ πΈ β (πβπ₯) β€ πΈ)) |
23 | 20, 21, 22 | syl2anc 585 |
. . . . . . . . . 10
β’ (((πΊ β Abel β§ πΈ β β) β§ π₯ β π) β ((πβπ₯) β₯ πΈ β (πβπ₯) β€ πΈ)) |
24 | 17, 23 | mpd 15 |
. . . . . . . . 9
β’ (((πΊ β Abel β§ πΈ β β) β§ π₯ β π) β (πβπ₯) β€ πΈ) |
25 | 24 | ralrimiva 3144 |
. . . . . . . 8
β’ ((πΊ β Abel β§ πΈ β β) β
βπ₯ β π (πβπ₯) β€ πΈ) |
26 | | ffn 6673 |
. . . . . . . . . 10
β’ (π:πβΆβ0 β π Fn π) |
27 | 7, 26 | ax-mp 5 |
. . . . . . . . 9
β’ π Fn π |
28 | | breq1 5113 |
. . . . . . . . . 10
β’ (π¦ = (πβπ₯) β (π¦ β€ πΈ β (πβπ₯) β€ πΈ)) |
29 | 28 | ralrn 7043 |
. . . . . . . . 9
β’ (π Fn π β (βπ¦ β ran π π¦ β€ πΈ β βπ₯ β π (πβπ₯) β€ πΈ)) |
30 | 27, 29 | ax-mp 5 |
. . . . . . . 8
β’
(βπ¦ β
ran π π¦ β€ πΈ β βπ₯ β π (πβπ₯) β€ πΈ) |
31 | 25, 30 | sylibr 233 |
. . . . . . 7
β’ ((πΊ β Abel β§ πΈ β β) β
βπ¦ β ran π π¦ β€ πΈ) |
32 | | brralrspcev 5170 |
. . . . . . 7
β’ ((πΈ β β€ β§
βπ¦ β ran π π¦ β€ πΈ) β βπ β β€ βπ¦ β ran π π¦ β€ π) |
33 | 13, 31, 32 | syl2anc 585 |
. . . . . 6
β’ ((πΊ β Abel β§ πΈ β β) β
βπ β β€
βπ¦ β ran π π¦ β€ π) |
34 | 33 | ad2antrr 725 |
. . . . 5
β’ ((((πΊ β Abel β§ πΈ β β) β§ (π₯ β π β§ (πβπ₯) = sup(ran π, β, < ))) β§ π¦ β π) β βπ β β€ βπ¦ β ran π π¦ β€ π) |
35 | 27 | a1i 11 |
. . . . . 6
β’ (((πΊ β Abel β§ πΈ β β) β§ (π₯ β π β§ (πβπ₯) = sup(ran π, β, < ))) β π Fn π) |
36 | | fnfvelrn 7036 |
. . . . . 6
β’ ((π Fn π β§ π¦ β π) β (πβπ¦) β ran π) |
37 | 35, 36 | sylan 581 |
. . . . 5
β’ ((((πΊ β Abel β§ πΈ β β) β§ (π₯ β π β§ (πβπ₯) = sup(ran π, β, < ))) β§ π¦ β π) β (πβπ¦) β ran π) |
38 | | suprzub 12871 |
. . . . 5
β’ ((ran
π β β€ β§
βπ β β€
βπ¦ β ran π π¦ β€ π β§ (πβπ¦) β ran π) β (πβπ¦) β€ sup(ran π, β, < )) |
39 | 11, 34, 37, 38 | mp3an2i 1467 |
. . . 4
β’ ((((πΊ β Abel β§ πΈ β β) β§ (π₯ β π β§ (πβπ₯) = sup(ran π, β, < ))) β§ π¦ β π) β (πβπ¦) β€ sup(ran π, β, < )) |
40 | | simplrr 777 |
. . . 4
β’ ((((πΊ β Abel β§ πΈ β β) β§ (π₯ β π β§ (πβπ₯) = sup(ran π, β, < ))) β§ π¦ β π) β (πβπ₯) = sup(ran π, β, < )) |
41 | 39, 40 | breqtrrd 5138 |
. . 3
β’ ((((πΊ β Abel β§ πΈ β β) β§ (π₯ β π β§ (πβπ₯) = sup(ran π, β, < ))) β§ π¦ β π) β (πβπ¦) β€ (πβπ₯)) |
42 | 1, 2, 3, 4, 5, 6, 41 | gexexlem 19637 |
. 2
β’ (((πΊ β Abel β§ πΈ β β) β§ (π₯ β π β§ (πβπ₯) = sup(ran π, β, < ))) β (πβπ₯) = πΈ) |
43 | 1 | grpbn0 18786 |
. . . . . 6
β’ (πΊ β Grp β π β β
) |
44 | 15, 43 | syl 17 |
. . . . 5
β’ ((πΊ β Abel β§ πΈ β β) β π β β
) |
45 | 7 | fdmi 6685 |
. . . . . . . 8
β’ dom π = π |
46 | 45 | eqeq1i 2742 |
. . . . . . 7
β’ (dom
π = β
β π = β
) |
47 | | dm0rn0 5885 |
. . . . . . 7
β’ (dom
π = β
β ran
π =
β
) |
48 | 46, 47 | bitr3i 277 |
. . . . . 6
β’ (π = β
β ran π = β
) |
49 | 48 | necon3bii 2997 |
. . . . 5
β’ (π β β
β ran π β β
) |
50 | 44, 49 | sylib 217 |
. . . 4
β’ ((πΊ β Abel β§ πΈ β β) β ran
π β
β
) |
51 | | suprzcl2 12870 |
. . . 4
β’ ((ran
π β β€ β§ ran
π β β
β§
βπ β β€
βπ¦ β ran π π¦ β€ π) β sup(ran π, β, < ) β ran π) |
52 | 11, 50, 33, 51 | mp3an2i 1467 |
. . 3
β’ ((πΊ β Abel β§ πΈ β β) β sup(ran
π, β, < ) β
ran π) |
53 | | fvelrnb 6908 |
. . . 4
β’ (π Fn π β (sup(ran π, β, < ) β ran π β βπ₯ β π (πβπ₯) = sup(ran π, β, < ))) |
54 | 27, 53 | ax-mp 5 |
. . 3
β’ (sup(ran
π, β, < ) β
ran π β βπ₯ β π (πβπ₯) = sup(ran π, β, < )) |
55 | 52, 54 | sylib 217 |
. 2
β’ ((πΊ β Abel β§ πΈ β β) β
βπ₯ β π (πβπ₯) = sup(ran π, β, < )) |
56 | 42, 55 | reximddv 3169 |
1
β’ ((πΊ β Abel β§ πΈ β β) β
βπ₯ β π (πβπ₯) = πΈ) |