Step | Hyp | Ref
| Expression |
1 | | dvhsca.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | eqid 2737 |
. . . 4
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
3 | | eqid 2737 |
. . . 4
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
4 | | dvhsca.d |
. . . 4
β’ π· = ((EDRingβπΎ)βπ) |
5 | | dvhsca.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
6 | 1, 2, 3, 4, 5 | dvhset 39547 |
. . 3
β’ ((πΎ β π β§ π β π») β π = ({β¨(Baseβndx),
(((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) |
7 | 6 | fveq2d 6847 |
. 2
β’ ((πΎ β π β§ π β π») β (Scalarβπ) = (Scalarβ({β¨(Baseβndx),
(((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))) |
8 | | dvhsca.f |
. 2
β’ πΉ = (Scalarβπ) |
9 | 4 | fvexi 6857 |
. . 3
β’ π· β V |
10 | | eqid 2737 |
. . . 4
β’
({β¨(Baseβndx), (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}) =
({β¨(Baseβndx), (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}) |
11 | 10 | lmodsca 17210 |
. . 3
β’ (π· β V β π· =
(Scalarβ({β¨(Baseβndx), (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))) |
12 | 9, 11 | ax-mp 5 |
. 2
β’ π· =
(Scalarβ({β¨(Baseβndx), (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ), π β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) |
13 | 7, 8, 12 | 3eqtr4g 2802 |
1
β’ ((πΎ β π β§ π β π») β πΉ = π·) |