Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (Baseβπ) = (Baseβπ)) |
2 | 1 | pweqd 4578 |
. . . . 5
β’ (π = π β π« (Baseβπ) = π« (Baseβπ)) |
3 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (0gβπ) = (0gβπ)) |
4 | 3 | eleq1d 2819 |
. . . . . 6
β’ (π = π β ((0gβπ) β π‘ β (0gβπ) β π‘)) |
5 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π β (+gβπ) = (+gβπ)) |
6 | 5 | oveqd 7375 |
. . . . . . . 8
β’ (π = π β (π₯(+gβπ)π¦) = (π₯(+gβπ)π¦)) |
7 | 6 | eleq1d 2819 |
. . . . . . 7
β’ (π = π β ((π₯(+gβπ)π¦) β π‘ β (π₯(+gβπ)π¦) β π‘)) |
8 | 7 | 2ralbidv 3209 |
. . . . . 6
β’ (π = π β (βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘ β βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)) |
9 | 4, 8 | anbi12d 632 |
. . . . 5
β’ (π = π β (((0gβπ) β π‘ β§ βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘) β ((0gβπ) β π‘ β§ βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘))) |
10 | 2, 9 | rabeqbidv 3423 |
. . . 4
β’ (π = π β {π‘ β π« (Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)} = {π‘ β π« (Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)}) |
11 | | df-submnd 18607 |
. . . 4
β’ SubMnd =
(π β Mnd β¦
{π‘ β π«
(Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)}) |
12 | | fvex 6856 |
. . . . . 6
β’
(Baseβπ)
β V |
13 | 12 | pwex 5336 |
. . . . 5
β’ π«
(Baseβπ) β
V |
14 | 13 | rabex 5290 |
. . . 4
β’ {π‘ β π«
(Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)} β V |
15 | 10, 11, 14 | fvmpt 6949 |
. . 3
β’ (π β Mnd β
(SubMndβπ) = {π‘ β π«
(Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)}) |
16 | 15 | eleq2d 2820 |
. 2
β’ (π β Mnd β (π β (SubMndβπ) β π β {π‘ β π« (Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)})) |
17 | | eleq2 2823 |
. . . . 5
β’ (π‘ = π β ((0gβπ) β π‘ β (0gβπ) β π)) |
18 | | eleq2 2823 |
. . . . . . 7
β’ (π‘ = π β ((π₯(+gβπ)π¦) β π‘ β (π₯(+gβπ)π¦) β π)) |
19 | 18 | raleqbi1dv 3306 |
. . . . . 6
β’ (π‘ = π β (βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘ β βπ¦ β π (π₯(+gβπ)π¦) β π)) |
20 | 19 | raleqbi1dv 3306 |
. . . . 5
β’ (π‘ = π β (βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘ β βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π)) |
21 | 17, 20 | anbi12d 632 |
. . . 4
β’ (π‘ = π β (((0gβπ) β π‘ β§ βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘) β ((0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
22 | 21 | elrab 3646 |
. . 3
β’ (π β {π‘ β π« (Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)} β (π β π« (Baseβπ) β§
((0gβπ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
23 | | issubm.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
24 | 23 | sseq2i 3974 |
. . . . 5
β’ (π β π΅ β π β (Baseβπ)) |
25 | | issubm.z |
. . . . . . 7
β’ 0 =
(0gβπ) |
26 | 25 | eleq1i 2825 |
. . . . . 6
β’ ( 0 β π β
(0gβπ)
β π) |
27 | | issubm.p |
. . . . . . . . 9
β’ + =
(+gβπ) |
28 | 27 | oveqi 7371 |
. . . . . . . 8
β’ (π₯ + π¦) = (π₯(+gβπ)π¦) |
29 | 28 | eleq1i 2825 |
. . . . . . 7
β’ ((π₯ + π¦) β π β (π₯(+gβπ)π¦) β π) |
30 | 29 | 2ralbii 3124 |
. . . . . 6
β’
(βπ₯ β
π βπ¦ β π (π₯ + π¦) β π β βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π) |
31 | 26, 30 | anbi12i 628 |
. . . . 5
β’ (( 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π) β ((0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π)) |
32 | 24, 31 | anbi12i 628 |
. . . 4
β’ ((π β π΅ β§ ( 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π)) β (π β (Baseβπ) β§ ((0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
33 | | 3anass 1096 |
. . . 4
β’ ((π β π΅ β§ 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π) β (π β π΅ β§ ( 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π))) |
34 | 12 | elpw2 5303 |
. . . . 5
β’ (π β π«
(Baseβπ) β π β (Baseβπ)) |
35 | 34 | anbi1i 625 |
. . . 4
β’ ((π β π«
(Baseβπ) β§
((0gβπ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π)) β (π β (Baseβπ) β§ ((0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
36 | 32, 33, 35 | 3bitr4ri 304 |
. . 3
β’ ((π β π«
(Baseβπ) β§
((0gβπ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π)) β (π β π΅ β§ 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π)) |
37 | 22, 36 | bitri 275 |
. 2
β’ (π β {π‘ β π« (Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)} β (π β π΅ β§ 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π)) |
38 | 16, 37 | bitrdi 287 |
1
β’ (π β Mnd β (π β (SubMndβπ) β (π β π΅ β§ 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π))) |