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

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) Generalization of ringsubdir . (Revised by AV, 23-Feb-2025)

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

Proof

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