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 ⊢ H = LHyp ⁡ K
dvhopvadd2.t ⊢ T = LTrn ⁡ K ⁡ W
dvhopvadd2.e ⊢ E = TEndo ⁡ K ⁡ W
dvhopvadd2.p ⊢ + ˙ = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
dvhopvadd2.u ⊢ U = DVecH ⁡ K ⁡ W
dvhopvadd2.s ⊢ ✚ ˙ = + U
Assertion dvhopvadd2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ Q ∈ E ∧ G ∈ T ∧ R ∈ E → F Q ✚ ˙ G R = F ∘ G Q + ˙ R

Proof

Step Hyp Ref Expression
1 dvhopvadd2.h ⊢ H = LHyp ⁡ K
2 dvhopvadd2.t ⊢ T = LTrn ⁡ K ⁡ W
3 dvhopvadd2.e ⊢ E = TEndo ⁡ K ⁡ W
4 dvhopvadd2.p ⊢ + ˙ = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
5 dvhopvadd2.u ⊢ U = DVecH ⁡ K ⁡ W
6 dvhopvadd2.s ⊢ ✚ ˙ = + U
7 eqid ⊢ Scalar ⁡ U = Scalar ⁡ U
8 eqid ⊢ + Scalar ⁡ U = + Scalar ⁡ U
9 1 2 3 5 7 6 8 dvhopvadd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ Q ∈ E ∧ G ∈ T ∧ R ∈ E → F Q ✚ ˙ G R = F ∘ G Q + Scalar ⁡ U R
10 1 2 3 5 7 4 8 dvhfplusr ⊢ K ∈ HL ∧ W ∈ H → + Scalar ⁡ U = + ˙
11 10 3ad2ant1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ Q ∈ E ∧ G ∈ T ∧ R ∈ E → + Scalar ⁡ U = + ˙
12 11 oveqd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ Q ∈ E ∧ G ∈ T ∧ R ∈ E → Q + Scalar ⁡ U R = Q + ˙ R
13 12 opeq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ Q ∈ E ∧ G ∈ T ∧ R ∈ E → F ∘ G Q + Scalar ⁡ U R = F ∘ G Q + ˙ R
14 9 13 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ Q ∈ E ∧ G ∈ T ∧ R ∈ E → F Q ✚ ˙ G R = F ∘ G Q + ˙ R