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 ( 𝜑 → ( ( 𝑋 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) ( 𝑌 · 𝑍 ) ) )