Metamath Proof Explorer

Theorem dvhvadd

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 11-Feb-2014) (Revised by Mario Carneiro, 23-Jun-2014)

		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	dvhvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⟩ )

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		eqid	⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ∘ ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ 𝑓 ) ⨣ ( 2^nd ‘ 𝑔 ) ) ⟩ ) = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ∘ ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ 𝑓 ) ⨣ ( 2^nd ‘ 𝑔 ) ) ⟩ )
9	1 2 3 4 5 7 8 6	dvhfvadd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → + = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ∘ ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ 𝑓 ) ⨣ ( 2^nd ‘ 𝑔 ) ) ⟩ ) )
10	9	oveqd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 + 𝐺 ) = ( 𝐹 ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ∘ ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ 𝑓 ) ⨣ ( 2^nd ‘ 𝑔 ) ) ⟩ ) 𝐺 ) )
11	8	dvhvaddval	⊢ ( ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝐹 ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ∘ ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ 𝑓 ) ⨣ ( 2^nd ‘ 𝑔 ) ) ⟩ ) 𝐺 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⟩ )
12	10 11	sylan9eq	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⟩ )