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 imbitrrid ⊢ ( ( ( 𝑅 ∈ 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 imbitrrid ⊢ ( ( ( 𝑅 ∈ 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 ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑁 · 𝑋 ) × 𝑌 ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) )