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	$⊢ H = LHyp (K)$
		dvhvadd.t	$⊢ T = LTrn (K) (W)$
		dvhvadd.e	$⊢ E = TEndo (K) (W)$
		dvhvadd.u	$⊢ U = DVecH (K) (W)$
		dvhvadd.f	$⊢ D = Scalar (U)$
		dvhvadd.s	$⊢ \underset{˙}{+} = +_{U}$
		dvhvadd.p	$⊢ \underset{˙}{⨣} = +_{D}$
	Assertion	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to F \underset{˙}{+} G = ⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩$

Proof

Step	Hyp	Ref	Expression
1		dvhvadd.h	$⊢ H = LHyp (K)$
2		dvhvadd.t	$⊢ T = LTrn (K) (W)$
3		dvhvadd.e	$⊢ E = TEndo (K) (W)$
4		dvhvadd.u	$⊢ U = DVecH (K) (W)$
5		dvhvadd.f	$⊢ D = Scalar (U)$
6		dvhvadd.s	$⊢ \underset{˙}{+} = +_{U}$
7		dvhvadd.p	$⊢ \underset{˙}{⨣} = +_{D}$
8		eqid	$⊢ (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩) = (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩)$
9	1 2 3 4 5 7 8 6	dvhfvadd	$⊢ (K \in HL \land W \in H) \to \underset{˙}{+} = (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩)$
10	9	oveqd	$⊢ (K \in HL \land W \in H) \to F \underset{˙}{+} G = F (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩) G$
11	8	dvhvaddval	$⊢ (F \in (T \times E) \land G \in (T \times E)) \to F (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩) G = ⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩$
12	10 11	sylan9eq	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to F \underset{˙}{+} G = ⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩$