Step | Hyp | Ref
| Expression |
1 | | df-linc 46388 |
. 2
β’ linC =
(π β V β¦ (π β
((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))))) |
2 | | 2fveq3 6844 |
. . . 4
β’ (π = π β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
3 | 2 | oveq1d 7366 |
. . 3
β’ (π = π β ((Baseβ(Scalarβπ)) βm π£) =
((Baseβ(Scalarβπ)) βm π£)) |
4 | | fveq2 6839 |
. . . 4
β’ (π = π β (Baseβπ) = (Baseβπ)) |
5 | 4 | pweqd 4575 |
. . 3
β’ (π = π β π« (Baseβπ) = π« (Baseβπ)) |
6 | | id 22 |
. . . 4
β’ (π = π β π = π) |
7 | | fveq2 6839 |
. . . . . 6
β’ (π = π β (
Β·π βπ) = ( Β·π
βπ)) |
8 | 7 | oveqd 7368 |
. . . . 5
β’ (π = π β ((π βπ₯)( Β·π
βπ)π₯) = ((π βπ₯)( Β·π
βπ)π₯)) |
9 | 8 | mpteq2dv 5205 |
. . . 4
β’ (π = π β (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯)) = (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))) |
10 | 6, 9 | oveq12d 7369 |
. . 3
β’ (π = π β (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))) = (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯)))) |
11 | 3, 5, 10 | mpoeq123dv 7426 |
. 2
β’ (π = π β (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯)))) = (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))))) |
12 | | elex 3461 |
. 2
β’ (π β π β π β V) |
13 | | fvex 6852 |
. . . 4
β’
(Baseβπ)
β V |
14 | 13 | pwex 5333 |
. . 3
β’ π«
(Baseβπ) β
V |
15 | | ovexd 7386 |
. . . 4
β’ (π β π β ((Baseβ(Scalarβπ)) βm π£) β V) |
16 | 15 | ralrimivw 3145 |
. . 3
β’ (π β π β βπ£ β π« (Baseβπ)((Baseβ(Scalarβπ)) βm π£) β V) |
17 | | eqid 2737 |
. . . 4
β’ (π β
((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯)))) = (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯)))) |
18 | 17 | mpoexxg2 46314 |
. . 3
β’
((π« (Baseβπ) β V β§ βπ£ β π« (Baseβπ)((Baseβ(Scalarβπ)) βm π£) β V) β (π β
((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯)))) β V) |
19 | 14, 16, 18 | sylancr 587 |
. 2
β’ (π β π β (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯)))) β V) |
20 | 1, 11, 12, 19 | fvmptd3 6968 |
1
β’ (π β π β ( linC βπ) = (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))))) |