Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . 7
β’ (((π β§ β β π) β§ π = ran (π₯ β β β¦ ({π₯} β π))) β π = ran (π₯ β β β¦ ({π₯} β π))) |
2 | | nsgqusf1o.s |
. . . . . . . . . 10
β’ π = {β β (SubGrpβπΊ) β£ π β β} |
3 | 2 | reqabi 3455 |
. . . . . . . . 9
β’ (β β π β (β β (SubGrpβπΊ) β§ π β β)) |
4 | | nsgqusf1o.b |
. . . . . . . . . . . 12
β’ π΅ = (BaseβπΊ) |
5 | | nsgqusf1o.t |
. . . . . . . . . . . 12
β’ π = (SubGrpβπ) |
6 | | nsgqusf1o.1 |
. . . . . . . . . . . 12
β’ β€ =
(leβ(toIncβπ)) |
7 | | nsgqusf1o.2 |
. . . . . . . . . . . 12
β’ β² =
(leβ(toIncβπ)) |
8 | | nsgqusf1o.q |
. . . . . . . . . . . 12
β’ π = (πΊ /s (πΊ ~QG π)) |
9 | | nsgqusf1o.p |
. . . . . . . . . . . 12
β’ β =
(LSSumβπΊ) |
10 | | nsgqusf1o.e |
. . . . . . . . . . . 12
β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) |
11 | | nsgqusf1o.f |
. . . . . . . . . . . 12
β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) |
12 | | nsgqusf1o.n |
. . . . . . . . . . . 12
β’ (π β π β (NrmSGrpβπΊ)) |
13 | 4, 2, 5, 6, 7, 8, 9, 10, 11, 12 | nsgqusf1olem1 32524 |
. . . . . . . . . . 11
β’ (((π β§ β β (SubGrpβπΊ)) β§ π β β) β ran (π₯ β β β¦ ({π₯} β π)) β π) |
14 | 13 | anasss 468 |
. . . . . . . . . 10
β’ ((π β§ (β β (SubGrpβπΊ) β§ π β β)) β ran (π₯ β β β¦ ({π₯} β π)) β π) |
15 | 14, 5 | eleqtrdi 2844 |
. . . . . . . . 9
β’ ((π β§ (β β (SubGrpβπΊ) β§ π β β)) β ran (π₯ β β β¦ ({π₯} β π)) β (SubGrpβπ)) |
16 | 3, 15 | sylan2b 595 |
. . . . . . . 8
β’ ((π β§ β β π) β ran (π₯ β β β¦ ({π₯} β π)) β (SubGrpβπ)) |
17 | 16 | adantr 482 |
. . . . . . 7
β’ (((π β§ β β π) β§ π = ran (π₯ β β β¦ ({π₯} β π))) β ran (π₯ β β β¦ ({π₯} β π)) β (SubGrpβπ)) |
18 | 1, 17 | eqeltrd 2834 |
. . . . . 6
β’ (((π β§ β β π) β§ π = ran (π₯ β β β¦ ({π₯} β π))) β π β (SubGrpβπ)) |
19 | 18 | r19.29an 3159 |
. . . . 5
β’ ((π β§ ββ β π π = ran (π₯ β β β¦ ({π₯} β π))) β π β (SubGrpβπ)) |
20 | | sseq2 4009 |
. . . . . . . 8
β’ (β = {π β π΅ β£ ({π} β π) β π} β (π β β β π β {π β π΅ β£ ({π} β π) β π})) |
21 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (SubGrpβπ)) β π β (NrmSGrpβπΊ)) |
22 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β (SubGrpβπ)) β π β (SubGrpβπ)) |
23 | 4, 8, 9, 21, 22 | nsgmgclem 32522 |
. . . . . . . 8
β’ ((π β§ π β (SubGrpβπ)) β {π β π΅ β£ ({π} β π) β π} β (SubGrpβπΊ)) |
24 | 5 | eleq2i 2826 |
. . . . . . . . 9
β’ (π β π β π β (SubGrpβπ)) |
25 | | nsgsubg 19038 |
. . . . . . . . . . . . 13
β’ (π β (NrmSGrpβπΊ) β π β (SubGrpβπΊ)) |
26 | 12, 25 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β (SubGrpβπΊ)) |
27 | 4 | subgss 19007 |
. . . . . . . . . . . 12
β’ (π β (SubGrpβπΊ) β π β π΅) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β π΅) |
29 | 28 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π΅) |
30 | 26 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β π) β π β (SubGrpβπΊ)) |
31 | 9 | grplsmid 32514 |
. . . . . . . . . . . 12
β’ ((π β (SubGrpβπΊ) β§ π β π) β ({π} β π) = π) |
32 | 30, 31 | sylancom 589 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π) β ({π} β π) = π) |
33 | 24 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π β π β π β (SubGrpβπ)) |
34 | 8 | nsgqus0 32521 |
. . . . . . . . . . . . 13
β’ ((π β (NrmSGrpβπΊ) β§ π β (SubGrpβπ)) β π β π) |
35 | 12, 33, 34 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π β π) |
36 | 35 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π) β π β π) |
37 | 32, 36 | eqeltrd 2834 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β π) β ({π} β π) β π) |
38 | 29, 37 | ssrabdv 4072 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β {π β π΅ β£ ({π} β π) β π}) |
39 | 24, 38 | sylan2br 596 |
. . . . . . . 8
β’ ((π β§ π β (SubGrpβπ)) β π β {π β π΅ β£ ({π} β π) β π}) |
40 | 20, 23, 39 | elrabd 3686 |
. . . . . . 7
β’ ((π β§ π β (SubGrpβπ)) β {π β π΅ β£ ({π} β π) β π} β {β β (SubGrpβπΊ) β£ π β β}) |
41 | 40, 2 | eleqtrrdi 2845 |
. . . . . 6
β’ ((π β§ π β (SubGrpβπ)) β {π β π΅ β£ ({π} β π) β π} β π) |
42 | | mpteq1 5242 |
. . . . . . . . 9
β’ (β = {π β π΅ β£ ({π} β π) β π} β (π₯ β β β¦ ({π₯} β π)) = (π₯ β {π β π΅ β£ ({π} β π) β π} β¦ ({π₯} β π))) |
43 | 42 | rneqd 5938 |
. . . . . . . 8
β’ (β = {π β π΅ β£ ({π} β π) β π} β ran (π₯ β β β¦ ({π₯} β π)) = ran (π₯ β {π β π΅ β£ ({π} β π) β π} β¦ ({π₯} β π))) |
44 | 43 | eqeq2d 2744 |
. . . . . . 7
β’ (β = {π β π΅ β£ ({π} β π) β π} β (π = ran (π₯ β β β¦ ({π₯} β π)) β π = ran (π₯ β {π β π΅ β£ ({π} β π) β π} β¦ ({π₯} β π)))) |
45 | 44 | adantl 483 |
. . . . . 6
β’ (((π β§ π β (SubGrpβπ)) β§ β = {π β π΅ β£ ({π} β π) β π}) β (π = ran (π₯ β β β¦ ({π₯} β π)) β π = ran (π₯ β {π β π΅ β£ ({π} β π) β π} β¦ ({π₯} β π)))) |
46 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(Baseβπ) =
(Baseβπ) |
47 | 46 | subgss 19007 |
. . . . . . . . . . . . . 14
β’ (π β (SubGrpβπ) β π β (Baseβπ)) |
48 | 47 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (SubGrpβπ)) β π β (Baseβπ)) |
49 | 48 | sselda 3983 |
. . . . . . . . . . . 12
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β π β (Baseβπ)) |
50 | 8 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β π = (πΊ /s (πΊ ~QG π))) |
51 | 4 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β π΅ = (BaseβπΊ)) |
52 | | ovexd 7444 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β (πΊ ~QG π) β V) |
53 | | subgrcl 19011 |
. . . . . . . . . . . . . . 15
β’ (π β (SubGrpβπΊ) β πΊ β Grp) |
54 | 26, 53 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΊ β Grp) |
55 | 54 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β πΊ β Grp) |
56 | 50, 51, 52, 55 | qusbas 17491 |
. . . . . . . . . . . 12
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β (π΅ / (πΊ ~QG π)) = (Baseβπ)) |
57 | 49, 56 | eleqtrrd 2837 |
. . . . . . . . . . 11
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β π β (π΅ / (πΊ ~QG π))) |
58 | | elqsi 8764 |
. . . . . . . . . . 11
β’ (π β (π΅ / (πΊ ~QG π)) β βπ₯ β π΅ π = [π₯](πΊ ~QG π)) |
59 | 57, 58 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β βπ₯ β π΅ π = [π₯](πΊ ~QG π)) |
60 | | sneq 4639 |
. . . . . . . . . . . . . . . 16
β’ (π = π₯ β {π} = {π₯}) |
61 | 60 | oveq1d 7424 |
. . . . . . . . . . . . . . 15
β’ (π = π₯ β ({π} β π) = ({π₯} β π)) |
62 | 61 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β (({π} β π) β π β ({π₯} β π) β π)) |
63 | | simplr 768 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (SubGrpβπ)) β§ π β π) β§ π₯ β π΅) β§ π = [π₯](πΊ ~QG π)) β π₯ β π΅) |
64 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (SubGrpβπ)) β§ π β π) β§ π₯ β π΅) β§ π = [π₯](πΊ ~QG π)) β π = [π₯](πΊ ~QG π)) |
65 | 26 | ad4antr 731 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β (SubGrpβπ)) β§ π β π) β§ π₯ β π΅) β§ π = [π₯](πΊ ~QG π)) β π β (SubGrpβπΊ)) |
66 | 4, 9, 65, 63 | quslsm 32516 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (SubGrpβπ)) β§ π β π) β§ π₯ β π΅) β§ π = [π₯](πΊ ~QG π)) β [π₯](πΊ ~QG π) = ({π₯} β π)) |
67 | 64, 66 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (SubGrpβπ)) β§ π β π) β§ π₯ β π΅) β§ π = [π₯](πΊ ~QG π)) β π = ({π₯} β π)) |
68 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (SubGrpβπ)) β§ π β π) β§ π₯ β π΅) β§ π = [π₯](πΊ ~QG π)) β π β π) |
69 | 67, 68 | eqeltrrd 2835 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (SubGrpβπ)) β§ π β π) β§ π₯ β π΅) β§ π = [π₯](πΊ ~QG π)) β ({π₯} β π) β π) |
70 | 62, 63, 69 | elrabd 3686 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (SubGrpβπ)) β§ π β π) β§ π₯ β π΅) β§ π = [π₯](πΊ ~QG π)) β π₯ β {π β π΅ β£ ({π} β π) β π}) |
71 | 70, 67 | jca 513 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (SubGrpβπ)) β§ π β π) β§ π₯ β π΅) β§ π = [π₯](πΊ ~QG π)) β (π₯ β {π β π΅ β£ ({π} β π) β π} β§ π = ({π₯} β π))) |
72 | 71 | expl 459 |
. . . . . . . . . . 11
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β ((π₯ β π΅ β§ π = [π₯](πΊ ~QG π)) β (π₯ β {π β π΅ β£ ({π} β π) β π} β§ π = ({π₯} β π)))) |
73 | 72 | reximdv2 3165 |
. . . . . . . . . 10
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β (βπ₯ β π΅ π = [π₯](πΊ ~QG π) β βπ₯ β {π β π΅ β£ ({π} β π) β π}π = ({π₯} β π))) |
74 | 59, 73 | mpd 15 |
. . . . . . . . 9
β’ (((π β§ π β (SubGrpβπ)) β§ π β π) β βπ₯ β {π β π΅ β£ ({π} β π) β π}π = ({π₯} β π)) |
75 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (SubGrpβπ)) β§ π₯ β {π β π΅ β£ ({π} β π) β π}) β§ π = ({π₯} β π)) β π₯ β {π β π΅ β£ ({π} β π) β π}) |
76 | 62 | elrab 3684 |
. . . . . . . . . . . 12
β’ (π₯ β {π β π΅ β£ ({π} β π) β π} β (π₯ β π΅ β§ ({π₯} β π) β π)) |
77 | 75, 76 | sylib 217 |
. . . . . . . . . . 11
β’ ((((π β§ π β (SubGrpβπ)) β§ π₯ β {π β π΅ β£ ({π} β π) β π}) β§ π = ({π₯} β π)) β (π₯ β π΅ β§ ({π₯} β π) β π)) |
78 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (SubGrpβπ)) β§ π = ({π₯} β π)) β§ π₯ β π΅) β§ ({π₯} β π) β π) β π = ({π₯} β π)) |
79 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (SubGrpβπ)) β§ π = ({π₯} β π)) β§ π₯ β π΅) β§ ({π₯} β π) β π) β ({π₯} β π) β π) |
80 | 78, 79 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (SubGrpβπ)) β§ π = ({π₯} β π)) β§ π₯ β π΅) β§ ({π₯} β π) β π) β π β π) |
81 | 80 | anasss 468 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (SubGrpβπ)) β§ π = ({π₯} β π)) β§ (π₯ β π΅ β§ ({π₯} β π) β π)) β π β π) |
82 | 81 | adantllr 718 |
. . . . . . . . . . 11
β’
(((((π β§ π β (SubGrpβπ)) β§ π₯ β {π β π΅ β£ ({π} β π) β π}) β§ π = ({π₯} β π)) β§ (π₯ β π΅ β§ ({π₯} β π) β π)) β π β π) |
83 | 77, 82 | mpdan 686 |
. . . . . . . . . 10
β’ ((((π β§ π β (SubGrpβπ)) β§ π₯ β {π β π΅ β£ ({π} β π) β π}) β§ π = ({π₯} β π)) β π β π) |
84 | 83 | r19.29an 3159 |
. . . . . . . . 9
β’ (((π β§ π β (SubGrpβπ)) β§ βπ₯ β {π β π΅ β£ ({π} β π) β π}π = ({π₯} β π)) β π β π) |
85 | 74, 84 | impbida 800 |
. . . . . . . 8
β’ ((π β§ π β (SubGrpβπ)) β (π β π β βπ₯ β {π β π΅ β£ ({π} β π) β π}π = ({π₯} β π))) |
86 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β {π β π΅ β£ ({π} β π) β π} β¦ ({π₯} β π)) = (π₯ β {π β π΅ β£ ({π} β π) β π} β¦ ({π₯} β π)) |
87 | 86 | elrnmpt 5956 |
. . . . . . . . 9
β’ (π β V β (π β ran (π₯ β {π β π΅ β£ ({π} β π) β π} β¦ ({π₯} β π)) β βπ₯ β {π β π΅ β£ ({π} β π) β π}π = ({π₯} β π))) |
88 | 87 | elv 3481 |
. . . . . . . 8
β’ (π β ran (π₯ β {π β π΅ β£ ({π} β π) β π} β¦ ({π₯} β π)) β βπ₯ β {π β π΅ β£ ({π} β π) β π}π = ({π₯} β π)) |
89 | 85, 88 | bitr4di 289 |
. . . . . . 7
β’ ((π β§ π β (SubGrpβπ)) β (π β π β π β ran (π₯ β {π β π΅ β£ ({π} β π) β π} β¦ ({π₯} β π)))) |
90 | 89 | eqrdv 2731 |
. . . . . 6
β’ ((π β§ π β (SubGrpβπ)) β π = ran (π₯ β {π β π΅ β£ ({π} β π) β π} β¦ ({π₯} β π))) |
91 | 41, 45, 90 | rspcedvd 3615 |
. . . . 5
β’ ((π β§ π β (SubGrpβπ)) β ββ β π π = ran (π₯ β β β¦ ({π₯} β π))) |
92 | 19, 91 | impbida 800 |
. . . 4
β’ (π β (ββ β π π = ran (π₯ β β β¦ ({π₯} β π)) β π β (SubGrpβπ))) |
93 | 92 | abbidv 2802 |
. . 3
β’ (π β {π β£ ββ β π π = ran (π₯ β β β¦ ({π₯} β π))} = {π β£ π β (SubGrpβπ)}) |
94 | 10 | rnmpt 5955 |
. . 3
β’ ran πΈ = {π β£ ββ β π π = ran (π₯ β β β¦ ({π₯} β π))} |
95 | | abid1 2871 |
. . 3
β’
(SubGrpβπ) =
{π β£ π β (SubGrpβπ)} |
96 | 93, 94, 95 | 3eqtr4g 2798 |
. 2
β’ (π β ran πΈ = (SubGrpβπ)) |
97 | 96, 5 | eqtr4di 2791 |
1
β’ (π β ran πΈ = π) |