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

Metamath Proof Explorer

Theorem subrgdv

Description: A subring always has the same division function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses subrgdv.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
subrgdv.2 ⊢ / = ( /r ‘ 𝑅 )
subrgdv.3 ⊢ 𝑈 = ( Unit ‘ 𝑆 )
subrgdv.4 ⊢ 𝐸 = ( /r ‘ 𝑆 )
Assertion subrgdv ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 𝐸 𝑌 ) )

Proof

Step Hyp Ref Expression
1 subrgdv.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 subrgdv.2 ⊢ / = ( /r ‘ 𝑅 )
3 subrgdv.3 ⊢ 𝑈 = ( Unit ‘ 𝑆 )
4 subrgdv.4 ⊢ 𝐸 = ( /r ‘ 𝑆 )
5 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
6 eqid ⊢ ( invr ‘ 𝑆 ) = ( invr ‘ 𝑆 )
7 1 5 3 6 subrginv ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) = ( ( invr ‘ 𝑆 ) ‘ 𝑌 ) )
8 7 3adant2 ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) = ( ( invr ‘ 𝑆 ) ‘ 𝑌 ) )
9 8 oveq2d ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑆 ) ‘ 𝑌 ) ) )
10 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11 1 10 ressmulr ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
12 11 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
13 12 oveqd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑆 ) ‘ 𝑌 ) ) = ( 𝑋 ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ 𝑌 ) ) )
14 9 13 eqtrd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( 𝑋 ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ 𝑌 ) ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 15 subrgss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
17 16 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
18 simp2 ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ 𝐴 )
19 17 18 sseldd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
20 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
21 1 20 3 subrguss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑈 ⊆ ( Unit ‘ 𝑅 ) )
22 21 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → 𝑈 ⊆ ( Unit ‘ 𝑅 ) )
23 simp3 ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )
24 22 23 sseldd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ ( Unit ‘ 𝑅 ) )
25 15 10 20 5 2 dvrval ⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑌 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
26 19 24 25 syl2anc ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
27 1 subrgbas ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
28 27 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → 𝐴 = ( Base ‘ 𝑆 ) )
29 18 28 eleqtrd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑆 ) )
30 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
31 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
32 30 31 3 6 4 dvrval ⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 𝐸 𝑌 ) = ( 𝑋 ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ 𝑌 ) ) )
33 29 23 32 syl2anc ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 𝐸 𝑌 ) = ( 𝑋 ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ 𝑌 ) ) )
34 14 26 33 3eqtr4d ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 𝐸 𝑌 ) )