dvavadd

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

	Ref	Expression
Hypotheses	dvafvadd.h	$⊢ H = LHyp (K)$
	dvafvadd.t	$⊢ T = LTrn (K) (W)$
	dvafvadd.u	$⊢ U = DVecA (K) (W)$
	dvafvadd.v	$⊢ \underset{˙}{+} = +_{U}$
Assertion	dvavadd	$⊢ ((K \in V \land W \in H) \land (F \in T \land G \in T)) \to F \underset{˙}{+} G = F \circ G$

Step	Hyp	Ref	Expression
1		dvafvadd.h	$⊢ H = LHyp (K)$
2		dvafvadd.t	$⊢ T = LTrn (K) (W)$
3		dvafvadd.u	$⊢ U = DVecA (K) (W)$
4		dvafvadd.v	$⊢ \underset{˙}{+} = +_{U}$
5	1 2 3 4	dvafvadd	$⊢ (K \in V \land W \in H) \to \underset{˙}{+} = (f \in T, g \in T ⟼ f \circ g)$
6	5	oveqd	$⊢ (K \in V \land W \in H) \to F \underset{˙}{+} G = F (f \in T, g \in T ⟼ f \circ g) G$
7		coexg	$⊢ (F \in T \land G \in T) \to F \circ G \in V$
8		coeq1	$⊢ f = F \to f \circ g = F \circ g$
9		coeq2	$⊢ g = G \to F \circ g = F \circ G$
10		eqid	$⊢ (f \in T, g \in T ⟼ f \circ g) = (f \in T, g \in T ⟼ f \circ g)$
11	8 9 10	ovmpog	$⊢ (F \in T \land G \in T \land F \circ G \in V) \to F (f \in T, g \in T ⟼ f \circ g) G = F \circ G$
12	7 11	mpd3an3	$⊢ (F \in T \land G \in T) \to F (f \in T, g \in T ⟼ f \circ g) G = F \circ G$
13	6 12	sylan9eq	$⊢ ((K \in V \land W \in H) \land (F \in T \land G \in T)) \to F \underset{˙}{+} G = F \circ G$

Metamath Proof Explorer