This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulgass3

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

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

Proof

Step Hyp Ref Expression
1 mulgass3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 mulgass3.m ⊢ · = ( .g ‘ 𝑅 )
3 mulgass3.t ⊢ × = ( .r ‘ 𝑅 )
4 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
5 4 opprring ⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
6 5 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( oppr ‘ 𝑅 ) ∈ Ring )
7 simpr1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑁 ∈ ℤ )
8 simpr3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
9 simpr2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
10 4 1 opprbas ⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
11 eqid ⊢ ( .g ‘ ( oppr ‘ 𝑅 ) ) = ( .g ‘ ( oppr ‘ 𝑅 ) )
12 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
13 10 11 12 mulgass2 ⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ) )
14 6 7 8 9 13 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ) )
15 1 3 4 12 opprmul ⊢ ( ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑋 × ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) )
16 1 3 4 12 opprmul ⊢ ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑋 × 𝑌 )
17 16 oveq2i ⊢ ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ) = ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) ( 𝑋 × 𝑌 ) )
18 14 15 17 3eqtr3g ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 × ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) ) = ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) ( 𝑋 × 𝑌 ) ) )
19 1 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝑅 ) )
20 10 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) ) )
21 ssv ⊢ 𝐵 ⊆ V
22 21 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐵 ⊆ V )
23 ovexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ V )
24 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
25 4 24 oppradd ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( oppr ‘ 𝑅 ) )
26 25 oveqi ⊢ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( oppr ‘ 𝑅 ) ) 𝑦 )
27 26 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( oppr ‘ 𝑅 ) ) 𝑦 ) )
28 2 11 19 20 22 23 27 mulgpropd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → · = ( .g ‘ ( oppr ‘ 𝑅 ) ) )
29 28 oveqd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑁 · 𝑌 ) = ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) )
30 29 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 × ( 𝑁 · 𝑌 ) ) = ( 𝑋 × ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) 𝑌 ) ) )
31 28 oveqd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑁 · ( 𝑋 × 𝑌 ) ) = ( 𝑁 ( .g ‘ ( oppr ‘ 𝑅 ) ) ( 𝑋 × 𝑌 ) ) )
32 18 30 31 3eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 × ( 𝑁 · 𝑌 ) ) = ( 𝑁 · ( 𝑋 × 𝑌 ) ) )