Metamath Proof Explorer

Theorem dvrdir

Description: Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017)

Ref Expression
Hypotheses dvrdir.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvrdir.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dvrdir.p ⊢ + = ( +g ‘ 𝑅 )
dvrdir.t ⊢ / = ( /r ‘ 𝑅 )
Assertion dvrdir ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 + 𝑌 ) / 𝑍 ) = ( ( 𝑋 / 𝑍 ) + ( 𝑌 / 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 dvrdir.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dvrdir.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 dvrdir.p ⊢ + = ( +g ‘ 𝑅 )
4 dvrdir.t ⊢ / = ( /r ‘ 𝑅 )
5 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑅 ∈ Ring )
6 simpr1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
7 simpr2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑌 ∈ 𝐵 )
8 1 2 unitss ⊢ 𝑈 ⊆ 𝐵
9 simpr3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑍 ∈ 𝑈 )
10 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
11 2 10 unitinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝑈 )
12 9 11 syldan ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝑈 )
13 8 12 sselid ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 )
14 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
15 1 3 14 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = ( ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) + ( 𝑌 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
16 5 6 7 13 15 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 + 𝑌 ) ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = ( ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) + ( 𝑌 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
17 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
18 17 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑅 ∈ Grp )
19 1 3 grpcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
20 18 6 7 19 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
21 1 14 2 10 4 dvrval ⊢ ( ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) → ( ( 𝑋 + 𝑌 ) / 𝑍 ) = ( ( 𝑋 + 𝑌 ) ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
22 20 9 21 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 + 𝑌 ) / 𝑍 ) = ( ( 𝑋 + 𝑌 ) ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
23 1 14 2 10 4 dvrval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑋 / 𝑍 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
24 6 9 23 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑋 / 𝑍 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
25 1 14 2 10 4 dvrval ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑌 / 𝑍 ) = ( 𝑌 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
26 7 9 25 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑌 / 𝑍 ) = ( 𝑌 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
27 24 26 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 / 𝑍 ) + ( 𝑌 / 𝑍 ) ) = ( ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) + ( 𝑌 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
28 16 22 27 3eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 + 𝑌 ) / 𝑍 ) = ( ( 𝑋 / 𝑍 ) + ( 𝑌 / 𝑍 ) ) )