Step | Hyp | Ref
| Expression |
1 | | nfv 1916 |
. . . . 5
β’
β²βπ |
2 | | vex 3477 |
. . . . . . . 8
β’ β β V |
3 | 2 | mptex 7227 |
. . . . . . 7
β’ (π₯ β β β¦ ({π₯} β π)) β V |
4 | 3 | rnex 7907 |
. . . . . 6
β’ ran
(π₯ β β β¦ ({π₯} β π)) β V |
5 | 4 | a1i 11 |
. . . . 5
β’ ((π β§ β β π) β ran (π₯ β β β¦ ({π₯} β π)) β V) |
6 | | nsgmgc.e |
. . . . 5
β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) |
7 | 1, 5, 6 | fnmptd 6691 |
. . . 4
β’ (π β πΈ Fn π) |
8 | | nsgmgc.b |
. . . . . . . 8
β’ π΅ = (BaseβπΊ) |
9 | | nsgmgc.q |
. . . . . . . 8
β’ π = (πΊ /s (πΊ ~QG π)) |
10 | | nsgmgc.p |
. . . . . . . 8
β’ β =
(LSSumβπΊ) |
11 | | mpteq1 5241 |
. . . . . . . . . . 11
β’ (β = π β (π₯ β β β¦ ({π₯} β π)) = (π₯ β π β¦ ({π₯} β π))) |
12 | 11 | rneqd 5937 |
. . . . . . . . . 10
β’ (β = π β ran (π₯ β β β¦ ({π₯} β π)) = ran (π₯ β π β¦ ({π₯} β π))) |
13 | 12 | cbvmptv 5261 |
. . . . . . . . 9
β’ (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) = (π β π β¦ ran (π₯ β π β¦ ({π₯} β π))) |
14 | 6, 13 | eqtri 2759 |
. . . . . . . 8
β’ πΈ = (π β π β¦ ran (π₯ β π β¦ ({π₯} β π))) |
15 | | eqid 2731 |
. . . . . . . 8
β’ (π₯ β π΅ β¦ [π₯](πΊ ~QG π)) = (π₯ β π΅ β¦ [π₯](πΊ ~QG π)) |
16 | | nsgmgc.n |
. . . . . . . . 9
β’ (π β π β (NrmSGrpβπΊ)) |
17 | 16 | adantr 480 |
. . . . . . . 8
β’ ((π β§ β β π) β π β (NrmSGrpβπΊ)) |
18 | | simpr 484 |
. . . . . . . 8
β’ ((π β§ β β π) β β β π) |
19 | | nsgmgc.s |
. . . . . . . . . 10
β’ π = {β β (SubGrpβπΊ) β£ π β β} |
20 | 19 | ssrab3 4080 |
. . . . . . . . 9
β’ π β (SubGrpβπΊ) |
21 | 20 | a1i 11 |
. . . . . . . 8
β’ ((π β§ β β π) β π β (SubGrpβπΊ)) |
22 | 8, 9, 10, 14, 15, 17, 18, 21 | qusima 32959 |
. . . . . . 7
β’ ((π β§ β β π) β (πΈββ) = ((π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β β)) |
23 | 8, 9, 15 | qusghm 19176 |
. . . . . . . . 9
β’ (π β (NrmSGrpβπΊ) β (π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β (πΊ GrpHom π)) |
24 | 17, 23 | syl 17 |
. . . . . . . 8
β’ ((π β§ β β π) β (π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β (πΊ GrpHom π)) |
25 | 20 | a1i 11 |
. . . . . . . . 9
β’ (π β π β (SubGrpβπΊ)) |
26 | 25 | sselda 3982 |
. . . . . . . 8
β’ ((π β§ β β π) β β β (SubGrpβπΊ)) |
27 | | ghmima 19158 |
. . . . . . . 8
β’ (((π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β (πΊ GrpHom π) β§ β β (SubGrpβπΊ)) β ((π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β β) β (SubGrpβπ)) |
28 | 24, 26, 27 | syl2anc 583 |
. . . . . . 7
β’ ((π β§ β β π) β ((π₯ β π΅ β¦ [π₯](πΊ ~QG π)) β β) β (SubGrpβπ)) |
29 | 22, 28 | eqeltrd 2832 |
. . . . . 6
β’ ((π β§ β β π) β (πΈββ) β (SubGrpβπ)) |
30 | | nsgmgc.t |
. . . . . 6
β’ π = (SubGrpβπ) |
31 | 29, 30 | eleqtrrdi 2843 |
. . . . 5
β’ ((π β§ β β π) β (πΈββ) β π) |
32 | 31 | ralrimiva 3145 |
. . . 4
β’ (π β ββ β π (πΈββ) β π) |
33 | | ffnfv 7120 |
. . . 4
β’ (πΈ:πβΆπ β (πΈ Fn π β§ ββ β π (πΈββ) β π)) |
34 | 7, 32, 33 | sylanbrc 582 |
. . 3
β’ (π β πΈ:πβΆπ) |
35 | | sseq2 4008 |
. . . . . 6
β’ (β = {π β π΅ β£ ({π} β π) β π} β (π β β β π β {π β π΅ β£ ({π} β π) β π})) |
36 | 16 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β π) β π β (NrmSGrpβπΊ)) |
37 | | simpr 484 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
38 | 37, 30 | eleqtrdi 2842 |
. . . . . . 7
β’ ((π β§ π β π) β π β (SubGrpβπ)) |
39 | 8, 9, 10, 36, 38 | nsgmgclem 32962 |
. . . . . 6
β’ ((π β§ π β π) β {π β π΅ β£ ({π} β π) β π} β (SubGrpβπΊ)) |
40 | | nsgsubg 19081 |
. . . . . . . . . 10
β’ (π β (NrmSGrpβπΊ) β π β (SubGrpβπΊ)) |
41 | 16, 40 | syl 17 |
. . . . . . . . 9
β’ (π β π β (SubGrpβπΊ)) |
42 | 8 | subgss 19050 |
. . . . . . . . 9
β’ (π β (SubGrpβπΊ) β π β π΅) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
β’ (π β π β π΅) |
44 | 43 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β π) β π β π΅) |
45 | 41 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π) β π β (SubGrpβπΊ)) |
46 | | simpr 484 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π) β π β π) |
47 | 10 | grplsmid 32954 |
. . . . . . . . 9
β’ ((π β (SubGrpβπΊ) β§ π β π) β ({π} β π) = π) |
48 | 45, 46, 47 | syl2anc 583 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β π) β ({π} β π) = π) |
49 | 16 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π) β π β (NrmSGrpβπΊ)) |
50 | 38 | adantr 480 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β π) β π β (SubGrpβπ)) |
51 | 9 | nsgqus0 32961 |
. . . . . . . . 9
β’ ((π β (NrmSGrpβπΊ) β§ π β (SubGrpβπ)) β π β π) |
52 | 49, 50, 51 | syl2anc 583 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β π) β π β π) |
53 | 48, 52 | eqeltrd 2832 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β π) β ({π} β π) β π) |
54 | 44, 53 | ssrabdv 4071 |
. . . . . 6
β’ ((π β§ π β π) β π β {π β π΅ β£ ({π} β π) β π}) |
55 | 35, 39, 54 | elrabd 3685 |
. . . . 5
β’ ((π β§ π β π) β {π β π΅ β£ ({π} β π) β π} β {β β (SubGrpβπΊ) β£ π β β}) |
56 | 55, 19 | eleqtrrdi 2843 |
. . . 4
β’ ((π β§ π β π) β {π β π΅ β£ ({π} β π) β π} β π) |
57 | | nsgmgc.f |
. . . 4
β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) |
58 | 56, 57 | fmptd 7115 |
. . 3
β’ (π β πΉ:πβΆπ) |
59 | 34, 58 | jca 511 |
. 2
β’ (π β (πΈ:πβΆπ β§ πΉ:πβΆπ)) |
60 | 8 | subgss 19050 |
. . . . . . . . . 10
β’ (β β (SubGrpβπΊ) β β β π΅) |
61 | 26, 60 | syl 17 |
. . . . . . . . 9
β’ ((π β§ β β π) β β β π΅) |
62 | 61 | ad2antrr 723 |
. . . . . . . 8
β’ ((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β β β π΅) |
63 | 6 | fvmpt2 7009 |
. . . . . . . . . . . 12
β’ ((β β π β§ ran (π₯ β β β¦ ({π₯} β π)) β V) β (πΈββ) = ran (π₯ β β β¦ ({π₯} β π))) |
64 | 18, 4, 63 | sylancl 585 |
. . . . . . . . . . 11
β’ ((π β§ β β π) β (πΈββ) = ran (π₯ β β β¦ ({π₯} β π))) |
65 | 64 | ad5ant12 753 |
. . . . . . . . . 10
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β (πΈββ) = ran (π₯ β β β¦ ({π₯} β π))) |
66 | | simplr 766 |
. . . . . . . . . 10
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β (πΈββ) β π) |
67 | 65, 66 | eqsstrrd 4021 |
. . . . . . . . 9
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β ran (π₯ β β β¦ ({π₯} β π)) β π) |
68 | | eqid 2731 |
. . . . . . . . . 10
β’ (π₯ β β β¦ ({π₯} β π)) = (π₯ β β β¦ ({π₯} β π)) |
69 | | simpr 484 |
. . . . . . . . . . 11
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β π β β) |
70 | | sneq 4638 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β {π₯} = {π}) |
71 | 70 | oveq1d 7427 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ({π₯} β π) = ({π} β π)) |
72 | 71 | eqeq2d 2742 |
. . . . . . . . . . . 12
β’ (π₯ = π β (({π} β π) = ({π₯} β π) β ({π} β π) = ({π} β π))) |
73 | 72 | adantl 481 |
. . . . . . . . . . 11
β’
((((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β§ π₯ = π) β (({π} β π) = ({π₯} β π) β ({π} β π) = ({π} β π))) |
74 | | eqidd 2732 |
. . . . . . . . . . 11
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β ({π} β π) = ({π} β π)) |
75 | 69, 73, 74 | rspcedvd 3614 |
. . . . . . . . . 10
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β βπ₯ β β ({π} β π) = ({π₯} β π)) |
76 | | ovexd 7447 |
. . . . . . . . . 10
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β ({π} β π) β V) |
77 | 68, 75, 76 | elrnmptd 5960 |
. . . . . . . . 9
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))) |
78 | 67, 77 | sseldd 3983 |
. . . . . . . 8
β’
(((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β§ π β β) β ({π} β π) β π) |
79 | 62, 78 | ssrabdv 4071 |
. . . . . . 7
β’ ((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β β β {π β π΅ β£ ({π} β π) β π}) |
80 | | simpr 484 |
. . . . . . . . 9
β’ (((π β§ β β π) β§ π β π) β π β π) |
81 | 8 | fvexi 6905 |
. . . . . . . . . 10
β’ π΅ β V |
82 | 81 | rabex 5332 |
. . . . . . . . 9
β’ {π β π΅ β£ ({π} β π) β π} β V |
83 | 57 | fvmpt2 7009 |
. . . . . . . . 9
β’ ((π β π β§ {π β π΅ β£ ({π} β π) β π} β V) β (πΉβπ) = {π β π΅ β£ ({π} β π) β π}) |
84 | 80, 82, 83 | sylancl 585 |
. . . . . . . 8
β’ (((π β§ β β π) β§ π β π) β (πΉβπ) = {π β π΅ β£ ({π} β π) β π}) |
85 | 84 | adantr 480 |
. . . . . . 7
β’ ((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β (πΉβπ) = {π β π΅ β£ ({π} β π) β π}) |
86 | 79, 85 | sseqtrrd 4023 |
. . . . . 6
β’ ((((π β§ β β π) β§ π β π) β§ (πΈββ) β π) β β β (πΉβπ)) |
87 | 64 | ad2antrr 723 |
. . . . . . 7
β’ ((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β (πΈββ) = ran (π₯ β β β¦ ({π₯} β π))) |
88 | | simpr 484 |
. . . . . . . . . . . 12
β’ ((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β β β (πΉβπ)) |
89 | 88 | sselda 3982 |
. . . . . . . . . . 11
β’
(((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β§ π₯ β β) β π₯ β (πΉβπ)) |
90 | 84 | ad2antrr 723 |
. . . . . . . . . . 11
β’
(((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β§ π₯ β β) β (πΉβπ) = {π β π΅ β£ ({π} β π) β π}) |
91 | 89, 90 | eleqtrd 2834 |
. . . . . . . . . 10
β’
(((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β§ π₯ β β) β π₯ β {π β π΅ β£ ({π} β π) β π}) |
92 | | sneq 4638 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β {π} = {π₯}) |
93 | 92 | oveq1d 7427 |
. . . . . . . . . . . . 13
β’ (π = π₯ β ({π} β π) = ({π₯} β π)) |
94 | 93 | eleq1d 2817 |
. . . . . . . . . . . 12
β’ (π = π₯ β (({π} β π) β π β ({π₯} β π) β π)) |
95 | 94 | elrab 3683 |
. . . . . . . . . . 11
β’ (π₯ β {π β π΅ β£ ({π} β π) β π} β (π₯ β π΅ β§ ({π₯} β π) β π)) |
96 | 95 | simprbi 496 |
. . . . . . . . . 10
β’ (π₯ β {π β π΅ β£ ({π} β π) β π} β ({π₯} β π) β π) |
97 | 91, 96 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β§ π₯ β β) β ({π₯} β π) β π) |
98 | 97 | ralrimiva 3145 |
. . . . . . . 8
β’ ((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β βπ₯ β β ({π₯} β π) β π) |
99 | 68 | rnmptss 7124 |
. . . . . . . 8
β’
(βπ₯ β
β ({π₯} β π) β π β ran (π₯ β β β¦ ({π₯} β π)) β π) |
100 | 98, 99 | syl 17 |
. . . . . . 7
β’ ((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β ran (π₯ β β β¦ ({π₯} β π)) β π) |
101 | 87, 100 | eqsstrd 4020 |
. . . . . 6
β’ ((((π β§ β β π) β§ π β π) β§ β β (πΉβπ)) β (πΈββ) β π) |
102 | 86, 101 | impbida 798 |
. . . . 5
β’ (((π β§ β β π) β§ π β π) β ((πΈββ) β π β β β (πΉβπ))) |
103 | 30 | fvexi 6905 |
. . . . . 6
β’ π β V |
104 | | nsgmgc.w |
. . . . . . 7
β’ π = (toIncβπ) |
105 | | eqid 2731 |
. . . . . . 7
β’
(leβπ) =
(leβπ) |
106 | 104, 105 | ipole 18497 |
. . . . . 6
β’ ((π β V β§ (πΈββ) β π β§ π β π) β ((πΈββ)(leβπ)π β (πΈββ) β π)) |
107 | 103, 31, 80, 106 | mp3an2ani 1467 |
. . . . 5
β’ (((π β§ β β π) β§ π β π) β ((πΈββ)(leβπ)π β (πΈββ) β π)) |
108 | | fvex 6904 |
. . . . . . 7
β’
(SubGrpβπΊ)
β V |
109 | 19, 108 | rabex2 5334 |
. . . . . 6
β’ π β V |
110 | 58 | ffvelcdmda 7086 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) β π) |
111 | 110 | adantlr 712 |
. . . . . 6
β’ (((π β§ β β π) β§ π β π) β (πΉβπ) β π) |
112 | | nsgmgc.v |
. . . . . . 7
β’ π = (toIncβπ) |
113 | | eqid 2731 |
. . . . . . 7
β’
(leβπ) =
(leβπ) |
114 | 112, 113 | ipole 18497 |
. . . . . 6
β’ ((π β V β§ β β π β§ (πΉβπ) β π) β (β(leβπ)(πΉβπ) β β β (πΉβπ))) |
115 | 109, 18, 111, 114 | mp3an2ani 1467 |
. . . . 5
β’ (((π β§ β β π) β§ π β π) β (β(leβπ)(πΉβπ) β β β (πΉβπ))) |
116 | 102, 107,
115 | 3bitr4d 311 |
. . . 4
β’ (((π β§ β β π) β§ π β π) β ((πΈββ)(leβπ)π β β(leβπ)(πΉβπ))) |
117 | 116 | anasss 466 |
. . 3
β’ ((π β§ (β β π β§ π β π)) β ((πΈββ)(leβπ)π β β(leβπ)(πΉβπ))) |
118 | 117 | ralrimivva 3199 |
. 2
β’ (π β ββ β π βπ β π ((πΈββ)(leβπ)π β β(leβπ)(πΉβπ))) |
119 | 112 | ipobas 18494 |
. . . 4
β’ (π β V β π = (Baseβπ)) |
120 | 109, 119 | ax-mp 5 |
. . 3
β’ π = (Baseβπ) |
121 | 104 | ipobas 18494 |
. . . 4
β’ (π β V β π = (Baseβπ)) |
122 | 103, 121 | ax-mp 5 |
. . 3
β’ π = (Baseβπ) |
123 | | nsgmgc.j |
. . 3
β’ π½ = (πMGalConnπ) |
124 | 112 | ipopos 18499 |
. . . 4
β’ π β Poset |
125 | | posprs 18279 |
. . . 4
β’ (π β Poset β π β Proset
) |
126 | 124, 125 | mp1i 13 |
. . 3
β’ (π β π β Proset ) |
127 | 104 | ipopos 18499 |
. . . 4
β’ π β Poset |
128 | | posprs 18279 |
. . . 4
β’ (π β Poset β π β Proset
) |
129 | 127, 128 | mp1i 13 |
. . 3
β’ (π β π β Proset ) |
130 | 120, 122,
113, 105, 123, 126, 129 | mgcval 32590 |
. 2
β’ (π β (πΈπ½πΉ β ((πΈ:πβΆπ β§ πΉ:πβΆπ) β§ ββ β π βπ β π ((πΈββ)(leβπ)π β β(leβπ)(πΉβπ))))) |
131 | 59, 118, 130 | mpbir2and 710 |
1
β’ (π β πΈπ½πΉ) |