srgmulgass

Description: An associative property between group multiple and ring multiplication for semirings. (Contributed by AV, 23-Aug-2019)

	Ref	Expression
Hypotheses	srgmulgass.b	$⊢ B = {Base}_{R}$
	srgmulgass.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	srgmulgass.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
Assertion	srgmulgass	$⊢ (R \in SRing \land (N \in ℕ_{0} \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		srgmulgass.b	$⊢ B = {Base}_{R}$
2		srgmulgass.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		srgmulgass.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	7	imbi2d	$⊢ x = 0 \to ((((X \in B \land Y \in B) \land R \in SRing) \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = x \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) \leftrightarrow (((X \in B \land Y \in B) \land R \in SRing) \to (0 \underset{˙}{\cdot} X) \underset{˙}{\times} Y = 0 \underset{˙}{\cdot} (X \underset{˙}{\times} Y)))$
9		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} X = y \underset{˙}{\cdot} X$
10	9	oveq1d	$⊢ x = y \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (y \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
11		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
12	10 11	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))$
13	12	imbi2d	$⊢ x = y \to ((((X \in B \land Y \in B) \land R \in SRing) \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = x \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) \leftrightarrow (((X \in B \land Y \in B) \land R \in SRing) \to (y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)))$
14		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\cdot} X = (y + 1) \underset{˙}{\cdot} X$
15	14	oveq1d	$⊢ x = y + 1 \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
16		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
17	15 16	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))$
18	17	imbi2d	$⊢ x = y + 1 \to ((((X \in B \land Y \in B) \land R \in SRing) \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = x \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) \leftrightarrow (((X \in B \land Y \in B) \land R \in SRing) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)))$
19		oveq1	$⊢ x = N \to x \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$
20	19	oveq1d	$⊢ x = N \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y$
21		oveq1	$⊢ x = N \to x \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
22	20 21	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))$
23	22	imbi2d	$⊢ x = N \to ((((X \in B \land Y \in B) \land R \in SRing) \to (x \underset{˙}{\cdot} X) \underset{˙}{\times} Y = x \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) \leftrightarrow (((X \in B \land Y \in B) \land R \in SRing) \to (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y)))$
24		simpr	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to R \in SRing$
25		simpr	$⊢ (X \in B \land Y \in B) \to Y \in B$
26	25	adantr	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to Y \in B$
27		eqid	$⊢ 0_{R} = 0_{R}$
28	1 3 27	srglz	$⊢ (R \in SRing \land Y \in B) \to 0_{R} \underset{˙}{\times} Y = 0_{R}$
29	24 26 28	syl2anc	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to 0_{R} \underset{˙}{\times} Y = 0_{R}$
30		simpl	$⊢ (X \in B \land Y \in B) \to X \in B$
31	30	adantr	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to X \in B$
32	1 27 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{R}$
33	31 32	syl	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to 0 \underset{˙}{\cdot} X = 0_{R}$
34	33	oveq1d	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to (0 \underset{˙}{\cdot} X) \underset{˙}{\times} Y = 0_{R} \underset{˙}{\times} Y$
35	1 3	srgcl	$⊢ (R \in SRing \land X \in B \land Y \in B) \to X \underset{˙}{\times} Y \in B$
36	24 31 26 35	syl3anc	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to X \underset{˙}{\times} Y \in B$
37	1 27 2	mulg0	$⊢ X \underset{˙}{\times} Y \in B \to 0 \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = 0_{R}$
38	36 37	syl	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to 0 \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = 0_{R}$
39	29 34 38	3eqtr4d	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to (0 \underset{˙}{\cdot} X) \underset{˙}{\times} Y = 0 \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
40		srgmnd	$⊢ R \in SRing \to R \in Mnd$
41	40	adantl	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to R \in Mnd$
42	41	adantl	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to R \in Mnd$
43		simpl	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to y \in ℕ_{0}$
44	31	adantl	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to X \in B$
45		eqid	$⊢ +_{R} = +_{R}$
46	1 2 45	mulgnn0p1	$⊢ (R \in Mnd \land y \in ℕ_{0} \land X \in B) \to (y + 1) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) +_{R} X$
47	42 43 44 46	syl3anc	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to (y + 1) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) +_{R} X$
48	47	oveq1d	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = ((y \underset{˙}{\cdot} X) +_{R} X) \underset{˙}{\times} Y$
49	24	adantl	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to R \in SRing$
50	1 2 42 43 44	mulgnn0cld	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to y \underset{˙}{\cdot} X \in B$
51	26	adantl	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to Y \in B$
52	1 45 3	srgdir	$⊢ (R \in SRing \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	49 50 44 51 52	syl13anc	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to ((y \underset{˙}{\cdot} X) +_{R} X) \underset{˙}{\times} Y = ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y) +_{R} (X \underset{˙}{\times} Y)$
54	48 53	eqtrd	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y) +_{R} (X \underset{˙}{\times} Y)$
55	54	adantr	$⊢ ((y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \land (y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = ((y \underset{˙}{\cdot} X) \underset{˙}{\times} Y) +_{R} (X \underset{˙}{\times} Y)$
56		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)$
57	35	3expb	$⊢ (R \in SRing \land (X \in B \land Y \in B)) \to X \underset{˙}{\times} Y \in B$
58	57	ancoms	$⊢ ((X \in B \land Y \in B) \land R \in SRing) \to X \underset{˙}{\times} Y \in B$
59	58	adantl	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to X \underset{˙}{\times} Y \in B$
60	1 2 45	mulgnn0p1	$⊢ (R \in Mnd \land y \in ℕ_{0} \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)$
61	42 43 59 60	syl3anc	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = (y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) +_{R} (X \underset{˙}{\times} Y)$
62	61	eqcomd	$⊢ (y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \to (y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) +_{R} (X \underset{˙}{\times} Y) = (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
63	56 62	sylan9eqr	$⊢ ((y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \land (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 + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
64	55 63	eqtrd	$⊢ ((y \in ℕ_{0} \land ((X \in B \land Y \in B) \land R \in SRing)) \land (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)$
65	64	exp31	$⊢ y \in ℕ_{0} \to (((X \in B \land Y \in B) \land R \in SRing) \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)))$
66	65	a2d	$⊢ y \in ℕ_{0} \to ((((X \in B \land Y \in B) \land R \in SRing) \to (y \underset{˙}{\cdot} X) \underset{˙}{\times} Y = y \underset{˙}{\cdot} (X \underset{˙}{\times} Y)) \to (((X \in B \land Y \in B) \land R \in SRing) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (y + 1) \underset{˙}{\cdot} (X \underset{˙}{\times} Y)))$
67	8 13 18 23 39 66	nn0ind	$⊢ N \in ℕ_{0} \to (((X \in B \land Y \in B) \land R \in SRing) \to (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
68	67	expd	$⊢ N \in ℕ_{0} \to ((X \in B \land Y \in B) \to (R \in SRing \to (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y)))$
69	68	3impib	$⊢ (N \in ℕ_{0} \land X \in B \land Y \in B) \to (R \in SRing \to (N \underset{˙}{\cdot} X) \underset{˙}{\times} Y = N \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$
70	69	impcom	$⊢ (R \in SRing \land (N \in ℕ_{0} \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 srgmulgass

Proof