Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvhfvadd Structured version   Unicode version

 Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.)
Hypotheses
Ref Expression
Assertion
Ref Expression
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)   (,)

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvhfvadd.h . . . . 5
2 dvhfvadd.t . . . . 5
3 dvhfvadd.e . . . . 5
4 eqid 2436 . . . . 5
5 dvhfvadd.u . . . . 5
61, 2, 3, 4, 5dvhset 31879 . . . 4 Scalar
76fveq2d 5732 . . 3 Scalar
8 dvhfvadd.p . . . . . . . . . 10
9 dvhfvadd.f . . . . . . . . . . . 12 Scalar
101, 4, 5, 9dvhsca 31880 . . . . . . . . . . 11
1110fveq2d 5732 . . . . . . . . . 10
128, 11syl5eq 2480 . . . . . . . . 9
1312oveqd 6098 . . . . . . . 8
14133ad2ant1 978 . . . . . . 7
15 xp2nd 6377 . . . . . . . . . 10
16 xp2nd 6377 . . . . . . . . . 10
1715, 16anim12i 550 . . . . . . . . 9
18 eqid 2436 . . . . . . . . . 10
191, 2, 3, 4, 18erngplus 31600 . . . . . . . . 9
2017, 19sylan2 461 . . . . . . . 8
21203impb 1149 . . . . . . 7
2214, 21eqtrd 2468 . . . . . 6
2322opeq2d 3991 . . . . 5
2423mpt2eq3dva 6138 . . . 4
25 fvex 5742 . . . . . . . 8
262, 25eqeltri 2506 . . . . . . 7
27 fvex 5742 . . . . . . . 8
283, 27eqeltri 2506 . . . . . . 7
2926, 28xpex 4990 . . . . . 6
3029, 29mpt2ex 6425 . . . . 5
31 eqid 2436 . . . . . 6 Scalar Scalar
3231lmodplusg 13595 . . . . 5 Scalar
3330, 32ax-mp 8 . . . 4 Scalar
3424, 33syl6req 2485 . . 3 Scalar
357, 34eqtrd 2468 . 2