Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . 5
β’
β²βπ |
2 | | vex 3448 |
. . . . . . . 8
β’ β β V |
3 | 2 | mptex 7174 |
. . . . . . 7
β’ (π₯ β β β¦ ({π₯} β π)) β V |
4 | 3 | rnex 7850 |
. . . . . 6
β’ ran
(π₯ β β β¦ ({π₯} β π)) β V |
5 | 4 | a1i 11 |
. . . . 5
β’ ((π β§ β β π) β ran (π₯ β β β¦ ({π₯} β π)) β V) |
6 | | nsgmgc.e |
. . . . 5
β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) |
7 | 1, 5, 6 | fnmptd 6643 |
. . . 4
β’ (π β πΈ Fn π) |
8 | | nsgmgc.b |
. . . . . . . 8
β’ π΅ = (BaseβπΊ) |
9 | | nsgmgc.q |
. . . . . . . 8
β’ π = (πΊ /s (πΊ ~QG π)) |
10 | | nsgmgc.p |
. . . . . . . 8
β’ β =
(LSSumβπΊ) |
11 | | mpteq1 5199 |
. . . . . . . . . . 11
β’ (β = π β (π₯ β β β¦ ({π₯} β π)) = (π₯ β π β¦ ({π₯} β π))) |
12 | 11 | rneqd 5894 |
. . . . . . . . . 10
β’ (β = π β ran (π₯ β β β¦ ({π₯} β π)) = ran (π₯ β π β¦ ({π₯} β π))) |
13 | 12 | cbvmptv 5219 |
. . . . . . . . 9
β’ (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) = (π β π β¦ ran (π₯ β π β¦ ({π₯} β π))) |
14 | 6, 13 | eqtri 2761 |
. . . . . . . 8
β’ πΈ = (π β π β¦ ran (π₯ β π β¦ ({π₯} β π))) |
15 | | eqid 2733 |
. . . . . . . 8
β’ (π₯ β π΅ β¦ [π₯](πΊ ~QG π)) = (π₯ β π΅ β¦ [π₯](πΊ ~QG π)) |
16 | | nsgmgc.n |
. . . . . . . . 9
β’ (π β π β (NrmSGrpβπΊ)) |
17 | 16 | adantr 482 |
. . . . . . . 8
β’ ((π β§ β β π) β π β (NrmSGrpβπΊ)) |
18 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ β β π) β β β π) |
19 | | nsgmgc.s |
. . . . . . . . . 10
β’ π = {β β (SubGrpβπΊ) β£ π β β} |
20 | 19 | ssrab3 4041 |
. . . . . . . . 9
β’ π β (SubGrpβπΊ) |
21 | 20 | a1i 11 |
. . . . . . . 8
β’ ((π β§ β β π) β π β (SubGrpβπΊ)) |
22 | 8, 9, 10, 14, 15, 17, 18, 21 | qusima 32235 |
. . . . . . 7
β’ ((π β§ β β π) β (πΈββ) = ((π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β β)) |
23 | 8, 9, 15 | qusghm 19050 |
. . . . . . . . 9
β’ (π β (NrmSGrpβπΊ) β (π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β (πΊ GrpHom π)) |
24 | 17, 23 | syl 17 |
. . . . . . . 8
β’ ((π β§ β β π) β (π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β (πΊ GrpHom π)) |
25 | 20 | a1i 11 |
. . . . . . . . 9
β’ (π β π β (SubGrpβπΊ)) |
26 | 25 | sselda 3945 |
. . . . . . . 8
β’ ((π β§ β β π) β β β (SubGrpβπΊ)) |
27 | | ghmima 19034 |
. . . . . . . 8
β’ (((π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β (πΊ GrpHom π) β§ β β (SubGrpβπΊ)) β ((π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β β) β (SubGrpβπ)) |
28 | 24, 26, 27 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ β β π) β ((π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β β) β (SubGrpβπ)) |
29 | 22, 28 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ β β π) β (πΈββ) β (SubGrpβπ)) |
30 | | nsgmgc.t |
. . . . . 6
β’ π = (SubGrpβπ) |
31 | 29, 30 | eleqtrrdi 2845 |
. . . . 5
β’ ((π β§ β β π) β (πΈββ) β π) |
32 | 31 | ralrimiva 3140 |
. . . 4
β’ (π β ββ β π (πΈββ) β π) |
33 | | ffnfv 7067 |
. . . 4
β’ (πΈ:πβΆπ β (πΈ Fn π β§ ββ β π (πΈββ) β π)) |
34 | 7, 32, 33 | sylanbrc 584 |
. . 3
β’ (π β πΈ:πβΆπ) |
35 | | sseq2 3971 |
. . . . . 6
β’ (β = {π β π΅ β£ ({π} β π) β π} β (π β β β π β {π β π΅ β£ ({π} β π) β π})) |
36 | 16 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β π β (NrmSGrpβπΊ)) |
37 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
38 | 37, 30 | eleqtrdi 2844 |
. . . . . . 7
β’ ((π β§ π β π) β π β (SubGrpβπ)) |
39 | 8, 9, 10, 36, 38 | nsgmgclem 32237 |
. . . . . 6
β’ ((π β§ π β π) β {π β π΅ β£ ({π} β π) β π} β (SubGrpβπΊ)) |
40 | | nsgsubg 18965 |
. . . . . . . . . 10
β’ (π β (NrmSGrpβπΊ) β π β (SubGrpβπΊ)) |
41 | 16, 40 | syl 17 |
. . . . . . . . 9
β’ (π β π β (SubGrpβπΊ)) |
42 | 8 | subgss 18934 |
. . . . . . . . 9
β’ (π β (SubGrpβπΊ) β π β π΅) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
β’ (π β π β π΅) |
44 | 43 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β π β π΅) |
45 | 41 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π) β π β (SubGrpβπΊ)) |
46 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π) β π β π) |
47 | 10 | grplsmid 32233 |
. . . . . . . . 9
β’ ((π β (SubGrpβπΊ) β§ π β π) β ({π} β π) = π) |
48 | 45, 46, 47 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β π) β ({π} β π) = π) |
49 | 16 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π) β π β (NrmSGrpβπΊ)) |
50 | 38 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π) β π β (SubGrpβπ)) |
51 | 9 | nsgqus0 32236 |
. . . . . . . . 9
β’ ((π β (NrmSGrpβπΊ) β§ π β (SubGrpβπ)) β π β π) |
52 | 49, 50, 51 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β π) β π β π) |
53 | 48, 52 | eqeltrd 2834 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β π) β ({π} β π) β π) |
54 | 44, 53 | ssrabdv 4032 |
. . . . . 6
β’ ((π β§ π β π) β π β {π β π΅ β£ ({π} β π) β π}) |
55 | 35, 39, 54 | elrabd 3648 |
. . . . 5
β’ ((π β§ π β π) β {π β π΅ β£ ({π} β π) β π} β {β β (SubGrpβπΊ) β£ π β β}) |
56 | 55, 19 | eleqtrrdi 2845 |
. . . 4
β’ ((π β§ π β π) β {π β π΅ β£ ({π} β π) β π} β π) |
57 | | nsgmgc.f |
. . . 4
β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) |
58 | 56, 57 | fmptd 7063 |
. . 3
β’ (π β πΉ:πβΆπ) |
59 | 34, 58 | jca 513 |
. 2
β’ (π β (πΈ:πβΆπ β§ πΉ:πβΆπ)) |
60 | 8 | subgss 18934 |
. . . . . . . . . 10
β’ (β β (SubGrpβπΊ) β β β π΅) |
61 | 26, 60 | syl 17 |
. . . . . . . . 9
β’ ((π β§ β β π) β β β π΅) |
62 | 61 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β β β π΅) |
63 | 6 | fvmpt2 6960 |
. . . . . . . . . . . 12
β’ ((β β π β§ ran (π₯ β β β¦ ({π₯} β π)) β V) β (πΈββ) = ran (π₯ β β β¦ ({π₯} β π))) |
64 | 18, 4, 63 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β§ β β π) β (πΈββ) = ran (π₯ β β β¦ ({π₯} β π))) |
65 | 64 | ad5ant12 755 |
. . . . . . . . . 10
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β (πΈββ) = ran (π₯ β β β¦ ({π₯} β π))) |
66 | | simplr 768 |
. . . . . . . . . 10
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β (πΈββ) β π) |
67 | 65, 66 | eqsstrrd 3984 |
. . . . . . . . 9
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β ran (π₯ β β β¦ ({π₯} β π)) β π) |
68 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β β β¦ ({π₯} β π)) = (π₯ β β β¦ ({π₯} β π)) |
69 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β π β β) |
70 | | sneq 4597 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β {π₯} = {π}) |
71 | 70 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ({π₯} β π) = ({π} β π)) |
72 | 71 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π₯ = π β (({π} β π) = ({π₯} β π) β ({π} β π) = ({π} β π))) |
73 | 72 | adantl 483 |
. . . . . . . . . . 11
β’
((((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β§ π₯ = π) β (({π} β π) = ({π₯} β π) β ({π} β π) = ({π} β π))) |
74 | | eqidd 2734 |
. . . . . . . . . . 11
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β ({π} β π) = ({π} β π)) |
75 | 69, 73, 74 | rspcedvd 3582 |
. . . . . . . . . 10
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β βπ₯ β β ({π} β π) = ({π₯} β π)) |
76 | | ovexd 7393 |
. . . . . . . . . 10
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β ({π} β π) β V) |
77 | 68, 75, 76 | elrnmptd 5917 |
. . . . . . . . 9
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))) |
78 | 67, 77 | sseldd 3946 |
. . . . . . . 8
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β ({π} β π) β π) |
79 | 62, 78 | ssrabdv 4032 |
. . . . . . 7
β’ ((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β β β {π β π΅ β£ ({π} β π) β π}) |
80 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ β β π) β§ π β π) β π β π) |
81 | 8 | fvexi 6857 |
. . . . . . . . . 10
β’ π΅ β V |
82 | 81 | rabex 5290 |
. . . . . . . . 9
β’ {π β π΅ β£ ({π} β π) β π} β V |
83 | 57 | fvmpt2 6960 |
. . . . . . . . 9
β’ ((π β π β§ {π β π΅ β£ ({π} β π) β π} β V) β (πΉβπ) = {π β π΅ β£ ({π} β π) β π}) |
84 | 80, 82, 83 | sylancl 587 |
. . . . . . . 8
β’ (((π β§ β β π) β§ π β π) β (πΉβπ) = {π β π΅ β£ ({π} β π) β π}) |
85 | 84 | adantr 482 |
. . . . . . 7
β’ ((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β (πΉβπ) = {π β π΅ β£ ({π} β π) β π}) |
86 | 79, 85 | sseqtrrd 3986 |
. . . . . 6
β’ ((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β β β (πΉβπ)) |
87 | 64 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β (πΈββ) = ran (π₯ β β β¦ ({π₯} β π))) |
88 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β β β (πΉβπ)) |
89 | 88 | sselda 3945 |
. . . . . . . . . . 11
β’
(((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β§ π₯ β β) β π₯ β (πΉβπ)) |
90 | 84 | ad2antrr 725 |
. . . . . . . . . . 11
β’
(((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β§ π₯ β β) β (πΉβπ) = {π β π΅ β£ ({π} β π) β π}) |
91 | 89, 90 | eleqtrd 2836 |
. . . . . . . . . 10
β’
(((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β§ π₯ β β) β π₯ β {π β π΅ β£ ({π} β π) β π}) |
92 | | sneq 4597 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β {π} = {π₯}) |
93 | 92 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (π = π₯ β ({π} β π) = ({π₯} β π)) |
94 | 93 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = π₯ β (({π} β π) β π β ({π₯} β π) β π)) |
95 | 94 | elrab 3646 |
. . . . . . . . . . 11
β’ (π₯ β {π β π΅ β£ ({π} β π) β π} β (π₯ β π΅ β§ ({π₯} β π) β π)) |
96 | 95 | simprbi 498 |
. . . . . . . . . 10
β’ (π₯ β {π β π΅ β£ ({π} β π) β π} β ({π₯} β π) β π) |
97 | 91, 96 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β§ π₯ β β) β ({π₯} β π) β π) |
98 | 97 | ralrimiva 3140 |
. . . . . . . 8
β’ ((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β βπ₯ β β ({π₯} β π) β π) |
99 | 68 | rnmptss 7071 |
. . . . . . . 8
β’
(βπ₯ β
β ({π₯} β π) β π β ran (π₯ β β β¦ ({π₯} β π)) β π) |
100 | 98, 99 | syl 17 |
. . . . . . 7
β’ ((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β ran (π₯ β β β¦ ({π₯} β π)) β π) |
101 | 87, 100 | eqsstrd 3983 |
. . . . . 6
β’ ((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β (πΈββ) β π) |
102 | 86, 101 | impbida 800 |
. . . . 5
β’ (((π β§ β β π) β§ π β π) β ((πΈββ) β π β β β (πΉβπ))) |
103 | 30 | fvexi 6857 |
. . . . . 6
β’ π β V |
104 | | nsgmgc.w |
. . . . . . 7
β’ π = (toIncβπ) |
105 | | eqid 2733 |
. . . . . . 7
β’
(leβπ) =
(leβπ) |
106 | 104, 105 | ipole 18428 |
. . . . . 6
β’ ((π β V β§ (πΈββ) β π β§ π β π) β ((πΈββ)(leβπ)π β (πΈββ) β π)) |
107 | 103, 31, 80, 106 | mp3an2ani 1469 |
. . . . 5
β’ (((π β§ β β π) β§ π β π) β ((πΈββ)(leβπ)π β (πΈββ) β π)) |
108 | | fvex 6856 |
. . . . . . 7
β’
(SubGrpβπΊ)
β V |
109 | 19, 108 | rabex2 5292 |
. . . . . 6
β’ π β V |
110 | 58 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) β π) |
111 | 110 | adantlr 714 |
. . . . . 6
β’ (((π β§ β β π) β§ π β π) β (πΉβπ) β π) |
112 | | nsgmgc.v |
. . . . . . 7
β’ π = (toIncβπ) |
113 | | eqid 2733 |
. . . . . . 7
β’
(leβπ) =
(leβπ) |
114 | 112, 113 | ipole 18428 |
. . . . . 6
β’ ((π β V β§ β β π β§ (πΉβπ) β π) β (β(leβπ)(πΉβπ) β β β (πΉβπ))) |
115 | 109, 18, 111, 114 | mp3an2ani 1469 |
. . . . 5
β’ (((π β§ β β π) β§ π β π) β (β(leβπ)(πΉβπ) β β β (πΉβπ))) |
116 | 102, 107,
115 | 3bitr4d 311 |
. . . 4
β’ (((π β§ β β π) β§ π β π) β ((πΈββ)(leβπ)π β β(leβπ)(πΉβπ))) |
117 | 116 | anasss 468 |
. . 3
β’ ((π β§ (β β π β§ π β π)) β ((πΈββ)(leβπ)π β β(leβπ)(πΉβπ))) |
118 | 117 | ralrimivva 3194 |
. 2
β’ (π β ββ β π βπ β π ((πΈββ)(leβπ)π β β(leβπ)(πΉβπ))) |
119 | 112 | ipobas 18425 |
. . . 4
β’ (π β V β π = (Baseβπ)) |
120 | 109, 119 | ax-mp 5 |
. . 3
β’ π = (Baseβπ) |
121 | 104 | ipobas 18425 |
. . . 4
β’ (π β V β π = (Baseβπ)) |
122 | 103, 121 | ax-mp 5 |
. . 3
β’ π = (Baseβπ) |
123 | | nsgmgc.j |
. . 3
β’ π½ = (πMGalConnπ) |
124 | 112 | ipopos 18430 |
. . . 4
β’ π β Poset |
125 | | posprs 18210 |
. . . 4
β’ (π β Poset β π β Proset
) |
126 | 124, 125 | mp1i 13 |
. . 3
β’ (π β π β Proset ) |
127 | 104 | ipopos 18430 |
. . . 4
β’ π β Poset |
128 | | posprs 18210 |
. . . 4
β’ (π β Poset β π β Proset
) |
129 | 127, 128 | mp1i 13 |
. . 3
β’ (π β π β Proset ) |
130 | 120, 122,
113, 105, 123, 126, 129 | mgcval 31896 |
. 2
β’ (π β (πΈπ½πΉ β ((πΈ:πβΆπ β§ πΉ:πβΆπ) β§ ββ β π βπ β π ((πΈββ)(leβπ)π β β(leβπ)(πΉβπ))))) |
131 | 59, 118, 130 | mpbir2and 712 |
1
β’ (π β πΈπ½πΉ) |