Step | Hyp | Ref
| Expression |
1 | | dvhfvsca.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | dvhfvsca.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
3 | | dvhfvsca.e |
. . . 4
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | | eqid 2737 |
. . . 4
β’
((EDRingβπΎ)βπ) = ((EDRingβπΎ)βπ) |
5 | | dvhfvsca.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
6 | 1, 2, 3, 4, 5 | dvhset 39547 |
. . 3
β’ ((πΎ β π β§ π β π») β π = ({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) |
7 | 6 | fveq2d 6847 |
. 2
β’ ((πΎ β π β§ π β π») β (
Β·π βπ) = ( Β·π
β({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))) |
8 | | dvhfvsca.s |
. 2
β’ Β· = (
Β·π βπ) |
9 | 3 | fvexi 6857 |
. . . 4
β’ πΈ β V |
10 | 2 | fvexi 6857 |
. . . . 5
β’ π β V |
11 | 10, 9 | xpex 7688 |
. . . 4
β’ (π Γ πΈ) β V |
12 | 9, 11 | mpoex 8013 |
. . 3
β’ (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β
V |
13 | | eqid 2737 |
. . . 4
β’
({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}) =
({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}) |
14 | 13 | lmodvsca 17211 |
. . 3
β’ ((π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β V β (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) = (
Β·π β({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))) |
15 | 12, 14 | ax-mp 5 |
. 2
β’ (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) = (
Β·π β({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) |
16 | 7, 8, 15 | 3eqtr4g 2802 |
1
β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)) |