erngmul-rN

Description: Ring addition operation. (Contributed by NM, 10-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	erngset.h-r	$⊢ H = LHyp (K)$
	erngset.t-r	$⊢ T = LTrn (K) (W)$
	erngset.e-r	$⊢ E = TEndo (K) (W)$
	erngset.d-r	$⊢ D = {EDRing}_{R} (K) (W)$
	erng.m-r	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
Assertion	erngmul-rN	$⊢ ((K \in X \land W \in H) \land (U \in E \land V \in E)) \to U \underset{˙}{\cdot} V = V \circ U$

Step	Hyp	Ref	Expression
1		erngset.h-r	$⊢ H = LHyp (K)$
2		erngset.t-r	$⊢ T = LTrn (K) (W)$
3		erngset.e-r	$⊢ E = TEndo (K) (W)$
4		erngset.d-r	$⊢ D = {EDRing}_{R} (K) (W)$
5		erng.m-r	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
6	1 2 3 4 5	erngfmul-rN	$⊢ (K \in X \land W \in H) \to \underset{˙}{\cdot} = (s \in E, t \in E ⟼ t \circ s)$
7	6	adantr	$⊢ ((K \in X \land W \in H) \land (U \in E \land V \in E)) \to \underset{˙}{\cdot} = (s \in E, t \in E ⟼ t \circ s)$
8	7	oveqd	$⊢ ((K \in X \land W \in H) \land (U \in E \land V \in E)) \to U \underset{˙}{\cdot} V = U (s \in E, t \in E ⟼ t \circ s) V$
9		coexg	$⊢ (V \in E \land U \in E) \to V \circ U \in V$
10	9	ancoms	$⊢ (U \in E \land V \in E) \to V \circ U \in V$
11		coeq2	$⊢ s = U \to t \circ s = t \circ U$
12		coeq1	$⊢ t = V \to t \circ U = V \circ U$
13		eqid	$⊢ (s \in E, t \in E ⟼ t \circ s) = (s \in E, t \in E ⟼ t \circ s)$
14	11 12 13	ovmpog	$⊢ (U \in E \land V \in E \land V \circ U \in V) \to U (s \in E, t \in E ⟼ t \circ s) V = V \circ U$
15	10 14	mpd3an3	$⊢ (U \in E \land V \in E) \to U (s \in E, t \in E ⟼ t \circ s) V = V \circ U$
16	15	adantl	$⊢ ((K \in X \land W \in H) \land (U \in E \land V \in E)) \to U (s \in E, t \in E ⟼ t \circ s) V = V \circ U$
17	8 16	eqtrd	$⊢ ((K \in X \land W \in H) \land (U \in E \land V \in E)) \to U \underset{˙}{\cdot} V = V \circ U$

Metamath Proof Explorer