Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ») =
(Baseβπ») |
2 | 1 | submss 18625 |
. . . . . . 7
β’ (π΄ β (SubMndβπ») β π΄ β (Baseβπ»)) |
3 | 2 | adantl 483 |
. . . . . 6
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β π΄ β (Baseβπ»)) |
4 | | subsubm.h |
. . . . . . . 8
β’ π» = (πΊ βΎs π) |
5 | 4 | submbas 18630 |
. . . . . . 7
β’ (π β (SubMndβπΊ) β π = (Baseβπ»)) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β π = (Baseβπ»)) |
7 | 3, 6 | sseqtrrd 3986 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β π΄ β π) |
8 | | eqid 2733 |
. . . . . . 7
β’
(BaseβπΊ) =
(BaseβπΊ) |
9 | 8 | submss 18625 |
. . . . . 6
β’ (π β (SubMndβπΊ) β π β (BaseβπΊ)) |
10 | 9 | adantr 482 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β π β (BaseβπΊ)) |
11 | 7, 10 | sstrd 3955 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β π΄ β (BaseβπΊ)) |
12 | | eqid 2733 |
. . . . . . 7
β’
(0gβπΊ) = (0gβπΊ) |
13 | 4, 12 | subm0 18631 |
. . . . . 6
β’ (π β (SubMndβπΊ) β
(0gβπΊ) =
(0gβπ»)) |
14 | 13 | adantr 482 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β (0gβπΊ) = (0gβπ»)) |
15 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ») = (0gβπ») |
16 | 15 | subm0cl 18627 |
. . . . . 6
β’ (π΄ β (SubMndβπ») β
(0gβπ»)
β π΄) |
17 | 16 | adantl 483 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β (0gβπ») β π΄) |
18 | 14, 17 | eqeltrd 2834 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β (0gβπΊ) β π΄) |
19 | 4 | oveq1i 7368 |
. . . . . . 7
β’ (π» βΎs π΄) = ((πΊ βΎs π) βΎs π΄) |
20 | | ressabs 17135 |
. . . . . . 7
β’ ((π β (SubMndβπΊ) β§ π΄ β π) β ((πΊ βΎs π) βΎs π΄) = (πΊ βΎs π΄)) |
21 | 19, 20 | eqtrid 2785 |
. . . . . 6
β’ ((π β (SubMndβπΊ) β§ π΄ β π) β (π» βΎs π΄) = (πΊ βΎs π΄)) |
22 | 7, 21 | syldan 592 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β (π» βΎs π΄) = (πΊ βΎs π΄)) |
23 | | eqid 2733 |
. . . . . . 7
β’ (π» βΎs π΄) = (π» βΎs π΄) |
24 | 23 | submmnd 18629 |
. . . . . 6
β’ (π΄ β (SubMndβπ») β (π» βΎs π΄) β Mnd) |
25 | 24 | adantl 483 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β (π» βΎs π΄) β Mnd) |
26 | 22, 25 | eqeltrrd 2835 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β (πΊ βΎs π΄) β Mnd) |
27 | | submrcl 18618 |
. . . . . 6
β’ (π β (SubMndβπΊ) β πΊ β Mnd) |
28 | 27 | adantr 482 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β πΊ β Mnd) |
29 | | eqid 2733 |
. . . . . 6
β’ (πΊ βΎs π΄) = (πΊ βΎs π΄) |
30 | 8, 12, 29 | issubm2 18620 |
. . . . 5
β’ (πΊ β Mnd β (π΄ β (SubMndβπΊ) β (π΄ β (BaseβπΊ) β§ (0gβπΊ) β π΄ β§ (πΊ βΎs π΄) β Mnd))) |
31 | 28, 30 | syl 17 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β (π΄ β (SubMndβπΊ) β (π΄ β (BaseβπΊ) β§ (0gβπΊ) β π΄ β§ (πΊ βΎs π΄) β Mnd))) |
32 | 11, 18, 26, 31 | mpbir3and 1343 |
. . 3
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β π΄ β (SubMndβπΊ)) |
33 | 32, 7 | jca 513 |
. 2
β’ ((π β (SubMndβπΊ) β§ π΄ β (SubMndβπ»)) β (π΄ β (SubMndβπΊ) β§ π΄ β π)) |
34 | | simprr 772 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β π΄ β π) |
35 | 5 | adantr 482 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β π = (Baseβπ»)) |
36 | 34, 35 | sseqtrd 3985 |
. . 3
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β π΄ β (Baseβπ»)) |
37 | 13 | adantr 482 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β (0gβπΊ) = (0gβπ»)) |
38 | 12 | subm0cl 18627 |
. . . . 5
β’ (π΄ β (SubMndβπΊ) β
(0gβπΊ)
β π΄) |
39 | 38 | ad2antrl 727 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β (0gβπΊ) β π΄) |
40 | 37, 39 | eqeltrrd 2835 |
. . 3
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β (0gβπ») β π΄) |
41 | 21 | adantrl 715 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β (π» βΎs π΄) = (πΊ βΎs π΄)) |
42 | 29 | submmnd 18629 |
. . . . 5
β’ (π΄ β (SubMndβπΊ) β (πΊ βΎs π΄) β Mnd) |
43 | 42 | ad2antrl 727 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β (πΊ βΎs π΄) β Mnd) |
44 | 41, 43 | eqeltrd 2834 |
. . 3
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β (π» βΎs π΄) β Mnd) |
45 | 4 | submmnd 18629 |
. . . . 5
β’ (π β (SubMndβπΊ) β π» β Mnd) |
46 | 45 | adantr 482 |
. . . 4
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β π» β Mnd) |
47 | 1, 15, 23 | issubm2 18620 |
. . . 4
β’ (π» β Mnd β (π΄ β (SubMndβπ») β (π΄ β (Baseβπ») β§ (0gβπ») β π΄ β§ (π» βΎs π΄) β Mnd))) |
48 | 46, 47 | syl 17 |
. . 3
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β (π΄ β (SubMndβπ») β (π΄ β (Baseβπ») β§ (0gβπ») β π΄ β§ (π» βΎs π΄) β Mnd))) |
49 | 36, 40, 44, 48 | mpbir3and 1343 |
. 2
β’ ((π β (SubMndβπΊ) β§ (π΄ β (SubMndβπΊ) β§ π΄ β π)) β π΄ β (SubMndβπ»)) |
50 | 33, 49 | impbida 800 |
1
β’ (π β (SubMndβπΊ) β (π΄ β (SubMndβπ») β (π΄ β (SubMndβπΊ) β§ π΄ β π))) |