Step | Hyp | Ref
| Expression |
1 | | fveq2 6891 |
. . . . . 6
β’ (π = π β (Baseβπ) = (Baseβπ)) |
2 | 1 | pweqd 4619 |
. . . . 5
β’ (π = π β π« (Baseβπ) = π« (Baseβπ)) |
3 | | fveq2 6891 |
. . . . . . 7
β’ (π = π β (0gβπ) = (0gβπ)) |
4 | 3 | eleq1d 2818 |
. . . . . 6
β’ (π = π β ((0gβπ) β π‘ β (0gβπ) β π‘)) |
5 | | fveq2 6891 |
. . . . . . . . 9
β’ (π = π β (+gβπ) = (+gβπ)) |
6 | 5 | oveqd 7425 |
. . . . . . . 8
β’ (π = π β (π₯(+gβπ)π¦) = (π₯(+gβπ)π¦)) |
7 | 6 | eleq1d 2818 |
. . . . . . 7
β’ (π = π β ((π₯(+gβπ)π¦) β π‘ β (π₯(+gβπ)π¦) β π‘)) |
8 | 7 | 2ralbidv 3218 |
. . . . . 6
β’ (π = π β (βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘ β βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)) |
9 | 4, 8 | anbi12d 631 |
. . . . 5
β’ (π = π β (((0gβπ) β π‘ β§ βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘) β ((0gβπ) β π‘ β§ βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘))) |
10 | 2, 9 | rabeqbidv 3449 |
. . . 4
β’ (π = π β {π‘ β π« (Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)} = {π‘ β π« (Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)}) |
11 | | df-submnd 18671 |
. . . 4
β’ SubMnd =
(π β Mnd β¦
{π‘ β π«
(Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)}) |
12 | | fvex 6904 |
. . . . . 6
β’
(Baseβπ)
β V |
13 | 12 | pwex 5378 |
. . . . 5
β’ π«
(Baseβπ) β
V |
14 | 13 | rabex 5332 |
. . . 4
β’ {π‘ β π«
(Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)} β V |
15 | 10, 11, 14 | fvmpt 6998 |
. . 3
β’ (π β Mnd β
(SubMndβπ) = {π‘ β π«
(Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)}) |
16 | 15 | eleq2d 2819 |
. 2
β’ (π β Mnd β (π β (SubMndβπ) β π β {π‘ β π« (Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)})) |
17 | | eleq2 2822 |
. . . . 5
β’ (π‘ = π β ((0gβπ) β π‘ β (0gβπ) β π)) |
18 | | eleq2 2822 |
. . . . . . 7
β’ (π‘ = π β ((π₯(+gβπ)π¦) β π‘ β (π₯(+gβπ)π¦) β π)) |
19 | 18 | raleqbi1dv 3333 |
. . . . . 6
β’ (π‘ = π β (βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘ β βπ¦ β π (π₯(+gβπ)π¦) β π)) |
20 | 19 | raleqbi1dv 3333 |
. . . . 5
β’ (π‘ = π β (βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘ β βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π)) |
21 | 17, 20 | anbi12d 631 |
. . . 4
β’ (π‘ = π β (((0gβπ) β π‘ β§ βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘) β ((0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
22 | 21 | elrab 3683 |
. . 3
β’ (π β {π‘ β π« (Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)} β (π β π« (Baseβπ) β§
((0gβπ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
23 | | issubm.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
24 | 23 | sseq2i 4011 |
. . . . 5
β’ (π β π΅ β π β (Baseβπ)) |
25 | | issubm.z |
. . . . . . 7
β’ 0 =
(0gβπ) |
26 | 25 | eleq1i 2824 |
. . . . . 6
β’ ( 0 β π β
(0gβπ)
β π) |
27 | | issubm.p |
. . . . . . . . 9
β’ + =
(+gβπ) |
28 | 27 | oveqi 7421 |
. . . . . . . 8
β’ (π₯ + π¦) = (π₯(+gβπ)π¦) |
29 | 28 | eleq1i 2824 |
. . . . . . 7
β’ ((π₯ + π¦) β π β (π₯(+gβπ)π¦) β π) |
30 | 29 | 2ralbii 3128 |
. . . . . 6
β’
(βπ₯ β
π βπ¦ β π (π₯ + π¦) β π β βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π) |
31 | 26, 30 | anbi12i 627 |
. . . . 5
β’ (( 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π) β ((0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π)) |
32 | 24, 31 | anbi12i 627 |
. . . 4
β’ ((π β π΅ β§ ( 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π)) β (π β (Baseβπ) β§ ((0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
33 | | 3anass 1095 |
. . . 4
β’ ((π β π΅ β§ 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π) β (π β π΅ β§ ( 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π))) |
34 | 12 | elpw2 5345 |
. . . . 5
β’ (π β π«
(Baseβπ) β π β (Baseβπ)) |
35 | 34 | anbi1i 624 |
. . . 4
β’ ((π β π«
(Baseβπ) β§
((0gβπ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π)) β (π β (Baseβπ) β§ ((0gβπ) β π β§ βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π))) |
36 | 32, 33, 35 | 3bitr4ri 303 |
. . 3
β’ ((π β π«
(Baseβπ) β§
((0gβπ)
β π β§
βπ₯ β π βπ¦ β π (π₯(+gβπ)π¦) β π)) β (π β π΅ β§ 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π)) |
37 | 22, 36 | bitri 274 |
. 2
β’ (π β {π‘ β π« (Baseβπ) β£
((0gβπ)
β π‘ β§
βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ)π¦) β π‘)} β (π β π΅ β§ 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π)) |
38 | 16, 37 | bitrdi 286 |
1
β’ (π β Mnd β (π β (SubMndβπ) β (π β π΅ β§ 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π))) |