Step | Hyp | Ref
| Expression |
1 | | rrxlines.e |
. . . 4
β’ πΈ = (β^βπΌ) |
2 | 1 | fvexi 6853 |
. . 3
β’ πΈ β V |
3 | | eqid 2737 |
. . . 4
β’
(BaseβπΈ) =
(BaseβπΈ) |
4 | | rrxlines.l |
. . . 4
β’ πΏ = (LineMβπΈ) |
5 | | eqid 2737 |
. . . 4
β’
(ScalarβπΈ) =
(ScalarβπΈ) |
6 | | eqid 2737 |
. . . 4
β’
(Baseβ(ScalarβπΈ)) = (Baseβ(ScalarβπΈ)) |
7 | | rrxlines.m |
. . . 4
β’ Β· = (
Β·π βπΈ) |
8 | | rrxlines.a |
. . . 4
β’ + =
(+gβπΈ) |
9 | | eqid 2737 |
. . . 4
β’
(-gβ(ScalarβπΈ)) =
(-gβ(ScalarβπΈ)) |
10 | | eqid 2737 |
. . . 4
β’
(1rβ(ScalarβπΈ)) =
(1rβ(ScalarβπΈ)) |
11 | 3, 4, 5, 6, 7, 8, 9, 10 | lines 46718 |
. . 3
β’ (πΈ β V β πΏ = (π₯ β (BaseβπΈ), π¦ β ((BaseβπΈ) β {π₯}) β¦ {π β (BaseβπΈ) β£ βπ‘ β (Baseβ(ScalarβπΈ))π =
((((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) Β· π₯) + (π‘ Β· π¦))})) |
12 | 2, 11 | mp1i 13 |
. 2
β’ (πΌ β Fin β πΏ = (π₯ β (BaseβπΈ), π¦ β ((BaseβπΈ) β {π₯}) β¦ {π β (BaseβπΈ) β£ βπ‘ β (Baseβ(ScalarβπΈ))π =
((((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) Β· π₯) + (π‘ Β· π¦))})) |
13 | | id 22 |
. . . . 5
β’ (πΌ β Fin β πΌ β Fin) |
14 | 13, 1, 3 | rrxbasefi 24726 |
. . . 4
β’ (πΌ β Fin β
(BaseβπΈ) = (β
βm πΌ)) |
15 | | rrxlines.p |
. . . 4
β’ π = (β βm
πΌ) |
16 | 14, 15 | eqtr4di 2795 |
. . 3
β’ (πΌ β Fin β
(BaseβπΈ) = π) |
17 | 16 | difeq1d 4079 |
. . 3
β’ (πΌ β Fin β
((BaseβπΈ) β
{π₯}) = (π β {π₯})) |
18 | 1 | rrxsca 24712 |
. . . . . . 7
β’ (πΌ β Fin β
(ScalarβπΈ) =
βfld) |
19 | 18 | fveq2d 6843 |
. . . . . 6
β’ (πΌ β Fin β
(Baseβ(ScalarβπΈ)) =
(Baseββfld)) |
20 | | rebase 20963 |
. . . . . 6
β’ β =
(Baseββfld) |
21 | 19, 20 | eqtr4di 2795 |
. . . . 5
β’ (πΌ β Fin β
(Baseβ(ScalarβπΈ)) = β) |
22 | 18 | fveq2d 6843 |
. . . . . . . . . . . 12
β’ (πΌ β Fin β
(1rβ(ScalarβπΈ)) =
(1rββfld)) |
23 | | re1r 20970 |
. . . . . . . . . . . 12
β’ 1 =
(1rββfld) |
24 | 22, 23 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ (πΌ β Fin β
(1rβ(ScalarβπΈ)) = 1) |
25 | 24 | oveq1d 7366 |
. . . . . . . . . 10
β’ (πΌ β Fin β
((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) =
(1(-gβ(ScalarβπΈ))π‘)) |
26 | 25 | adantr 481 |
. . . . . . . . 9
β’ ((πΌ β Fin β§ π‘ β
(Baseβ(ScalarβπΈ))) β
((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) =
(1(-gβ(ScalarβπΈ))π‘)) |
27 | 18 | fveq2d 6843 |
. . . . . . . . . . 11
β’ (πΌ β Fin β
(-gβ(ScalarβπΈ)) =
(-gββfld)) |
28 | 27 | oveqd 7368 |
. . . . . . . . . 10
β’ (πΌ β Fin β
(1(-gβ(ScalarβπΈ))π‘) =
(1(-gββfld)π‘)) |
29 | 28 | adantr 481 |
. . . . . . . . 9
β’ ((πΌ β Fin β§ π‘ β
(Baseβ(ScalarβπΈ))) β
(1(-gβ(ScalarβπΈ))π‘) =
(1(-gββfld)π‘)) |
30 | 21 | eleq2d 2823 |
. . . . . . . . . . 11
β’ (πΌ β Fin β (π‘ β
(Baseβ(ScalarβπΈ)) β π‘ β β)) |
31 | | 1re 11113 |
. . . . . . . . . . . 12
β’ 1 β
β |
32 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(-gββfld) =
(-gββfld) |
33 | 32 | resubgval 20966 |
. . . . . . . . . . . . 13
β’ ((1
β β β§ π‘
β β) β (1 β π‘) =
(1(-gββfld)π‘)) |
34 | 33 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ ((1
β β β§ π‘
β β) β (1(-gββfld)π‘) = (1 β π‘)) |
35 | 31, 34 | mpan 688 |
. . . . . . . . . . 11
β’ (π‘ β β β
(1(-gββfld)π‘) = (1 β π‘)) |
36 | 30, 35 | syl6bi 252 |
. . . . . . . . . 10
β’ (πΌ β Fin β (π‘ β
(Baseβ(ScalarβπΈ)) β
(1(-gββfld)π‘) = (1 β π‘))) |
37 | 36 | imp 407 |
. . . . . . . . 9
β’ ((πΌ β Fin β§ π‘ β
(Baseβ(ScalarβπΈ))) β
(1(-gββfld)π‘) = (1 β π‘)) |
38 | 26, 29, 37 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((πΌ β Fin β§ π‘ β
(Baseβ(ScalarβπΈ))) β
((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) = (1 β π‘)) |
39 | 38 | oveq1d 7366 |
. . . . . . 7
β’ ((πΌ β Fin β§ π‘ β
(Baseβ(ScalarβπΈ))) β
(((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) Β· π₯) = ((1 β π‘) Β· π₯)) |
40 | 39 | oveq1d 7366 |
. . . . . 6
β’ ((πΌ β Fin β§ π‘ β
(Baseβ(ScalarβπΈ))) β
((((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) Β· π₯) + (π‘ Β· π¦)) = (((1 β π‘) Β· π₯) + (π‘ Β· π¦))) |
41 | 40 | eqeq2d 2748 |
. . . . 5
β’ ((πΌ β Fin β§ π‘ β
(Baseβ(ScalarβπΈ))) β (π =
((((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) Β· π₯) + (π‘ Β· π¦)) β π = (((1 β π‘) Β· π₯) + (π‘ Β· π¦)))) |
42 | 21, 41 | rexeqbidva 3320 |
. . . 4
β’ (πΌ β Fin β (βπ‘ β
(Baseβ(ScalarβπΈ))π =
((((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) Β· π₯) + (π‘ Β· π¦)) β βπ‘ β β π = (((1 β π‘) Β· π₯) + (π‘ Β· π¦)))) |
43 | 16, 42 | rabeqbidv 3422 |
. . 3
β’ (πΌ β Fin β {π β (BaseβπΈ) β£ βπ‘ β
(Baseβ(ScalarβπΈ))π =
((((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) Β· π₯) + (π‘ Β· π¦))} = {π β π β£ βπ‘ β β π = (((1 β π‘) Β· π₯) + (π‘ Β· π¦))}) |
44 | 16, 17, 43 | mpoeq123dv 7426 |
. 2
β’ (πΌ β Fin β (π₯ β (BaseβπΈ), π¦ β ((BaseβπΈ) β {π₯}) β¦ {π β (BaseβπΈ) β£ βπ‘ β (Baseβ(ScalarβπΈ))π =
((((1rβ(ScalarβπΈ))(-gβ(ScalarβπΈ))π‘) Β· π₯) + (π‘ Β· π¦))}) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π β π β£ βπ‘ β β π = (((1 β π‘) Β· π₯) + (π‘ Β· π¦))})) |
45 | 12, 44 | eqtrd 2777 |
1
β’ (πΌ β Fin β πΏ = (π₯ β π, π¦ β (π β {π₯}) β¦ {π β π β£ βπ‘ β β π = (((1 β π‘) Β· π₯) + (π‘ Β· π¦))})) |