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	$⊢ \underset{˙}{+} = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
		dvhopvadd2.u	$⊢ U = DVecH (K) (W)$
		dvhopvadd2.s	$⊢ \underset{˙}{✚} = +_{U}$
	Assertion	dvhopvadd2	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to ⟨F, Q⟩ \underset{˙}{✚} ⟨G, R⟩ = ⟨F \circ G, Q \underset{˙}{+} 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	$⊢ \underset{˙}{+} = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
5		dvhopvadd2.u	$⊢ U = DVecH (K) (W)$
6		dvhopvadd2.s	$⊢ \underset{˙}{✚} = +_{U}$
7		eqid	$⊢ Scalar (U) = Scalar (U)$
8		eqid	$⊢ +_{Scalar (U)} = +_{Scalar (U)}$
9	1 2 3 5 7 6 8	dvhopvadd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to ⟨F, Q⟩ \underset{˙}{✚} ⟨G, R⟩ = ⟨F \circ G, Q +_{Scalar (U)} R⟩$
10	1 2 3 5 7 4 8	dvhfplusr	$⊢ (K \in HL \land W \in H) \to +_{Scalar (U)} = \underset{˙}{+}$
11	10	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to +_{Scalar (U)} = \underset{˙}{+}$
12	11	oveqd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to Q +_{Scalar (U)} R = Q \underset{˙}{+} R$
13	12	opeq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to ⟨F \circ G, Q +_{Scalar (U)} R⟩ = ⟨F \circ G, Q \underset{˙}{+} R⟩$
14	9 13	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to ⟨F, Q⟩ \underset{˙}{✚} ⟨G, R⟩ = ⟨F \circ G, Q \underset{˙}{+} R⟩$