Step | Hyp | Ref
| Expression |
1 | | lincop 47177 |
. . . 4
β’ (π β π β ( linC βπ) = (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))))) |
2 | 1 | 3ad2ant1 1133 |
. . 3
β’ ((π β π β§ π β ((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β ( linC βπ) = (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))))) |
3 | 2 | oveqd 7428 |
. 2
β’ ((π β π β§ π β ((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (π( linC βπ)π) = (π(π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))))π)) |
4 | | simp2 1137 |
. . 3
β’ ((π β π β§ π β ((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β π β ((Baseβ(Scalarβπ)) βm π)) |
5 | | simp3 1138 |
. . 3
β’ ((π β π β§ π β ((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β π β π« (Baseβπ)) |
6 | | ovexd 7446 |
. . 3
β’ ((π β π β§ π β ((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (π Ξ£g (π₯ β π β¦ ((πβπ₯)( Β·π
βπ)π₯))) β V) |
7 | | simpr 485 |
. . . . . 6
β’ ((π = π β§ π£ = π) β π£ = π) |
8 | | fveq1 6890 |
. . . . . . . 8
β’ (π = π β (π βπ₯) = (πβπ₯)) |
9 | 8 | oveq1d 7426 |
. . . . . . 7
β’ (π = π β ((π βπ₯)( Β·π
βπ)π₯) = ((πβπ₯)( Β·π
βπ)π₯)) |
10 | 9 | adantr 481 |
. . . . . 6
β’ ((π = π β§ π£ = π) β ((π βπ₯)( Β·π
βπ)π₯) = ((πβπ₯)( Β·π
βπ)π₯)) |
11 | 7, 10 | mpteq12dv 5239 |
. . . . 5
β’ ((π = π β§ π£ = π) β (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯)) = (π₯ β π β¦ ((πβπ₯)( Β·π
βπ)π₯))) |
12 | 11 | oveq2d 7427 |
. . . 4
β’ ((π = π β§ π£ = π) β (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))) = (π Ξ£g (π₯ β π β¦ ((πβπ₯)( Β·π
βπ)π₯)))) |
13 | | oveq2 7419 |
. . . 4
β’ (π£ = π β ((Baseβ(Scalarβπ)) βm π£) =
((Baseβ(Scalarβπ)) βm π)) |
14 | | eqid 2732 |
. . . 4
β’ (π β
((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯)))) = (π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯)))) |
15 | 12, 13, 14 | ovmpox2 47105 |
. . 3
β’ ((π β
((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ) β§ (π Ξ£g (π₯ β π β¦ ((πβπ₯)( Β·π
βπ)π₯))) β V) β (π(π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))))π) = (π Ξ£g (π₯ β π β¦ ((πβπ₯)( Β·π
βπ)π₯)))) |
16 | 4, 5, 6, 15 | syl3anc 1371 |
. 2
β’ ((π β π β§ π β ((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (π(π β ((Baseβ(Scalarβπ)) βm π£), π£ β π« (Baseβπ) β¦ (π Ξ£g (π₯ β π£ β¦ ((π βπ₯)( Β·π
βπ)π₯))))π) = (π Ξ£g (π₯ β π β¦ ((πβπ₯)( Β·π
βπ)π₯)))) |
17 | 3, 16 | eqtrd 2772 |
1
β’ ((π β π β§ π β ((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (π( linC βπ)π) = (π Ξ£g (π₯ β π β¦ ((πβπ₯)( Β·π
βπ)π₯)))) |