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 𝐻 = ( LHyp ‘ 𝐾 )
dvhfvadd.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvhfvadd.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dvhfvadd.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvhfvadd.f 𝐷 = ( Scalar ‘ 𝑈 )
dvhfvadd.p = ( +g𝐷 )
dvhfvadd.a = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( ( 2nd𝑓 ) ( 2nd𝑔 ) ) ⟩ )
dvhfvadd.s + = ( +g𝑈 )
Assertion dvhfvadd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → + = )

Proof

Step Hyp Ref Expression
1 dvhfvadd.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dvhfvadd.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dvhfvadd.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 dvhfvadd.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dvhfvadd.f 𝐷 = ( Scalar ‘ 𝑈 )
6 dvhfvadd.p = ( +g𝐷 )
7 dvhfvadd.a = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( ( 2nd𝑓 ) ( 2nd𝑔 ) ) ⟩ )
8 dvhfvadd.s + = ( +g𝑈 )
9 eqid ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
10 1 2 3 9 4 dvhset ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑈 = ( { ⟨ ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1st𝑓 ) ) , ( 𝑠 ∘ ( 2nd𝑓 ) ) ⟩ ) ⟩ } ) )
11 10 fveq2d ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( +g𝑈 ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1st𝑓 ) ) , ( 𝑠 ∘ ( 2nd𝑓 ) ) ⟩ ) ⟩ } ) ) )
12 1 9 4 5 dvhsca ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
13 12 fveq2d ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( +g𝐷 ) = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
14 6 13 syl5eq ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
15 14 oveqd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( 2nd𝑓 ) ( 2nd𝑔 ) ) = ( ( 2nd𝑓 ) ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ( 2nd𝑔 ) ) )
16 15 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 2nd𝑓 ) ( 2nd𝑔 ) ) = ( ( 2nd𝑓 ) ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ( 2nd𝑔 ) ) )
17 xp2nd ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → ( 2nd𝑓 ) ∈ 𝐸 )
18 xp2nd ( 𝑔 ∈ ( 𝑇 × 𝐸 ) → ( 2nd𝑔 ) ∈ 𝐸 )
19 17 18 anim12i ( ( 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 2nd𝑓 ) ∈ 𝐸 ∧ ( 2nd𝑔 ) ∈ 𝐸 ) )
20 eqid ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
21 1 2 3 9 20 erngplus ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 2nd𝑓 ) ∈ 𝐸 ∧ ( 2nd𝑔 ) ∈ 𝐸 ) ) → ( ( 2nd𝑓 ) ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ( 2nd𝑔 ) ) = ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) )
22 19 21 sylan2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd𝑓 ) ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ( 2nd𝑔 ) ) = ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) )
23 22 3impb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 2nd𝑓 ) ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ( 2nd𝑔 ) ) = ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) )
24 16 23 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 2nd𝑓 ) ( 2nd𝑔 ) ) = ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) )
25 24 opeq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( ( 2nd𝑓 ) ( 2nd𝑔 ) ) ⟩ = ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ )
26 25 mpoeq3dva ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( ( 2nd𝑓 ) ( 2nd𝑔 ) ) ⟩ ) = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ ) )
27 2 fvexi 𝑇 ∈ V
28 3 fvexi 𝐸 ∈ V
29 27 28 xpex ( 𝑇 × 𝐸 ) ∈ V
30 29 29 mpoex ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ ) ∈ V
31 eqid ( { ⟨ ( 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𝑓 ) ) ⟩ ) ⟩ } )
32 31 lmodplusg ( ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ ) ∈ V → ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1st𝑓 ) ) , ( 𝑠 ∘ ( 2nd𝑓 ) ) ⟩ ) ⟩ } ) ) )
33 30 32 ax-mp ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1st𝑓 ) ) , ( 𝑠 ∘ ( 2nd𝑓 ) ) ⟩ ) ⟩ } ) )
34 26 33 eqtr2di ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( 𝑇 ↦ ( ( ( 2nd𝑓 ) ‘ ) ∘ ( ( 2nd𝑔 ) ‘ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1st𝑓 ) ) , ( 𝑠 ∘ ( 2nd𝑓 ) ) ⟩ ) ⟩ } ) ) = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( ( 2nd𝑓 ) ( 2nd𝑔 ) ) ⟩ ) )
35 11 34 eqtrd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( +g𝑈 ) = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st𝑓 ) ∘ ( 1st𝑔 ) ) , ( ( 2nd𝑓 ) ( 2nd𝑔 ) ) ⟩ ) )
36 35 8 7 3eqtr4g ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → + = )