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 = ( R |`s A )
subrgdv.2 
|- ./ = ( /r ` R )
subrgdv.3 
|- U = ( Unit ` S )
subrgdv.4 
|- E = ( /r ` S )
Assertion subrgdv 
|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( X ./ Y ) = ( X E Y ) )

Proof

Step Hyp Ref Expression
1 subrgdv.1 
 |-  S = ( R |`s A )
2 subrgdv.2 
 |-  ./ = ( /r ` R )
3 subrgdv.3 
 |-  U = ( Unit ` S )
4 subrgdv.4 
 |-  E = ( /r ` S )
5 eqid 
 |-  ( invr ` R ) = ( invr ` R )
6 eqid 
 |-  ( invr ` S ) = ( invr ` S )
7 1 5 3 6 subrginv 
 |-  ( ( A e. ( SubRing ` R ) /\ Y e. U ) -> ( ( invr ` R ) ` Y ) = ( ( invr ` S ) ` Y ) )
8 7 3adant2 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( ( invr ` R ) ` Y ) = ( ( invr ` S ) ` Y ) )
9 8 oveq2d 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) = ( X ( .r ` R ) ( ( invr ` S ) ` Y ) ) )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 1 10 ressmulr 
 |-  ( A e. ( SubRing ` R ) -> ( .r ` R ) = ( .r ` S ) )
12 11 3ad2ant1 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( .r ` R ) = ( .r ` S ) )
13 12 oveqd 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( X ( .r ` R ) ( ( invr ` S ) ` Y ) ) = ( X ( .r ` S ) ( ( invr ` S ) ` Y ) ) )
14 9 13 eqtrd 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) = ( X ( .r ` S ) ( ( invr ` S ) ` Y ) ) )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 15 subrgss 
 |-  ( A e. ( SubRing ` R ) -> A C_ ( Base ` R ) )
17 16 3ad2ant1 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> A C_ ( Base ` R ) )
18 simp2 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> X e. A )
19 17 18 sseldd 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> X e. ( Base ` R ) )
20 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
21 1 20 3 subrguss 
 |-  ( A e. ( SubRing ` R ) -> U C_ ( Unit ` R ) )
22 21 3ad2ant1 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> U C_ ( Unit ` R ) )
23 simp3 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> Y e. U )
24 22 23 sseldd 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> Y e. ( Unit ` R ) )
25 15 10 20 5 2 dvrval 
 |-  ( ( X e. ( Base ` R ) /\ Y e. ( Unit ` R ) ) -> ( X ./ Y ) = ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) )
26 19 24 25 syl2anc 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( X ./ Y ) = ( X ( .r ` R ) ( ( invr ` R ) ` Y ) ) )
27 1 subrgbas 
 |-  ( A e. ( SubRing ` R ) -> A = ( Base ` S ) )
28 27 3ad2ant1 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> A = ( Base ` S ) )
29 18 28 eleqtrd 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> X e. ( Base ` S ) )
30 eqid 
 |-  ( Base ` S ) = ( Base ` S )
31 eqid 
 |-  ( .r ` S ) = ( .r ` S )
32 30 31 3 6 4 dvrval 
 |-  ( ( X e. ( Base ` S ) /\ Y e. U ) -> ( X E Y ) = ( X ( .r ` S ) ( ( invr ` S ) ` Y ) ) )
33 29 23 32 syl2anc 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( X E Y ) = ( X ( .r ` S ) ( ( invr ` S ) ` Y ) ) )
34 14 26 33 3eqtr4d 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( X ./ Y ) = ( X E Y ) )