dvaplusgv

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

	Ref	Expression
Hypotheses	dvafplus.h	$⊢ H = LHyp (K)$
	dvafplus.t	$⊢ T = LTrn (K) (W)$
	dvafplus.e	$⊢ E = TEndo (K) (W)$
	dvafplus.u	$⊢ U = DVecA (K) (W)$
	dvafplus.f	$⊢ F = Scalar (U)$
	dvafplus.p	$⊢ \underset{˙}{+} = +_{F}$
Assertion	dvaplusgv	$⊢ ((K \in V \land W \in H) \land (R \in E \land S \in E \land G \in T)) \to (R \underset{˙}{+} S) (G) = R (G) \circ S (G)$

Step	Hyp	Ref	Expression
1		dvafplus.h	$⊢ H = LHyp (K)$
2		dvafplus.t	$⊢ T = LTrn (K) (W)$
3		dvafplus.e	$⊢ E = TEndo (K) (W)$
4		dvafplus.u	$⊢ U = DVecA (K) (W)$
5		dvafplus.f	$⊢ F = Scalar (U)$
6		dvafplus.p	$⊢ \underset{˙}{+} = +_{F}$
7	1 2 3 4 5 6	dvaplusg	$⊢ ((K \in V \land W \in H) \land (R \in E \land S \in E)) \to R \underset{˙}{+} S = (f \in T ⟼ R (f) \circ S (f))$
8	7	fveq1d	$⊢ ((K \in V \land W \in H) \land (R \in E \land S \in E)) \to (R \underset{˙}{+} S) (G) = (f \in T ⟼ R (f) \circ S (f)) (G)$
9	8	3adantr3	$⊢ ((K \in V \land W \in H) \land (R \in E \land S \in E \land G \in T)) \to (R \underset{˙}{+} S) (G) = (f \in T ⟼ R (f) \circ S (f)) (G)$
10		simpr3	$⊢ ((K \in V \land W \in H) \land (R \in E \land S \in E \land G \in T)) \to G \in T$
11		fveq2	$⊢ f = G \to R (f) = R (G)$
12		fveq2	$⊢ f = G \to S (f) = S (G)$
13	11 12	coeq12d	$⊢ f = G \to R (f) \circ S (f) = R (G) \circ S (G)$
14		eqid	$⊢ (f \in T ⟼ R (f) \circ S (f)) = (f \in T ⟼ R (f) \circ S (f))$
15		fvex	$⊢ R (G) \in V$
16		fvex	$⊢ S (G) \in V$
17	15 16	coex	$⊢ R (G) \circ S (G) \in V$
18	13 14 17	fvmpt	$⊢ G \in T \to (f \in T ⟼ R (f) \circ S (f)) (G) = R (G) \circ S (G)$
19	10 18	syl	$⊢ ((K \in V \land W \in H) \land (R \in E \land S \in E \land G \in T)) \to (f \in T ⟼ R (f) \circ S (f)) (G) = R (G) \circ S (G)$
20	9 19	eqtrd	$⊢ ((K \in V \land W \in H) \land (R \in E \land S \in E \land G \in T)) \to (R \underset{˙}{+} S) (G) = R (G) \circ S (G)$

Metamath Proof Explorer