mulgass3

Description: An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	mulgass3.b	$⊢ B = {Base}_{R}$
	mulgass3.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mulgass3.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
Assertion	mulgass3	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to X \underset{˙}{\times} (N \underset{˙}{\cdot} Y) = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Proof

Step	Hyp	Ref	Expression
1		mulgass3.b	$⊢ B = {Base}_{R}$
2		mulgass3.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		mulgass3.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
4		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
5	4	opprring	$⊢ R \in Ring \to {opp}_{r} (R) \in Ring$
6	5	adantr	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to {opp}_{r} (R) \in Ring$
7		simpr1	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to N \in ℤ$
8		simpr3	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to Y \in B$
9		simpr2	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to X \in B$
10	4 1	opprbas	$⊢ B = {Base}_{{opp}_{r} (R)}$
11		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
12		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
13	10 11 12	mulgass2	$⊢ ({opp}_{r} (R) \in Ring \land (N \in ℤ \land Y \in B \land X \in B)) \to (N \cdot_{{opp}_{r} (R)} Y) \cdot_{{opp}_{r} (R)} X = N \cdot_{{opp}_{r} (R)} (Y \cdot_{{opp}_{r} (R)} X)$
14	6 7 8 9 13	syl13anc	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to (N \cdot_{{opp}_{r} (R)} Y) \cdot_{{opp}_{r} (R)} X = N \cdot_{{opp}_{r} (R)} (Y \cdot_{{opp}_{r} (R)} X)$
15	1 3 4 12	opprmul	$⊢ (N \cdot_{{opp}_{r} (R)} Y) \cdot_{{opp}_{r} (R)} X = X \underset{˙}{\times} (N \cdot_{{opp}_{r} (R)} Y)$
16	1 3 4 12	opprmul	$⊢ Y \cdot_{{opp}_{r} (R)} X = X \underset{˙}{\times} Y$
17	16	oveq2i	$⊢ N \cdot_{{opp}_{r} (R)} (Y \cdot_{{opp}_{r} (R)} X) = N \cdot_{{opp}_{r} (R)} (X \underset{˙}{\times} Y)$
18	14 15 17	3eqtr3g	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to X \underset{˙}{\times} (N \cdot_{{opp}_{r} (R)} Y) = N \cdot_{{opp}_{r} (R)} (X \underset{˙}{\times} Y)$
19	1	a1i	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to B = {Base}_{R}$
20	10	a1i	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to B = {Base}_{{opp}_{r} (R)}$
21		ssv	$⊢ B \subseteq V$
22	21	a1i	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to B \subseteq V$
23		ovexd	$⊢ ((R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \land (x \in V \land y \in V)) \to x +_{R} y \in V$
24		eqid	$⊢ +_{R} = +_{R}$
25	4 24	oppradd	$⊢ +_{R} = +_{{opp}_{r} (R)}$
26	25	oveqi	$⊢ x +_{R} y = x +_{{opp}_{r} (R)} y$
27	26	a1i	$⊢ ((R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \land (x \in V \land y \in V)) \to x +_{R} y = x +_{{opp}_{r} (R)} y$
28	2 11 19 20 22 23 27	mulgpropd	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to \underset{˙}{\cdot} = \cdot_{{opp}_{r} (R)}$
29	28	oveqd	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to N \underset{˙}{\cdot} Y = N \cdot_{{opp}_{r} (R)} Y$
30	29	oveq2d	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to X \underset{˙}{\times} (N \underset{˙}{\cdot} Y) = X \underset{˙}{\times} (N \cdot_{{opp}_{r} (R)} Y)$
31	28	oveqd	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to N \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = N \cdot_{{opp}_{r} (R)} (X \underset{˙}{\times} Y)$
32	18 30 31	3eqtr4d	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to X \underset{˙}{\times} (N \underset{˙}{\cdot} Y) = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Metamath Proof Explorer

Theorem mulgass3

Proof