This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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