mulgass2

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

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

Proof

Step	Hyp	Ref	Expression
1		mulgass2.b	$⊢ B = {Base}_{R}$
2		mulgass2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		mulgass2.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
4		oveq1	$⊢ x = 0 \to x \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
5	4	oveq1d	$⊢ x = 0 \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (0 \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
6		oveq1	$⊢ x = 0 \to x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = 0 \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
7	5 6	eqeq12d	$⊢ x = 0 \to ((x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \leftrightarrow (0 \underset{˙}{\cdot} X) \underset{˙}{\times} Y = 0 \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
8		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} X = y \underset{˙}{\cdot} X$
9	8	oveq1d	$⊢ x = y \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (y \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
10		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
11	9 10	eqeq12d	$⊢ x = y \to ((x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \leftrightarrow (y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
12		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\cdot} X = (y + 1) \underset{˙}{\cdot} X$
13	12	oveq1d	$⊢ x = y + 1 \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
14		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
15	13 14	eqeq12d	$⊢ x = y + 1 \to ((x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \leftrightarrow ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
16		oveq1	$⊢ x = - y \to x \underset{˙}{\cdot} X = (- y) \underset{˙}{\cdot} X$
17	16	oveq1d	$⊢ x = - y \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = ((- y) \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
18		oveq1	$⊢ x = - y \to x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = (- y) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
19	17 18	eqeq12d	$⊢ x = - y \to ((x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \leftrightarrow ((- y) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (- y) \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
20		oveq1	$⊢ x = N \to x \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$
21	20	oveq1d	$⊢ x = N \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
22		oveq1	$⊢ x = N \to x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
23	21 22	eqeq12d	$⊢ x = N \to ((x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \leftrightarrow (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
24		eqid	$⊢ 0_{R} = 0_{R}$
25	1 3 24	ringlz	$⊢ (R \in Ring \land Y \in B) \to 0_{R} \underset{˙}{\times} Y = 0_{R}$
26	25	3adant3	$⊢ (R \in Ring \land Y \in B \land X \in B) \to 0_{R} \underset{˙}{\times} Y = 0_{R}$
27		simp3	$⊢ (R \in Ring \land Y \in B \land X \in B) \to X \in B$
28	1 24 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{R}$
29	27 28	syl	$⊢ (R \in Ring \land Y \in B \land X \in B) \to 0 \underset{˙}{\cdot} X = 0_{R}$
30	29	oveq1d	$⊢ (R \in Ring \land Y \in B \land X \in B) \to (0 \underset{˙}{\cdot} X) \underset{˙}{\times} Y = 0_{R} \underset{˙}{\times} Y$
31	1 3	ringcl	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \underset{˙}{\times} Y \in B$
32	31	3com23	$⊢ (R \in Ring \land Y \in B \land X \in B) \to X \underset{˙}{\times} Y \in B$
33	1 24 2	mulg0	$⊢ X \underset{˙}{\times} Y \in B \to 0 \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = 0_{R}$
34	32 33	syl	$⊢ (R \in Ring \land Y \in B \land X \in B) \to 0 \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = 0_{R}$
35	26 30 34	3eqtr4d	$⊢ (R \in Ring \land Y \in B \land X \in B) \to (0 \underset{˙}{\cdot} X) \underset{˙}{\times} Y = 0 \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
36		oveq1	$⊢ (y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \to ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y) +_{R} (X \underset{˙}{\times} Y) = (y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) +_{R} (X \underset{˙}{\times} Y)$
37		simpl1	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to R \in Ring$
38		ringgrp	$⊢ R \in Ring \to R \in Grp$
39	37 38	syl	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to R \in Grp$
40		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
41	40	adantl	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to y \in ℤ$
42	27	adantr	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to X \in B$
43		eqid	$⊢ +_{R} = +_{R}$
44	1 2 43	mulgp1	$⊢ (R \in Grp \land y \in ℤ \land X \in B) \to (y + 1) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) +_{R} X$
45	39 41 42 44	syl3anc	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to (y + 1) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) +_{R} X$
46	45	oveq1d	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = ((y \underset{˙}{\cdot} X) +_{R} X) \underset{˙}{\times} Y$
47	38	3ad2ant1	$⊢ (R \in Ring \land Y \in B \land X \in B) \to R \in Grp$
48	47	adantr	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to R \in Grp$
49	1 2	mulgcl	$⊢ (R \in Grp \land y \in ℤ \land X \in B) \to y \underset{˙}{\cdot} X \in B$
50	48 41 42 49	syl3anc	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to y \underset{˙}{\cdot} X \in B$
51		simpl2	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to Y \in B$
52	1 43 3	ringdir	$⊢ (R \in Ring \land (y \underset{˙}{\cdot} X \in B \land X \in B \land Y \in B)) \to ((y \underset{˙}{\cdot} X) +_{R} X) \underset{˙}{\times} Y = ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y) +_{R} (X \underset{˙}{\times} Y)$
53	37 50 42 51 52	syl13anc	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to ((y \underset{˙}{\cdot} X) +_{R} X) \underset{˙}{\times} Y = ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y) +_{R} (X \underset{˙}{\times} Y)$
54	46 53	eqtrd	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y) +_{R} (X \underset{˙}{\times} Y)$
55	32	adantr	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to X \underset{˙}{\times} Y \in B$
56	1 2 43	mulgp1	$⊢ (R \in Grp \land y \in ℤ \land X \underset{˙}{\times} Y \in B) \to (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = (y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) +_{R} (X \underset{˙}{\times} Y)$
57	39 41 55 56	syl3anc	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = (y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) +_{R} (X \underset{˙}{\times} Y)$
58	54 57	eqeq12d	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to (((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \leftrightarrow ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y) +_{R} (X \underset{˙}{\times} Y) = (y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) +_{R} (X \underset{˙}{\times} Y))$
59	36 58	imbitrrid	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ_{0}) \to ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
60	59	ex	$⊢ (R \in Ring \land Y \in B \land X \in B) \to (y \in ℕ_{0} \to ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)))$
61		fveq2	$⊢ (y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \to {inv}_{g} (R) ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y) = {inv}_{g} (R) (y \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
62	47	adantr	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to R \in Grp$
63		nnz	$⊢ y \in ℕ \to y \in ℤ$
64	63	adantl	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to y \in ℤ$
65	27	adantr	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to X \in B$
66		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
67	1 2 66	mulgneg	$⊢ (R \in Grp \land y \in ℤ \land X \in B) \to (- y) \underset{˙}{\cdot} X = {inv}_{g} (R) (y \underset{˙}{\cdot} X)$
68	62 64 65 67	syl3anc	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to (- y) \underset{˙}{\cdot} X = {inv}_{g} (R) (y \underset{˙}{\cdot} X)$
69	68	oveq1d	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = {inv}_{g} (R) (y \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
70		simpl1	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to R \in Ring$
71	62 64 65 49	syl3anc	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to y \underset{˙}{\cdot} X \in B$
72		simpl2	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to Y \in B$
73	1 3 66 70 71 72	ringmneg1	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to {inv}_{g} (R) (y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = {inv}_{g} (R) ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y)$
74	69 73	eqtrd	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = {inv}_{g} (R) ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y)$
75	32	adantr	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to X \underset{˙}{\times} Y \in B$
76	1 2 66	mulgneg	$⊢ (R \in Grp \land y \in ℤ \land X \underset{˙}{\times} Y \in B) \to (- y) \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = {inv}_{g} (R) (y \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
77	62 64 75 76	syl3anc	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to (- y) \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = {inv}_{g} (R) (y \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
78	74 77	eqeq12d	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to (((- y) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (- y) \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \leftrightarrow {inv}_{g} (R) ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y) = {inv}_{g} (R) (y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)))$
79	61 78	imbitrrid	$⊢ ((R \in Ring \land Y \in B \land X \in B) \land y \in ℕ) \to ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (- y) \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
80	79	ex	$⊢ (R \in Ring \land Y \in B \land X \in B) \to (y \in ℕ \to ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (- y) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)))$
81	7 11 15 19 23 35 60 80	zindd	$⊢ (R \in Ring \land Y \in B \land X \in B) \to (N \in ℤ \to (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
82	81	3exp	$⊢ R \in Ring \to (Y \in B \to (X \in B \to (N \in ℤ \to (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y))))$
83	82	com24	$⊢ R \in Ring \to (N \in ℤ \to (X \in B \to (Y \in B \to (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y))))$
84	83	3imp2	$⊢ (R \in Ring \land (N \in ℤ \land X \in B \land Y \in B)) \to (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Metamath Proof Explorer

Theorem mulgass2

Proof