Metamath Proof Explorer

Theorem dvhfvadd

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)

Ref Expression
Hypotheses dvhfvadd.h ⊢H=LHyp⁡K
dvhfvadd.t ⊢T=LTrn⁡K⁡W
dvhfvadd.e ⊢E=TEndo⁡K⁡W
dvhfvadd.u ⊢U=DVecH⁡K⁡W
dvhfvadd.f ⊢D=Scalar⁡U
dvhfvadd.p ⊢⨣˙=+D
dvhfvadd.a ⊢✚˙=f∈T×E,g∈T×E⟼1st⁡f∘1st⁡g2nd⁡f⨣˙2nd⁡g
dvhfvadd.s ⊢+˙=+U
Assertion dvhfvadd ⊢K∈HL∧W∈H→+˙=✚˙

Proof

Step Hyp Ref Expression
1 dvhfvadd.h ⊢H=LHyp⁡K
2 dvhfvadd.t ⊢T=LTrn⁡K⁡W
3 dvhfvadd.e ⊢E=TEndo⁡K⁡W
4 dvhfvadd.u ⊢U=DVecH⁡K⁡W
5 dvhfvadd.f ⊢D=Scalar⁡U
6 dvhfvadd.p ⊢⨣˙=+D
7 dvhfvadd.a ⊢✚˙=f∈T×E,g∈T×E⟼1st⁡f∘1st⁡g2nd⁡f⨣˙2nd⁡g
8 dvhfvadd.s ⊢+˙=+U
9 eqid ⊢EDRing⁡K⁡W=EDRing⁡K⁡W
10 1 2 3 9 4 dvhset ⊢K∈HL∧W∈H→U=BasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f
11 10 fveq2d ⊢K∈HL∧W∈H→+U=+BasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f
12 1 9 4 5 dvhsca ⊢K∈HL∧W∈H→D=EDRing⁡K⁡W
13 12 fveq2d ⊢K∈HL∧W∈H→+D=+EDRing⁡K⁡W
14 6 13 eqtrid ⊢K∈HL∧W∈H→⨣˙=+EDRing⁡K⁡W
15 14 oveqd ⊢K∈HL∧W∈H→2nd⁡f⨣˙2nd⁡g=2nd⁡f+EDRing⁡K⁡W2nd⁡g
16 15 3ad2ant1 ⊢K∈HL∧W∈H∧f∈T×E∧g∈T×E→2nd⁡f⨣˙2nd⁡g=2nd⁡f+EDRing⁡K⁡W2nd⁡g
17 xp2nd ⊢f∈T×E→2nd⁡f∈E
18 xp2nd ⊢g∈T×E→2nd⁡g∈E
19 17 18 anim12i ⊢f∈T×E∧g∈T×E→2nd⁡f∈E∧2nd⁡g∈E
20 eqid ⊢+EDRing⁡K⁡W=+EDRing⁡K⁡W
21 1 2 3 9 20 erngplus ⊢K∈HL∧W∈H∧2nd⁡f∈E∧2nd⁡g∈E→2nd⁡f+EDRing⁡K⁡W2nd⁡g=h∈T⟼2nd⁡f⁡h∘2nd⁡g⁡h
22 19 21 sylan2 ⊢K∈HL∧W∈H∧f∈T×E∧g∈T×E→2nd⁡f+EDRing⁡K⁡W2nd⁡g=h∈T⟼2nd⁡f⁡h∘2nd⁡g⁡h
23 22 3impb ⊢K∈HL∧W∈H∧f∈T×E∧g∈T×E→2nd⁡f+EDRing⁡K⁡W2nd⁡g=h∈T⟼2nd⁡f⁡h∘2nd⁡g⁡h
24 16 23 eqtrd ⊢K∈HL∧W∈H∧f∈T×E∧g∈T×E→2nd⁡f⨣˙2nd⁡g=h∈T⟼2nd⁡f⁡h∘2nd⁡g⁡h
25 24 opeq2d ⊢K∈HL∧W∈H∧f∈T×E∧g∈T×E→1st⁡f∘1st⁡g2nd⁡f⨣˙2nd⁡g=1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡h
26 25 mpoeq3dva ⊢K∈HL∧W∈H→f∈T×E,g∈T×E⟼1st⁡f∘1st⁡g2nd⁡f⨣˙2nd⁡g=f∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡h
27 2 fvexi ⊢T∈V
28 3 fvexi ⊢E∈V
29 27 28 xpex ⊢T×E∈V
30 29 29 mpoex ⊢f∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡h∈V
31 eqid ⊢BasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f=BasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f
32 31 lmodplusg ⊢f∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡h∈V→f∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡h=+BasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f
33 30 32 ax-mp ⊢f∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡h=+BasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f
34 26 33 eqtr2di ⊢K∈HL∧W∈H→+BasendxT×E+ndxf∈T×E,g∈T×E⟼1st⁡f∘1st⁡gh∈T⟼2nd⁡f⁡h∘2nd⁡g⁡hScalar⁡ndxEDRing⁡K⁡W∪⋅ndxs∈E,f∈T×E⟼s⁡1st⁡fs∘2nd⁡f=f∈T×E,g∈T×E⟼1st⁡f∘1st⁡g2nd⁡f⨣˙2nd⁡g
35 11 34 eqtrd ⊢K∈HL∧W∈H→+U=f∈T×E,g∈T×E⟼1st⁡f∘1st⁡g2nd⁡f⨣˙2nd⁡g
36 35 8 7 3eqtr4g ⊢K∈HL∧W∈H→+˙=✚˙