dvavsca

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

	Ref	Expression
Hypotheses	dvafvsca.h	$⊢ H = LHyp (K)$
	dvafvsca.t	$⊢ T = LTrn (K) (W)$
	dvafvsca.e	$⊢ E = TEndo (K) (W)$
	dvafvsca.u	$⊢ U = DVecA (K) (W)$
	dvafvsca.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
Assertion	dvavsca	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T)) \to R \underset{˙}{\cdot} F = R (F)$

Step	Hyp	Ref	Expression
1		dvafvsca.h	$⊢ H = LHyp (K)$
2		dvafvsca.t	$⊢ T = LTrn (K) (W)$
3		dvafvsca.e	$⊢ E = TEndo (K) (W)$
4		dvafvsca.u	$⊢ U = DVecA (K) (W)$
5		dvafvsca.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
6	1 2 3 4 5	dvafvsca	$⊢ (K \in V \land W \in H) \to \underset{˙}{\cdot} = (s \in E, f \in T ⟼ s (f))$
7	6	oveqd	$⊢ (K \in V \land W \in H) \to R \underset{˙}{\cdot} F = R (s \in E, f \in T ⟼ s (f)) F$
8		fveq1	$⊢ s = R \to s (f) = R (f)$
9		fveq2	$⊢ f = F \to R (f) = R (F)$
10		eqid	$⊢ (s \in E, f \in T ⟼ s (f)) = (s \in E, f \in T ⟼ s (f))$
11		fvex	$⊢ R (F) \in V$
12	8 9 10 11	ovmpo	$⊢ (R \in E \land F \in T) \to R (s \in E, f \in T ⟼ s (f)) F = R (F)$
13	7 12	sylan9eq	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T)) \to R \underset{˙}{\cdot} F = R (F)$

Metamath Proof Explorer