Step | Hyp | Ref
| Expression |
1 | | rrgval.e |
. 2
β’ πΈ = (RLRegβπ
) |
2 | | fveq2 6843 |
. . . . . 6
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
3 | | rrgval.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
4 | 2, 3 | eqtr4di 2791 |
. . . . 5
β’ (π = π
β (Baseβπ) = π΅) |
5 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π
β (.rβπ) = (.rβπ
)) |
6 | | rrgval.t |
. . . . . . . . . 10
β’ Β· =
(.rβπ
) |
7 | 5, 6 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π = π
β (.rβπ) = Β· ) |
8 | 7 | oveqd 7375 |
. . . . . . . 8
β’ (π = π
β (π₯(.rβπ)π¦) = (π₯ Β· π¦)) |
9 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π
β (0gβπ) = (0gβπ
)) |
10 | | rrgval.z |
. . . . . . . . 9
β’ 0 =
(0gβπ
) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = π
β (0gβπ) = 0 ) |
12 | 8, 11 | eqeq12d 2749 |
. . . . . . 7
β’ (π = π
β ((π₯(.rβπ)π¦) = (0gβπ) β (π₯ Β· π¦) = 0 )) |
13 | 11 | eqeq2d 2744 |
. . . . . . 7
β’ (π = π
β (π¦ = (0gβπ) β π¦ = 0 )) |
14 | 12, 13 | imbi12d 345 |
. . . . . 6
β’ (π = π
β (((π₯(.rβπ)π¦) = (0gβπ) β π¦ = (0gβπ)) β ((π₯ Β· π¦) = 0 β π¦ = 0 ))) |
15 | 4, 14 | raleqbidv 3318 |
. . . . 5
β’ (π = π
β (βπ¦ β (Baseβπ)((π₯(.rβπ)π¦) = (0gβπ) β π¦ = (0gβπ)) β βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 ))) |
16 | 4, 15 | rabeqbidv 3423 |
. . . 4
β’ (π = π
β {π₯ β (Baseβπ) β£ βπ¦ β (Baseβπ)((π₯(.rβπ)π¦) = (0gβπ) β π¦ = (0gβπ))} = {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )}) |
17 | | df-rlreg 20769 |
. . . 4
β’ RLReg =
(π β V β¦ {π₯ β (Baseβπ) β£ βπ¦ β (Baseβπ)((π₯(.rβπ)π¦) = (0gβπ) β π¦ = (0gβπ))}) |
18 | 3 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
19 | 18 | rabex 5290 |
. . . 4
β’ {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )} β
V |
20 | 16, 17, 19 | fvmpt 6949 |
. . 3
β’ (π
β V β
(RLRegβπ
) = {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )}) |
21 | | fvprc 6835 |
. . . 4
β’ (Β¬
π
β V β
(RLRegβπ
) =
β
) |
22 | | fvprc 6835 |
. . . . . . 7
β’ (Β¬
π
β V β
(Baseβπ
) =
β
) |
23 | 3, 22 | eqtrid 2785 |
. . . . . 6
β’ (Β¬
π
β V β π΅ = β
) |
24 | 23 | rabeqdv 3421 |
. . . . 5
β’ (Β¬
π
β V β {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )} = {π₯ β β
β£ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )}) |
25 | | rab0 4343 |
. . . . 5
β’ {π₯ β β
β£
βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )} =
β
|
26 | 24, 25 | eqtrdi 2789 |
. . . 4
β’ (Β¬
π
β V β {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )} =
β
) |
27 | 21, 26 | eqtr4d 2776 |
. . 3
β’ (Β¬
π
β V β
(RLRegβπ
) = {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )}) |
28 | 20, 27 | pm2.61i 182 |
. 2
β’
(RLRegβπ
) =
{π₯ β π΅ β£ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )} |
29 | 1, 28 | eqtri 2761 |
1
β’ πΈ = {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )} |