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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( ⟨ 𝐹 , 𝑄 ⟩ + ⟨ 𝐺 , 𝑅 ⟩ ) = ⟨ ( 𝐹 ∘ 𝐺 ) , ( 𝑄 ⨣ 𝑅 ) ⟩ )