Theorem dvhopvadd2

Description: The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd and/or dvhfplusr . (Contributed by NM, 26-Sep-2014)

	Ref	Expression
Hypotheses	dvhopvadd2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvhopvadd2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dvhopvadd2.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dvhopvadd2.p	⊢ + = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
	dvhopvadd2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dvhopvadd2.s	⊢ ✚ = ( +g ‘ 𝑈 )
Assertion	dvhopvadd2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( ⟨ 𝐹 , 𝑄 ⟩ ✚ ⟨ 𝐺 , 𝑅 ⟩ ) = ⟨ ( 𝐹 ∘ 𝐺 ) , ( 𝑄 + 𝑅 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		dvhopvadd2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dvhopvadd2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3		dvhopvadd2.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4		dvhopvadd2.p	⊢ + = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
5		dvhopvadd2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6		dvhopvadd2.s	⊢ ✚ = ( +g ‘ 𝑈 )
7		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
8		eqid	⊢ ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( +g ‘ ( Scalar ‘ 𝑈 ) )
9	1 2 3 5 7 6 8	dvhopvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( ⟨ 𝐹 , 𝑄 ⟩ ✚ ⟨ 𝐺 , 𝑅 ⟩ ) = ⟨ ( 𝐹 ∘ 𝐺 ) , ( 𝑄 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑅 ) ⟩ )
10	1 2 3 5 7 4 8	dvhfplusr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ ( Scalar ‘ 𝑈 ) ) = + )
11	10	3ad2ant1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( +g ‘ ( Scalar ‘ 𝑈 ) ) = + )
12	11	oveqd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( 𝑄 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑅 ) = ( 𝑄 + 𝑅 ) )
13	12	opeq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ⟨ ( 𝐹 ∘ 𝐺 ) , ( 𝑄 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑅 ) ⟩ = ⟨ ( 𝐹 ∘ 𝐺 ) , ( 𝑄 + 𝑅 ) ⟩ )
14	9 13	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( ⟨ 𝐹 , 𝑄 ⟩ ✚ ⟨ 𝐺 , 𝑅 ⟩ ) = ⟨ ( 𝐹 ∘ 𝐺 ) , ( 𝑄 + 𝑅 ) ⟩ )