Step | Hyp | Ref
| Expression |
1 | | dvhfvadd.h |
. . . . 5
β’ π» = (LHypβπΎ) |
2 | | dvhfvadd.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
3 | | dvhfvadd.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | | eqid 2737 |
. . . . 5
β’
((EDRingβπΎ)βπ) = ((EDRingβπΎ)βπ) |
5 | | dvhfvadd.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
6 | 1, 2, 3, 4, 5 | dvhset 39547 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π = ({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) |
7 | 6 | fveq2d 6847 |
. . 3
β’ ((πΎ β HL β§ π β π») β (+gβπ) =
(+gβ({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))) |
8 | | dvhfvadd.p |
. . . . . . . . . 10
⒠⨣ =
(+gβπ·) |
9 | | dvhfvadd.f |
. . . . . . . . . . . 12
β’ π· = (Scalarβπ) |
10 | 1, 4, 5, 9 | dvhsca 39548 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β π») β π· = ((EDRingβπΎ)βπ)) |
11 | 10 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π») β (+gβπ·) =
(+gβ((EDRingβπΎ)βπ))) |
12 | 8, 11 | eqtrid 2789 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β ⨣ =
(+gβ((EDRingβπΎ)βπ))) |
13 | 12 | oveqd 7375 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β ((2nd βπ) ⨣ (2nd
βπ)) =
((2nd βπ)(+gβ((EDRingβπΎ)βπ))(2nd βπ))) |
14 | 13 | 3ad2ant1 1134 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ) β§ π β (π Γ πΈ)) β ((2nd βπ) ⨣ (2nd
βπ)) =
((2nd βπ)(+gβ((EDRingβπΎ)βπ))(2nd βπ))) |
15 | | xp2nd 7955 |
. . . . . . . . . 10
β’ (π β (π Γ πΈ) β (2nd βπ) β πΈ) |
16 | | xp2nd 7955 |
. . . . . . . . . 10
β’ (π β (π Γ πΈ) β (2nd βπ) β πΈ) |
17 | 15, 16 | anim12i 614 |
. . . . . . . . 9
β’ ((π β (π Γ πΈ) β§ π β (π Γ πΈ)) β ((2nd βπ) β πΈ β§ (2nd βπ) β πΈ)) |
18 | | eqid 2737 |
. . . . . . . . . 10
β’
(+gβ((EDRingβπΎ)βπ)) =
(+gβ((EDRingβπΎ)βπ)) |
19 | 1, 2, 3, 4, 18 | erngplus 39269 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ ((2nd βπ) β πΈ β§ (2nd βπ) β πΈ)) β ((2nd βπ)(+gβ((EDRingβπΎ)βπ))(2nd βπ)) = (β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))) |
20 | 17, 19 | sylan2 594 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β (π Γ πΈ) β§ π β (π Γ πΈ))) β ((2nd βπ)(+gβ((EDRingβπΎ)βπ))(2nd βπ)) = (β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))) |
21 | 20 | 3impb 1116 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ) β§ π β (π Γ πΈ)) β ((2nd βπ)(+gβ((EDRingβπΎ)βπ))(2nd βπ)) = (β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))) |
22 | 14, 21 | eqtrd 2777 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ) β§ π β (π Γ πΈ)) β ((2nd βπ) ⨣ (2nd
βπ)) = (β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))) |
23 | 22 | opeq2d 4838 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ) β§ π β (π Γ πΈ)) β β¨((1st
βπ) β
(1st βπ)),
((2nd βπ)
⨣
(2nd βπ))β© = β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©) |
24 | 23 | mpoeq3dva 7435 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
((2nd βπ)
⨣
(2nd βπ))β©) = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)) |
25 | 2 | fvexi 6857 |
. . . . . . 7
β’ π β V |
26 | 3 | fvexi 6857 |
. . . . . . 7
β’ πΈ β V |
27 | 25, 26 | xpex 7688 |
. . . . . 6
β’ (π Γ πΈ) β V |
28 | 27, 27 | mpoex 8013 |
. . . . 5
β’ (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©) β V |
29 | | eqid 2737 |
. . . . . 6
β’
({β¨(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 βπ))β©)β©}) |
30 | 29 | lmodplusg 17209 |
. . . . 5
β’ ((π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©) β V β (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©) =
(+gβ({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))) |
31 | 28, 30 | ax-mp 5 |
. . . 4
β’ (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©) =
(+gβ({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) |
32 | 24, 31 | eqtr2di 2794 |
. . 3
β’ ((πΎ β HL β§ π β π») β
(+gβ({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
((2nd βπ)
⨣
(2nd βπ))β©)) |
33 | 7, 32 | eqtrd 2777 |
. 2
β’ ((πΎ β HL β§ π β π») β (+gβπ) = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
((2nd βπ)
⨣
(2nd βπ))β©)) |
34 | | dvhfvadd.s |
. 2
β’ + =
(+gβπ) |
35 | | dvhfvadd.a |
. 2
β’ β =
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
((2nd βπ)
⨣
(2nd βπ))β©) |
36 | 33, 34, 35 | 3eqtr4g 2802 |
1
β’ ((πΎ β HL β§ π β π») β + = β ) |