Metamath Proof Explorer

Theorem cnsubdrglem

Description: Lemma for resubdrg and friends. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses cnsubglem.1 
|- ( x e. A -> x e. CC )
cnsubglem.2 
|- ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )
cnsubglem.3 
|- ( x e. A -> -u x e. A )
cnsubrglem.4 
|- 1 e. A
cnsubrglem.5 
|- ( ( x e. A /\ y e. A ) -> ( x x. y ) e. A )
cnsubrglem.6 
|- ( ( x e. A /\ x =/= 0 ) -> ( 1 / x ) e. A )
Assertion cnsubdrglem 
|- ( A e. ( SubRing ` CCfld ) /\ ( CCfld |`s A ) e. DivRing )

Proof

Step Hyp Ref Expression
1 cnsubglem.1 
 |-  ( x e. A -> x e. CC )
2 cnsubglem.2 
 |-  ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )
3 cnsubglem.3 
 |-  ( x e. A -> -u x e. A )
4 cnsubrglem.4 
 |-  1 e. A
5 cnsubrglem.5 
 |-  ( ( x e. A /\ y e. A ) -> ( x x. y ) e. A )
6 cnsubrglem.6 
 |-  ( ( x e. A /\ x =/= 0 ) -> ( 1 / x ) e. A )
7 1 2 3 4 5 cnsubrglem 
 |-  A e. ( SubRing ` CCfld )
8 cndrng 
 |-  CCfld e. DivRing
9 eqid 
 |-  ( CCfld |`s A ) = ( CCfld |`s A )
10 cnfld0 
 |-  0 = ( 0g ` CCfld )
11 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
12 9 10 11 issubdrg 
 |-  ( ( CCfld e. DivRing /\ A e. ( SubRing ` CCfld ) ) -> ( ( CCfld |`s A ) e. DivRing <-> A. x e. ( A \ { 0 } ) ( ( invr ` CCfld ) ` x ) e. A ) )
13 8 7 12 mp2an 
 |-  ( ( CCfld |`s A ) e. DivRing <-> A. x e. ( A \ { 0 } ) ( ( invr ` CCfld ) ` x ) e. A )
14 cnring 
 |-  CCfld e. Ring
15 1 ssriv 
 |-  A C_ CC
16 ssdif 
 |-  ( A C_ CC -> ( A \ { 0 } ) C_ ( CC \ { 0 } ) )
17 15 16 ax-mp 
 |-  ( A \ { 0 } ) C_ ( CC \ { 0 } )
18 17 sseli 
 |-  ( x e. ( A \ { 0 } ) -> x e. ( CC \ { 0 } ) )
19 cnfldbas 
 |-  CC = ( Base ` CCfld )
20 19 10 8 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
21 cnflddiv 
 |-  / = ( /r ` CCfld )
22 cnfld1 
 |-  1 = ( 1r ` CCfld )
23 19 20 21 22 11 ringinvdv 
 |-  ( ( CCfld e. Ring /\ x e. ( CC \ { 0 } ) ) -> ( ( invr ` CCfld ) ` x ) = ( 1 / x ) )
24 14 18 23 sylancr 
 |-  ( x e. ( A \ { 0 } ) -> ( ( invr ` CCfld ) ` x ) = ( 1 / x ) )
25 eldifsn 
 |-  ( x e. ( A \ { 0 } ) <-> ( x e. A /\ x =/= 0 ) )
26 25 6 sylbi 
 |-  ( x e. ( A \ { 0 } ) -> ( 1 / x ) e. A )
27 24 26 eqeltrd 
 |-  ( x e. ( A \ { 0 } ) -> ( ( invr ` CCfld ) ` x ) e. A )
28 13 27 mprgbir 
 |-  ( CCfld |`s A ) e. DivRing
29 7 28 pm3.2i 
 |-  ( A e. ( SubRing ` CCfld ) /\ ( CCfld |`s A ) e. DivRing )