Metamath Proof Explorer

Theorem rngsubdir

Description: Ring multiplication distributes over subtraction. ( subdir analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014)

Ref Expression
Hypotheses ringsubdi.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringsubdi.t ⊢ · = ( .r ‘ 𝑅 )
ringsubdi.m ⊢ − = ( -g ‘ 𝑅 )
ringsubdi.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ringsubdi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ringsubdi.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
ringsubdi.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion rngsubdir ( 𝜑 → ( ( 𝑋 − 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) − ( 𝑌 · 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 ringsubdi.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringsubdi.t ⊢ · = ( .r ‘ 𝑅 )
3 ringsubdi.m ⊢ − = ( -g ‘ 𝑅 )
4 ringsubdi.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 ringsubdi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 ringsubdi.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 ringsubdi.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
9 4 8 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
10 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
11 1 10 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
12 9 6 11 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
13 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
14 1 13 2 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) · 𝑍 ) ) )
15 4 5 12 7 14 syl13anc ⊢ ( 𝜑 → ( ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) · 𝑍 ) ) )
16 1 2 10 4 6 7 ringmneg1 ⊢ ( 𝜑 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) · 𝑍 ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) )
17 16 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) · 𝑍 ) ) = ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) )
18 15 17 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) )
19 1 13 10 3 grpsubval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ) )
20 5 6 19 syl2anc ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ) )
21 20 oveq1d ⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) · 𝑍 ) = ( ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑍 ) )
22 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
23 4 5 7 22 syl3anc ⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
24 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 · 𝑍 ) ∈ 𝐵 )
25 4 6 7 24 syl3anc ⊢ ( 𝜑 → ( 𝑌 · 𝑍 ) ∈ 𝐵 )
26 1 13 10 3 grpsubval ⊢ ( ( ( 𝑋 · 𝑍 ) ∈ 𝐵 ∧ ( 𝑌 · 𝑍 ) ∈ 𝐵 ) → ( ( 𝑋 · 𝑍 ) − ( 𝑌 · 𝑍 ) ) = ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) )
27 23 25 26 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 · 𝑍 ) − ( 𝑌 · 𝑍 ) ) = ( ( 𝑋 · 𝑍 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) )
28 18 21 27 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) − ( 𝑌 · 𝑍 ) ) )