Step | Hyp | Ref
| Expression |
1 | | submrcl 18720 |
. . . . . 6
β’ (π΄ β (SubMndβπ) β π β Mnd) |
2 | | eqid 2731 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
3 | | eqid 2731 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
4 | | eqid 2731 |
. . . . . . 7
β’
(.gβπ) = (.gβπ) |
5 | | eqid 2731 |
. . . . . . 7
β’
(leβπ) =
(leβπ) |
6 | | eqid 2731 |
. . . . . . 7
β’
(ltβπ) =
(ltβπ) |
7 | 2, 3, 4, 5, 6 | isarchi2 32598 |
. . . . . 6
β’ ((π β Toset β§ π β Mnd) β (π β Archi β
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)))) |
8 | 1, 7 | sylan2 592 |
. . . . 5
β’ ((π β Toset β§ π΄ β (SubMndβπ)) β (π β Archi β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)))) |
9 | 8 | biimpa 476 |
. . . 4
β’ (((π β Toset β§ π΄ β (SubMndβπ)) β§ π β Archi) β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯))) |
10 | 9 | an32s 649 |
. . 3
β’ (((π β Toset β§ π β Archi) β§ π΄ β (SubMndβπ)) β βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯))) |
11 | | eqid 2731 |
. . . . . . . 8
β’ (π βΎs π΄) = (π βΎs π΄) |
12 | 11 | submbas 18732 |
. . . . . . 7
β’ (π΄ β (SubMndβπ) β π΄ = (Baseβ(π βΎs π΄))) |
13 | 2 | submss 18727 |
. . . . . . 7
β’ (π΄ β (SubMndβπ) β π΄ β (Baseβπ)) |
14 | 12, 13 | eqsstrrd 4022 |
. . . . . 6
β’ (π΄ β (SubMndβπ) β (Baseβ(π βΎs π΄)) β (Baseβπ)) |
15 | | ssralv 4051 |
. . . . . . . 8
β’
((Baseβ(π
βΎs π΄))
β (Baseβπ)
β (βπ¦ β
(Baseβπ)((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β βπ¦ β (Baseβ(π βΎs π΄))((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)))) |
16 | 15 | ralimdv 3168 |
. . . . . . 7
β’
((Baseβ(π
βΎs π΄))
β (Baseβπ)
β (βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β βπ₯ β (Baseβπ)βπ¦ β (Baseβ(π βΎs π΄))((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)))) |
17 | | ssralv 4051 |
. . . . . . 7
β’
((Baseβ(π
βΎs π΄))
β (Baseβπ)
β (βπ₯ β
(Baseβπ)βπ¦ β (Baseβ(π βΎs π΄))((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)))) |
18 | 16, 17 | syld 47 |
. . . . . 6
β’
((Baseβ(π
βΎs π΄))
β (Baseβπ)
β (βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ)((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)))) |
19 | 14, 18 | syl 17 |
. . . . 5
β’ (π΄ β (SubMndβπ) β (βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)))) |
20 | 19 | adantl 481 |
. . . 4
β’ (((π β Toset β§ π β Archi) β§ π΄ β (SubMndβπ)) β (βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)))) |
21 | 11, 3 | subm0 18733 |
. . . . . . . . . 10
β’ (π΄ β (SubMndβπ) β
(0gβπ) =
(0gβ(π
βΎs π΄))) |
22 | 21 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β (0gβπ) = (0gβ(π βΎs π΄))) |
23 | 11, 5 | ressle 17330 |
. . . . . . . . . . . 12
β’ (π΄ β (SubMndβπ) β (leβπ) = (leβ(π βΎs π΄))) |
24 | 23 | difeq1d 4122 |
. . . . . . . . . . 11
β’ (π΄ β (SubMndβπ) β ((leβπ) β I ) =
((leβ(π
βΎs π΄))
β I )) |
25 | 5, 6 | pltfval 18289 |
. . . . . . . . . . . 12
β’ (π β Mnd β
(ltβπ) =
((leβπ) β I
)) |
26 | 1, 25 | syl 17 |
. . . . . . . . . . 11
β’ (π΄ β (SubMndβπ) β (ltβπ) = ((leβπ) β I )) |
27 | 11 | submmnd 18731 |
. . . . . . . . . . . 12
β’ (π΄ β (SubMndβπ) β (π βΎs π΄) β Mnd) |
28 | | eqid 2731 |
. . . . . . . . . . . . 13
β’
(leβ(π
βΎs π΄)) =
(leβ(π
βΎs π΄)) |
29 | | eqid 2731 |
. . . . . . . . . . . . 13
β’
(ltβ(π
βΎs π΄)) =
(ltβ(π
βΎs π΄)) |
30 | 28, 29 | pltfval 18289 |
. . . . . . . . . . . 12
β’ ((π βΎs π΄) β Mnd β
(ltβ(π
βΎs π΄)) =
((leβ(π
βΎs π΄))
β I )) |
31 | 27, 30 | syl 17 |
. . . . . . . . . . 11
β’ (π΄ β (SubMndβπ) β (ltβ(π βΎs π΄)) = ((leβ(π βΎs π΄)) β I )) |
32 | 24, 26, 31 | 3eqtr4d 2781 |
. . . . . . . . . 10
β’ (π΄ β (SubMndβπ) β (ltβπ) = (ltβ(π βΎs π΄))) |
33 | 32 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β (ltβπ) = (ltβ(π βΎs π΄))) |
34 | | eqidd 2732 |
. . . . . . . . 9
β’ (((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β π₯ = π₯) |
35 | 22, 33, 34 | breq123d 5163 |
. . . . . . . 8
β’ (((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β ((0gβπ)(ltβπ)π₯ β (0gβ(π βΎs π΄))(ltβ(π βΎs π΄))π₯)) |
36 | | eqidd 2732 |
. . . . . . . . . 10
β’ ((((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β§ π β β) β π¦ = π¦) |
37 | 23 | ad3antrrr 727 |
. . . . . . . . . 10
β’ ((((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β§ π β β) β (leβπ) = (leβ(π βΎs π΄))) |
38 | | simplll 772 |
. . . . . . . . . . 11
β’ ((((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β§ π β β) β π΄ β (SubMndβπ)) |
39 | | simpr 484 |
. . . . . . . . . . . 12
β’ ((((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β§ π β β) β π β β) |
40 | 39 | nnnn0d 12537 |
. . . . . . . . . . 11
β’ ((((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β§ π β β) β π β β0) |
41 | | simpllr 773 |
. . . . . . . . . . . 12
β’ ((((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β§ π β β) β π₯ β (Baseβ(π βΎs π΄))) |
42 | 38, 12 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β§ π β β) β π΄ = (Baseβ(π βΎs π΄))) |
43 | 41, 42 | eleqtrrd 2835 |
. . . . . . . . . . 11
β’ ((((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β§ π β β) β π₯ β π΄) |
44 | | eqid 2731 |
. . . . . . . . . . . 12
β’
(.gβ(π βΎs π΄)) = (.gβ(π βΎs π΄)) |
45 | 4, 11, 44 | submmulg 19035 |
. . . . . . . . . . 11
β’ ((π΄ β (SubMndβπ) β§ π β β0 β§ π₯ β π΄) β (π(.gβπ)π₯) = (π(.gβ(π βΎs π΄))π₯)) |
46 | 38, 40, 43, 45 | syl3anc 1370 |
. . . . . . . . . 10
β’ ((((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β§ π β β) β (π(.gβπ)π₯) = (π(.gβ(π βΎs π΄))π₯)) |
47 | 36, 37, 46 | breq123d 5163 |
. . . . . . . . 9
β’ ((((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β§ π β β) β (π¦(leβπ)(π(.gβπ)π₯) β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯))) |
48 | 47 | rexbidva 3175 |
. . . . . . . 8
β’ (((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β (βπ β β π¦(leβπ)(π(.gβπ)π₯) β βπ β β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯))) |
49 | 35, 48 | imbi12d 343 |
. . . . . . 7
β’ (((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β§ π¦ β (Baseβ(π βΎs π΄))) β (((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β ((0gβ(π βΎs π΄))(ltβ(π βΎs π΄))π₯ β βπ β β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯)))) |
50 | 49 | ralbidva 3174 |
. . . . . 6
β’ ((π΄ β (SubMndβπ) β§ π₯ β (Baseβ(π βΎs π΄))) β (βπ¦ β (Baseβ(π βΎs π΄))((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β βπ¦ β (Baseβ(π βΎs π΄))((0gβ(π βΎs π΄))(ltβ(π βΎs π΄))π₯ β βπ β β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯)))) |
51 | 50 | ralbidva 3174 |
. . . . 5
β’ (π΄ β (SubMndβπ) β (βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβ(π βΎs π΄))(ltβ(π βΎs π΄))π₯ β βπ β β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯)))) |
52 | 51 | adantl 481 |
. . . 4
β’ (((π β Toset β§ π β Archi) β§ π΄ β (SubMndβπ)) β (βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβ(π βΎs π΄))(ltβ(π βΎs π΄))π₯ β βπ β β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯)))) |
53 | 20, 52 | sylibd 238 |
. . 3
β’ (((π β Toset β§ π β Archi) β§ π΄ β (SubMndβπ)) β (βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)((0gβπ)(ltβπ)π₯ β βπ β β π¦(leβπ)(π(.gβπ)π₯)) β βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβ(π βΎs π΄))(ltβ(π βΎs π΄))π₯ β βπ β β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯)))) |
54 | 10, 53 | mpd 15 |
. 2
β’ (((π β Toset β§ π β Archi) β§ π΄ β (SubMndβπ)) β βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβ(π βΎs π΄))(ltβ(π βΎs π΄))π₯ β βπ β β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯))) |
55 | | resstos 32401 |
. . . 4
β’ ((π β Toset β§ π΄ β (SubMndβπ)) β (π βΎs π΄) β Toset) |
56 | 27 | adantl 481 |
. . . 4
β’ ((π β Toset β§ π΄ β (SubMndβπ)) β (π βΎs π΄) β Mnd) |
57 | | eqid 2731 |
. . . . 5
β’
(Baseβ(π
βΎs π΄)) =
(Baseβ(π
βΎs π΄)) |
58 | | eqid 2731 |
. . . . 5
β’
(0gβ(π βΎs π΄)) = (0gβ(π βΎs π΄)) |
59 | 57, 58, 44, 28, 29 | isarchi2 32598 |
. . . 4
β’ (((π βΎs π΄) β Toset β§ (π βΎs π΄) β Mnd) β ((π βΎs π΄) β Archi β
βπ₯ β
(Baseβ(π
βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβ(π βΎs π΄))(ltβ(π βΎs π΄))π₯ β βπ β β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯)))) |
60 | 55, 56, 59 | syl2anc 583 |
. . 3
β’ ((π β Toset β§ π΄ β (SubMndβπ)) β ((π βΎs π΄) β Archi β βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβ(π βΎs π΄))(ltβ(π βΎs π΄))π₯ β βπ β β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯)))) |
61 | 60 | adantlr 712 |
. 2
β’ (((π β Toset β§ π β Archi) β§ π΄ β (SubMndβπ)) β ((π βΎs π΄) β Archi β βπ₯ β (Baseβ(π βΎs π΄))βπ¦ β (Baseβ(π βΎs π΄))((0gβ(π βΎs π΄))(ltβ(π βΎs π΄))π₯ β βπ β β π¦(leβ(π βΎs π΄))(π(.gβ(π βΎs π΄))π₯)))) |
62 | 54, 61 | mpbird 256 |
1
β’ (((π β Toset β§ π β Archi) β§ π΄ β (SubMndβπ)) β (π βΎs π΄) β Archi) |