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

Metamath Proof Explorer

Theorem dvavadd

Description: Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013)

Ref Expression
Hypotheses dvafvadd.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvafvadd.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvafvadd.u ⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
dvafvadd.v ⊢ + = ( +g ‘ 𝑈 )
Assertion dvavadd ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝐹 + 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 dvafvadd.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvafvadd.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dvafvadd.u ⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
4 dvafvadd.v ⊢ + = ( +g ‘ 𝑈 )
5 1 2 3 4 dvafvadd ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → + = ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) )
6 5 oveqd ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 + 𝐺 ) = ( 𝐹 ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) 𝐺 ) )
7 coexg ⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ V )
8 coeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∘ 𝑔 ) = ( 𝐹 ∘ 𝑔 ) )
9 coeq2 ⊢ ( 𝑔 = 𝐺 → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ 𝐺 ) )
10 eqid ⊢ ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) )
11 8 9 10 ovmpog ⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝐹 ∘ 𝐺 ) ∈ V ) → ( 𝐹 ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )
12 7 11 mpd3an3 ⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )
13 6 12 sylan9eq ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝐹 + 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )