Metamath Proof Explorer

Theorem dvrass

Description: An associative law for division. ( divass analog.) (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses dvrass.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvrass.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dvrass.d ⊢ / = ( /r ‘ 𝑅 )
dvrass.t ⊢ · = ( .r ‘ 𝑅 )
Assertion dvrass ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) / 𝑍 ) = ( 𝑋 · ( 𝑌 / 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 dvrass.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dvrass.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 dvrass.d ⊢ / = ( /r ‘ 𝑅 )
4 dvrass.t ⊢ · = ( .r ‘ 𝑅 )
5 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑅 ∈ Ring )
6 simpr1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
7 simpr2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑌 ∈ 𝐵 )
8 simpr3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑍 ∈ 𝑈 )
9 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
10 2 9 1 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 )
11 5 8 10 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 )
12 1 4 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 ) ) → ( ( 𝑋 · 𝑌 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = ( 𝑋 · ( 𝑌 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
13 5 6 7 11 12 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = ( 𝑋 · ( 𝑌 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
14 1 4 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
15 14 3adant3r3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
16 1 4 2 9 3 dvrval ⊢ ( ( ( 𝑋 · 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) / 𝑍 ) = ( ( 𝑋 · 𝑌 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
17 15 8 16 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) / 𝑍 ) = ( ( 𝑋 · 𝑌 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
18 1 4 2 9 3 dvrval ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑌 / 𝑍 ) = ( 𝑌 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
19 7 8 18 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑌 / 𝑍 ) = ( 𝑌 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) )
20 19 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑋 · ( 𝑌 / 𝑍 ) ) = ( 𝑋 · ( 𝑌 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) ) )
21 13 17 20 3eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) / 𝑍 ) = ( 𝑋 · ( 𝑌 / 𝑍 ) ) )