Metamath Proof Explorer


Theorem mulgass2

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

Ref Expression
Hypotheses mulgass2.b 𝐵 = ( Base ‘ 𝑅 )
mulgass2.m · = ( .g𝑅 )
mulgass2.t × = ( .r𝑅 )
Assertion mulgass2 ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mulgass2.b 𝐵 = ( Base ‘ 𝑅 )
2 mulgass2.m · = ( .g𝑅 )
3 mulgass2.t × = ( .r𝑅 )
4 oveq1 ( 𝑥 = 0 → ( 𝑥 · 𝑋 ) = ( 0 · 𝑋 ) )
5 4 oveq1d ( 𝑥 = 0 → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( ( 0 · 𝑋 ) × 𝑌 ) )
6 oveq1 ( 𝑥 = 0 → ( 𝑥 · ( 𝑋 × 𝑌 ) ) = ( 0 · ( 𝑋 × 𝑌 ) ) )
7 5 6 eqeq12d ( 𝑥 = 0 → ( ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ↔ ( ( 0 · 𝑋 ) × 𝑌 ) = ( 0 · ( 𝑋 × 𝑌 ) ) ) )
8 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 · 𝑋 ) = ( 𝑦 · 𝑋 ) )
9 8 oveq1d ( 𝑥 = 𝑦 → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( ( 𝑦 · 𝑋 ) × 𝑌 ) )
10 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 · ( 𝑋 × 𝑌 ) ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) )
11 9 10 eqeq12d ( 𝑥 = 𝑦 → ( ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ↔ ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) )
12 oveq1 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 · 𝑋 ) = ( ( 𝑦 + 1 ) · 𝑋 ) )
13 12 oveq1d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) )
14 oveq1 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 · ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) )
15 13 14 eqeq12d ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ↔ ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) ) )
16 oveq1 ( 𝑥 = - 𝑦 → ( 𝑥 · 𝑋 ) = ( - 𝑦 · 𝑋 ) )
17 16 oveq1d ( 𝑥 = - 𝑦 → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( ( - 𝑦 · 𝑋 ) × 𝑌 ) )
18 oveq1 ( 𝑥 = - 𝑦 → ( 𝑥 · ( 𝑋 × 𝑌 ) ) = ( - 𝑦 · ( 𝑋 × 𝑌 ) ) )
19 17 18 eqeq12d ( 𝑥 = - 𝑦 → ( ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ↔ ( ( - 𝑦 · 𝑋 ) × 𝑌 ) = ( - 𝑦 · ( 𝑋 × 𝑌 ) ) ) )
20 oveq1 ( 𝑥 = 𝑁 → ( 𝑥 · 𝑋 ) = ( 𝑁 · 𝑋 ) )
21 20 oveq1d ( 𝑥 = 𝑁 → ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( ( 𝑁 · 𝑋 ) × 𝑌 ) )
22 oveq1 ( 𝑥 = 𝑁 → ( 𝑥 · ( 𝑋 × 𝑌 ) ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) )
23 21 22 eqeq12d ( 𝑥 = 𝑁 → ( ( ( 𝑥 · 𝑋 ) × 𝑌 ) = ( 𝑥 · ( 𝑋 × 𝑌 ) ) ↔ ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) ) )
24 eqid ( 0g𝑅 ) = ( 0g𝑅 )
25 1 3 24 ringlz ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵 ) → ( ( 0g𝑅 ) × 𝑌 ) = ( 0g𝑅 ) )
26 25 3adant3 ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → ( ( 0g𝑅 ) × 𝑌 ) = ( 0g𝑅 ) )
27 simp3 ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → 𝑋𝐵 )
28 1 24 2 mulg0 ( 𝑋𝐵 → ( 0 · 𝑋 ) = ( 0g𝑅 ) )
29 27 28 syl ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → ( 0 · 𝑋 ) = ( 0g𝑅 ) )
30 29 oveq1d ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → ( ( 0 · 𝑋 ) × 𝑌 ) = ( ( 0g𝑅 ) × 𝑌 ) )
31 1 3 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
32 31 3com23 ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
33 1 24 2 mulg0 ( ( 𝑋 × 𝑌 ) ∈ 𝐵 → ( 0 · ( 𝑋 × 𝑌 ) ) = ( 0g𝑅 ) )
34 32 33 syl ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → ( 0 · ( 𝑋 × 𝑌 ) ) = ( 0g𝑅 ) )
35 26 30 34 3eqtr4d ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → ( ( 0 · 𝑋 ) × 𝑌 ) = ( 0 · ( 𝑋 × 𝑌 ) ) )
36 oveq1 ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g𝑅 ) ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 · ( 𝑋 × 𝑌 ) ) ( +g𝑅 ) ( 𝑋 × 𝑌 ) ) )
37 simpl1 ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → 𝑅 ∈ Ring )
38 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
39 37 38 syl ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → 𝑅 ∈ Grp )
40 nn0z ( 𝑦 ∈ ℕ0𝑦 ∈ ℤ )
41 40 adantl ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → 𝑦 ∈ ℤ )
42 27 adantr ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → 𝑋𝐵 )
43 eqid ( +g𝑅 ) = ( +g𝑅 )
44 1 2 43 mulgp1 ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) → ( ( 𝑦 + 1 ) · 𝑋 ) = ( ( 𝑦 · 𝑋 ) ( +g𝑅 ) 𝑋 ) )
45 39 41 42 44 syl3anc ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑦 + 1 ) · 𝑋 ) = ( ( 𝑦 · 𝑋 ) ( +g𝑅 ) 𝑋 ) )
46 45 oveq1d ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 · 𝑋 ) ( +g𝑅 ) 𝑋 ) × 𝑌 ) )
47 38 3ad2ant1 ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → 𝑅 ∈ Grp )
48 47 adantr ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → 𝑅 ∈ Grp )
49 1 2 mulgcl ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
50 48 41 42 49 syl3anc ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
51 simpl2 ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → 𝑌𝐵 )
52 1 43 3 ringdir ( ( 𝑅 ∈ Ring ∧ ( ( 𝑦 · 𝑋 ) ∈ 𝐵𝑋𝐵𝑌𝐵 ) ) → ( ( ( 𝑦 · 𝑋 ) ( +g𝑅 ) 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g𝑅 ) ( 𝑋 × 𝑌 ) ) )
53 37 50 42 51 52 syl13anc ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 · 𝑋 ) ( +g𝑅 ) 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g𝑅 ) ( 𝑋 × 𝑌 ) ) )
54 46 53 eqtrd ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g𝑅 ) ( 𝑋 × 𝑌 ) ) )
55 32 adantr ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
56 1 2 43 mulgp1 ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ ( 𝑋 × 𝑌 ) ∈ 𝐵 ) → ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 · ( 𝑋 × 𝑌 ) ) ( +g𝑅 ) ( 𝑋 × 𝑌 ) ) )
57 39 41 55 56 syl3anc ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 · ( 𝑋 × 𝑌 ) ) ( +g𝑅 ) ( 𝑋 × 𝑌 ) ) )
58 54 57 eqeq12d ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) ↔ ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) ( +g𝑅 ) ( 𝑋 × 𝑌 ) ) = ( ( 𝑦 · ( 𝑋 × 𝑌 ) ) ( +g𝑅 ) ( 𝑋 × 𝑌 ) ) ) )
59 36 58 syl5ibr ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) ) )
60 59 ex ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → ( 𝑦 ∈ ℕ0 → ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) × 𝑌 ) = ( ( 𝑦 + 1 ) · ( 𝑋 × 𝑌 ) ) ) ) )
61 fveq2 ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) → ( ( invg𝑅 ) ‘ ( ( 𝑦 · 𝑋 ) × 𝑌 ) ) = ( ( invg𝑅 ) ‘ ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) )
62 47 adantr ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → 𝑅 ∈ Grp )
63 nnz ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
64 63 adantl ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℤ )
65 27 adantr ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → 𝑋𝐵 )
66 eqid ( invg𝑅 ) = ( invg𝑅 )
67 1 2 66 mulgneg ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) → ( - 𝑦 · 𝑋 ) = ( ( invg𝑅 ) ‘ ( 𝑦 · 𝑋 ) ) )
68 62 64 65 67 syl3anc ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → ( - 𝑦 · 𝑋 ) = ( ( invg𝑅 ) ‘ ( 𝑦 · 𝑋 ) ) )
69 68 oveq1d ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → ( ( - 𝑦 · 𝑋 ) × 𝑌 ) = ( ( ( invg𝑅 ) ‘ ( 𝑦 · 𝑋 ) ) × 𝑌 ) )
70 simpl1 ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → 𝑅 ∈ Ring )
71 62 64 65 49 syl3anc ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
72 simpl2 ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → 𝑌𝐵 )
73 1 3 66 70 71 72 ringmneg1 ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → ( ( ( invg𝑅 ) ‘ ( 𝑦 · 𝑋 ) ) × 𝑌 ) = ( ( invg𝑅 ) ‘ ( ( 𝑦 · 𝑋 ) × 𝑌 ) ) )
74 69 73 eqtrd ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → ( ( - 𝑦 · 𝑋 ) × 𝑌 ) = ( ( invg𝑅 ) ‘ ( ( 𝑦 · 𝑋 ) × 𝑌 ) ) )
75 32 adantr ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑋 × 𝑌 ) ∈ 𝐵 )
76 1 2 66 mulgneg ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ ( 𝑋 × 𝑌 ) ∈ 𝐵 ) → ( - 𝑦 · ( 𝑋 × 𝑌 ) ) = ( ( invg𝑅 ) ‘ ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) )
77 62 64 75 76 syl3anc ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → ( - 𝑦 · ( 𝑋 × 𝑌 ) ) = ( ( invg𝑅 ) ‘ ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) )
78 74 77 eqeq12d ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → ( ( ( - 𝑦 · 𝑋 ) × 𝑌 ) = ( - 𝑦 · ( 𝑋 × 𝑌 ) ) ↔ ( ( invg𝑅 ) ‘ ( ( 𝑦 · 𝑋 ) × 𝑌 ) ) = ( ( invg𝑅 ) ‘ ( 𝑦 · ( 𝑋 × 𝑌 ) ) ) ) )
79 61 78 syl5ibr ( ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) ∧ 𝑦 ∈ ℕ ) → ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) → ( ( - 𝑦 · 𝑋 ) × 𝑌 ) = ( - 𝑦 · ( 𝑋 × 𝑌 ) ) ) )
80 79 ex ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → ( 𝑦 ∈ ℕ → ( ( ( 𝑦 · 𝑋 ) × 𝑌 ) = ( 𝑦 · ( 𝑋 × 𝑌 ) ) → ( ( - 𝑦 · 𝑋 ) × 𝑌 ) = ( - 𝑦 · ( 𝑋 × 𝑌 ) ) ) ) )
81 7 11 15 19 23 35 60 80 zindd ( ( 𝑅 ∈ Ring ∧ 𝑌𝐵𝑋𝐵 ) → ( 𝑁 ∈ ℤ → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) ) )
82 81 3exp ( 𝑅 ∈ Ring → ( 𝑌𝐵 → ( 𝑋𝐵 → ( 𝑁 ∈ ℤ → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) ) ) ) )
83 82 com24 ( 𝑅 ∈ Ring → ( 𝑁 ∈ ℤ → ( 𝑋𝐵 → ( 𝑌𝐵 → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) ) ) ) )
84 83 3imp2 ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) )