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

Metamath Proof Explorer

Theorem dvhvaddval

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013)

		Ref	Expression
	Hypothesis	dvhvaddval.a	$⊢ \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)⟩)$
	Assertion	dvhvaddval	$⊢ (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		dvhvaddval.a	$⊢ \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)⟩)$
2		fveq2	$⊢ h = F \to 1^{st} (h) = 1^{st} (F)$
3	2	coeq1d	$⊢ h = F \to 1^{st} (h) \circ 1^{st} (i) = 1^{st} (F) \circ 1^{st} (i)$
4		fveq2	$⊢ h = F \to 2^{nd} (h) = 2^{nd} (F)$
5	4	oveq1d	$⊢ h = F \to 2^{nd} (h) \underset{˙}{⨣} 2^{nd} (i) = 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (i)$
6	3 5	opeq12d	$⊢ h = F \to ⟨1^{st} (h) \circ 1^{st} (i), 2^{nd} (h) \underset{˙}{⨣} 2^{nd} (i)⟩ = ⟨1^{st} (F) \circ 1^{st} (i), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (i)⟩$
7		fveq2	$⊢ i = G \to 1^{st} (i) = 1^{st} (G)$
8	7	coeq2d	$⊢ i = G \to 1^{st} (F) \circ 1^{st} (i) = 1^{st} (F) \circ 1^{st} (G)$
9		fveq2	$⊢ i = G \to 2^{nd} (i) = 2^{nd} (G)$
10	9	oveq2d	$⊢ i = G \to 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (i) = 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)$
11	8 10	opeq12d	$⊢ i = G \to ⟨1^{st} (F) \circ 1^{st} (i), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (i)⟩ = ⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩$
12	1	dvhvaddcbv	$⊢ \underset{˙}{+} = (h \in (T \times E), i \in (T \times E) ⟼ ⟨1^{st} (h) \circ 1^{st} (i), 2^{nd} (h) \underset{˙}{⨣} 2^{nd} (i)⟩)$
13		opex	$⊢ ⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩ \in V$
14	6 11 12 13	ovmpo	$⊢ (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)⟩$