Metamath Proof Explorer

Theorem srgmulgass

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

Ref Expression
Hypotheses srgmulgass.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
srgmulgass.m ⊢ · = ( .g ‘ 𝑅 )
srgmulgass.t ⊢ × = ( .r ‘ 𝑅 )
Assertion srgmulgass ( ( 𝑅 ∈ SRing ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 srgmulgass.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 srgmulgass.m ⊢ · = ( .g ‘ 𝑅 )
3 srgmulgass.t ⊢ × = ( .r ‘ 𝑅 )
4 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 · 𝑋 ) = ( 0 · 𝑋 ) )
5 4 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( ( 0 · 𝑋 ) × 𝑌 ) )
6 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 · ( 𝑋 × 𝑌 ) ) = ( 0 · ( 𝑋 × 𝑌 ) ) )
7 5 6 eqeq12d ⊢ ( 𝑥 = 0 → ( ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ↔ ( ( 0 · 𝑋 ) × 𝑌 ) = ( 0 · ( 𝑋 × 𝑌 ) ) ) )
8 7 imbi2d ⊢ ( 𝑥 = 0 → ( ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ) ↔ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 0 · 𝑋 ) × 𝑌 ) = ( 0 · ( 𝑋 × 𝑌 ) ) ) ) )
9 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 · 𝑋 ) = ( 𝑦 · 𝑋 ) )
10 9 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( ( 𝑦 · 𝑋 ) × 𝑌 ) )
11 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 · ( 𝑋 × 𝑌 ) ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) )
12 10 11 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ↔ ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) )
13 12 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ) ↔ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) ) )
14 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 · 𝑋 ) = ( ( 𝑦 + 1 ) · 𝑋 ) )
15 14 oveq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) )
16 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 · ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) )
17 15 16 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ↔ ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) ) )
18 17 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ) ↔ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) ) ) )
19 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 · 𝑋 ) = ( 𝑁 · 𝑋 ) )
20 19 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( ( 𝑁 · 𝑋 ) × 𝑌 ) )
21 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 · ( 𝑋 × 𝑌 ) ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) )
22 20 21 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ↔ ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) ) )
23 22 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ) ↔ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) ) ) )
24 simpr ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → 𝑅 ∈ SRing )
25 simpr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
26 25 adantr ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → 𝑌 ∈ 𝐵 )
27 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
28 1 3 27 srglz ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑌 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) × 𝑌 ) = ( 0g ‘ 𝑅 ) )
29 24 26 28 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 0g ‘ 𝑅 ) × 𝑌 ) = ( 0g ‘ 𝑅 ) )
30 simpl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
31 30 adantr ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → 𝑋 ∈ 𝐵 )
32 1 27 2 mulg0 ⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝑅 ) )
33 31 32 syl ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝑅 ) )
34 33 oveq1d ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 0 · 𝑋 ) × 𝑌 ) = ( ( 0g ‘ 𝑅 ) × 𝑌 ) )
35 1 3 srgcl ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
36 24 31 26 35 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
37 1 27 2 mulg0 ⊢ ( ( 𝑋 × 𝑌 ) ∈ 𝐵 → ( 0 · ( 𝑋 × 𝑌 ) ) = ( 0g ‘ 𝑅 ) )
38 36 37 syl ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( 0 · ( 𝑋 × 𝑌 ) ) = ( 0g ‘ 𝑅 ) )
39 29 34 38 3eqtr4d ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 0 · 𝑋 ) × 𝑌 ) = ( 0 · ( 𝑋 × 𝑌 ) ) )
40 srgmnd ⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
41 40 adantl ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → 𝑅 ∈ Mnd )
42 41 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → 𝑅 ∈ Mnd )
43 simpl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → 𝑦 ∈ ℕ0 )
44 31 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → 𝑋 ∈ 𝐵 )
45 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
46 1 2 45 mulgnn0p1 ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑦 + 1 ) · 𝑋 ) = ( ( 𝑦 · 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) )
47 42 43 44 46 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → ( ( 𝑦 + 1 ) · 𝑋 ) = ( ( 𝑦 · 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) )
48 47 oveq1d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 · 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) × 𝑌 ) )
49 24 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → 𝑅 ∈ SRing )
50 1 2 mulgnn0cl ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
51 42 43 44 50 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
52 26 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → 𝑌 ∈ 𝐵 )
53 1 45 3 srgdir ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑦 · 𝑋 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑦 · 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) )
54 49 51 44 52 53 syl13anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → ( ( ( 𝑦 · 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) )
55 48 54 eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) )
56 55 adantr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) ∧ ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) )
57 oveq1 ⊢ ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 · ( 𝑋 × 𝑌 ) ) ( +g ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) )
58 35 3expb ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
59 58 ancoms ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
60 59 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
61 1 2 45 mulgnn0p1 ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ ( 𝑋 × 𝑌 ) ∈ 𝐵 ) → ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 · ( 𝑋 × 𝑌 ) ) ( +g ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) )
62 42 43 60 61 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 · ( 𝑋 × 𝑌 ) ) ( +g ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) )
63 62 eqcomd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) → ( ( 𝑦 · ( 𝑋 × 𝑌 ) ) ( +g ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) )
64 57 63 sylan9eqr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) ∧ ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) → ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g ‘ 𝑅 ) ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) )
65 56 64 eqtrd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) ) ∧ ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) )
66 65 exp31 ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) ) ) )
67 66 a2d ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) → ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) ) ) )
68 8 13 18 23 39 67 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑅 ∈ SRing ) → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) ) )
69 68 expd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑅 ∈ SRing → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) ) ) )
70 69 3impib ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑅 ∈ SRing → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) ) )
71 70 impcom ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) )