Step | Hyp | Ref
| Expression |
1 | | finodsubmsubg.s |
. 2
β’ (π β π β (SubMndβπΊ)) |
2 | | finodsubmsubg.1 |
. . 3
β’ (π β βπ β π (πβπ) β β) |
3 | | eqid 2732 |
. . . . . . . 8
β’
(BaseβπΊ) =
(BaseβπΊ) |
4 | | finodsubmsubg.o |
. . . . . . . 8
β’ π = (odβπΊ) |
5 | | eqid 2732 |
. . . . . . . 8
β’
(.gβπΊ) = (.gβπΊ) |
6 | | eqid 2732 |
. . . . . . . 8
β’
(invgβπΊ) = (invgβπΊ) |
7 | | finodsubmsubg.g |
. . . . . . . . 9
β’ (π β πΊ β Grp) |
8 | 7 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β π) β πΊ β Grp) |
9 | 3 | submss 18686 |
. . . . . . . . . 10
β’ (π β (SubMndβπΊ) β π β (BaseβπΊ)) |
10 | 1, 9 | syl 17 |
. . . . . . . . 9
β’ (π β π β (BaseβπΊ)) |
11 | 10 | sselda 3981 |
. . . . . . . 8
β’ ((π β§ π β π) β π β (BaseβπΊ)) |
12 | 3, 4, 5, 6, 8, 11 | odm1inv 19415 |
. . . . . . 7
β’ ((π β§ π β π) β (((πβπ) β 1)(.gβπΊ)π) = ((invgβπΊ)βπ)) |
13 | 12 | adantr 481 |
. . . . . 6
β’ (((π β§ π β π) β§ (πβπ) β β) β (((πβπ) β 1)(.gβπΊ)π) = ((invgβπΊ)βπ)) |
14 | | eqid 2732 |
. . . . . . . 8
β’
(Baseβ(πΊ
βΎs π)) =
(Baseβ(πΊ
βΎs π)) |
15 | | eqid 2732 |
. . . . . . . 8
β’
(.gβ(πΊ βΎs π)) = (.gβ(πΊ βΎs π)) |
16 | | eqid 2732 |
. . . . . . . . . . 11
β’ (πΊ βΎs π) = (πΊ βΎs π) |
17 | 16 | submmnd 18690 |
. . . . . . . . . 10
β’ (π β (SubMndβπΊ) β (πΊ βΎs π) β Mnd) |
18 | 1, 17 | syl 17 |
. . . . . . . . 9
β’ (π β (πΊ βΎs π) β Mnd) |
19 | 18 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (πβπ) β β) β (πΊ βΎs π) β Mnd) |
20 | | nnm1nn0 12509 |
. . . . . . . . 9
β’ ((πβπ) β β β ((πβπ) β 1) β
β0) |
21 | 20 | adantl 482 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (πβπ) β β) β ((πβπ) β 1) β
β0) |
22 | | simplr 767 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (πβπ) β β) β π β π) |
23 | 16, 3 | ressbas2 17178 |
. . . . . . . . . . 11
β’ (π β (BaseβπΊ) β π = (Baseβ(πΊ βΎs π))) |
24 | 10, 23 | syl 17 |
. . . . . . . . . 10
β’ (π β π = (Baseβ(πΊ βΎs π))) |
25 | 24 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (πβπ) β β) β π = (Baseβ(πΊ βΎs π))) |
26 | 22, 25 | eleqtrd 2835 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (πβπ) β β) β π β (Baseβ(πΊ βΎs π))) |
27 | 14, 15, 19, 21, 26 | mulgnn0cld 18969 |
. . . . . . 7
β’ (((π β§ π β π) β§ (πβπ) β β) β (((πβπ) β 1)(.gβ(πΊ βΎs π))π) β (Baseβ(πΊ βΎs π))) |
28 | 1 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (πβπ) β β) β π β (SubMndβπΊ)) |
29 | 5, 16, 15 | submmulg 18992 |
. . . . . . . 8
β’ ((π β (SubMndβπΊ) β§ ((πβπ) β 1) β β0 β§
π β π) β (((πβπ) β 1)(.gβπΊ)π) = (((πβπ) β 1)(.gβ(πΊ βΎs π))π)) |
30 | 28, 21, 22, 29 | syl3anc 1371 |
. . . . . . 7
β’ (((π β§ π β π) β§ (πβπ) β β) β (((πβπ) β 1)(.gβπΊ)π) = (((πβπ) β 1)(.gβ(πΊ βΎs π))π)) |
31 | 27, 30, 25 | 3eltr4d 2848 |
. . . . . 6
β’ (((π β§ π β π) β§ (πβπ) β β) β (((πβπ) β 1)(.gβπΊ)π) β π) |
32 | 13, 31 | eqeltrrd 2834 |
. . . . 5
β’ (((π β§ π β π) β§ (πβπ) β β) β
((invgβπΊ)βπ) β π) |
33 | 32 | ex 413 |
. . . 4
β’ ((π β§ π β π) β ((πβπ) β β β
((invgβπΊ)βπ) β π)) |
34 | 33 | ralimdva 3167 |
. . 3
β’ (π β (βπ β π (πβπ) β β β βπ β π ((invgβπΊ)βπ) β π)) |
35 | 2, 34 | mpd 15 |
. 2
β’ (π β βπ β π ((invgβπΊ)βπ) β π) |
36 | 6 | issubg3 19018 |
. . 3
β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β (SubMndβπΊ) β§ βπ β π ((invgβπΊ)βπ) β π))) |
37 | 7, 36 | syl 17 |
. 2
β’ (π β (π β (SubGrpβπΊ) β (π β (SubMndβπΊ) β§ βπ β π ((invgβπΊ)βπ) β π))) |
38 | 1, 35, 37 | mpbir2and 711 |
1
β’ (π β π β (SubGrpβπΊ)) |