Metamath Proof Explorer


Theorem dvhopvadd

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 21-Feb-2014) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses dvhvadd.h 𝐻 = ( LHyp ‘ 𝐾 )
dvhvadd.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvhvadd.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dvhvadd.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvhvadd.f 𝐷 = ( Scalar ‘ 𝑈 )
dvhvadd.s + = ( +g𝑈 )
dvhvadd.p = ( +g𝐷 )
Assertion dvhopvadd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ( ⟨ 𝐹 , 𝑄+𝐺 , 𝑅 ⟩ ) = ⟨ ( 𝐹𝐺 ) , ( 𝑄 𝑅 ) ⟩ )

Proof

Step Hyp Ref Expression
1 dvhvadd.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dvhvadd.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dvhvadd.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 dvhvadd.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dvhvadd.f 𝐷 = ( Scalar ‘ 𝑈 )
6 dvhvadd.s + = ( +g𝑈 )
7 dvhvadd.p = ( +g𝐷 )
8 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
9 opelxpi ( ( 𝐹𝑇𝑄𝐸 ) → ⟨ 𝐹 , 𝑄 ⟩ ∈ ( 𝑇 × 𝐸 ) )
10 9 3ad2ant2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ⟨ 𝐹 , 𝑄 ⟩ ∈ ( 𝑇 × 𝐸 ) )
11 opelxpi ( ( 𝐺𝑇𝑅𝐸 ) → ⟨ 𝐺 , 𝑅 ⟩ ∈ ( 𝑇 × 𝐸 ) )
12 11 3ad2ant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ⟨ 𝐺 , 𝑅 ⟩ ∈ ( 𝑇 × 𝐸 ) )
13 1 2 3 4 5 6 7 dvhvadd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ⟨ 𝐹 , 𝑄 ⟩ ∈ ( 𝑇 × 𝐸 ) ∧ ⟨ 𝐺 , 𝑅 ⟩ ∈ ( 𝑇 × 𝐸 ) ) ) → ( ⟨ 𝐹 , 𝑄+𝐺 , 𝑅 ⟩ ) = ⟨ ( ( 1st ‘ ⟨ 𝐹 , 𝑄 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐺 , 𝑅 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐹 , 𝑄 ⟩ ) ( 2nd ‘ ⟨ 𝐺 , 𝑅 ⟩ ) ) ⟩ )
14 8 10 12 13 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ( ⟨ 𝐹 , 𝑄+𝐺 , 𝑅 ⟩ ) = ⟨ ( ( 1st ‘ ⟨ 𝐹 , 𝑄 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐺 , 𝑅 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐹 , 𝑄 ⟩ ) ( 2nd ‘ ⟨ 𝐺 , 𝑅 ⟩ ) ) ⟩ )
15 op1stg ( ( 𝐹𝑇𝑄𝐸 ) → ( 1st ‘ ⟨ 𝐹 , 𝑄 ⟩ ) = 𝐹 )
16 15 3ad2ant2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ( 1st ‘ ⟨ 𝐹 , 𝑄 ⟩ ) = 𝐹 )
17 op1stg ( ( 𝐺𝑇𝑅𝐸 ) → ( 1st ‘ ⟨ 𝐺 , 𝑅 ⟩ ) = 𝐺 )
18 17 3ad2ant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ( 1st ‘ ⟨ 𝐺 , 𝑅 ⟩ ) = 𝐺 )
19 16 18 coeq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ( ( 1st ‘ ⟨ 𝐹 , 𝑄 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐺 , 𝑅 ⟩ ) ) = ( 𝐹𝐺 ) )
20 op2ndg ( ( 𝐹𝑇𝑄𝐸 ) → ( 2nd ‘ ⟨ 𝐹 , 𝑄 ⟩ ) = 𝑄 )
21 20 3ad2ant2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ( 2nd ‘ ⟨ 𝐹 , 𝑄 ⟩ ) = 𝑄 )
22 op2ndg ( ( 𝐺𝑇𝑅𝐸 ) → ( 2nd ‘ ⟨ 𝐺 , 𝑅 ⟩ ) = 𝑅 )
23 22 3ad2ant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ( 2nd ‘ ⟨ 𝐺 , 𝑅 ⟩ ) = 𝑅 )
24 21 23 oveq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ( ( 2nd ‘ ⟨ 𝐹 , 𝑄 ⟩ ) ( 2nd ‘ ⟨ 𝐺 , 𝑅 ⟩ ) ) = ( 𝑄 𝑅 ) )
25 19 24 opeq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ⟨ ( ( 1st ‘ ⟨ 𝐹 , 𝑄 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐺 , 𝑅 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐹 , 𝑄 ⟩ ) ( 2nd ‘ ⟨ 𝐺 , 𝑅 ⟩ ) ) ⟩ = ⟨ ( 𝐹𝐺 ) , ( 𝑄 𝑅 ) ⟩ )
26 14 25 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑄𝐸 ) ∧ ( 𝐺𝑇𝑅𝐸 ) ) → ( ⟨ 𝐹 , 𝑄+𝐺 , 𝑅 ⟩ ) = ⟨ ( 𝐹𝐺 ) , ( 𝑄 𝑅 ) ⟩ )