Metamath Proof Explorer

Theorem cphreccllem

Description: Lemma for cphreccl . (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses cphsubrglem.k 
|- K = ( Base ` F )
cphsubrglem.1 
|- ( ph -> F = ( CCfld |`s A ) )
cphsubrglem.2 
|- ( ph -> F e. DivRing )
Assertion cphreccllem 
|- ( ( ph /\ X e. K /\ X =/= 0 ) -> ( 1 / X ) e. K )

Proof

Step Hyp Ref Expression
1 cphsubrglem.k 
 |-  K = ( Base ` F )
2 cphsubrglem.1 
 |-  ( ph -> F = ( CCfld |`s A ) )
3 cphsubrglem.2 
 |-  ( ph -> F e. DivRing )
4 1 2 3 cphsubrglem 
 |-  ( ph -> ( F = ( CCfld |`s K ) /\ K = ( A i^i CC ) /\ K e. ( SubRing ` CCfld ) ) )
5 4 simp3d 
 |-  ( ph -> K e. ( SubRing ` CCfld ) )
6 5 3ad2ant1 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> K e. ( SubRing ` CCfld ) )
7 cnfldbas 
 |-  CC = ( Base ` CCfld )
8 7 subrgss 
 |-  ( K e. ( SubRing ` CCfld ) -> K C_ CC )
9 6 8 syl 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> K C_ CC )
10 simp2 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> X e. K )
11 9 10 sseldd 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> X e. CC )
12 simp3 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> X =/= 0 )
13 cnfldinv 
 |-  ( ( X e. CC /\ X =/= 0 ) -> ( ( invr ` CCfld ) ` X ) = ( 1 / X ) )
14 11 12 13 syl2anc 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> ( ( invr ` CCfld ) ` X ) = ( 1 / X ) )
15 eqid 
 |-  ( CCfld |`s K ) = ( CCfld |`s K )
16 cnfld0 
 |-  0 = ( 0g ` CCfld )
17 15 16 subrg0 
 |-  ( K e. ( SubRing ` CCfld ) -> 0 = ( 0g ` ( CCfld |`s K ) ) )
18 6 17 syl 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> 0 = ( 0g ` ( CCfld |`s K ) ) )
19 4 simp1d 
 |-  ( ph -> F = ( CCfld |`s K ) )
20 19 3ad2ant1 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> F = ( CCfld |`s K ) )
21 20 fveq2d 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> ( 0g ` F ) = ( 0g ` ( CCfld |`s K ) ) )
22 18 21 eqtr4d 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> 0 = ( 0g ` F ) )
23 12 22 neeqtrd 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> X =/= ( 0g ` F ) )
24 eldifsn 
 |-  ( X e. ( K \ { ( 0g ` F ) } ) <-> ( X e. K /\ X =/= ( 0g ` F ) ) )
25 10 23 24 sylanbrc 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> X e. ( K \ { ( 0g ` F ) } ) )
26 3 3ad2ant1 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> F e. DivRing )
27 eqid 
 |-  ( Unit ` F ) = ( Unit ` F )
28 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
29 1 27 28 isdrng 
 |-  ( F e. DivRing <-> ( F e. Ring /\ ( Unit ` F ) = ( K \ { ( 0g ` F ) } ) ) )
30 29 simprbi 
 |-  ( F e. DivRing -> ( Unit ` F ) = ( K \ { ( 0g ` F ) } ) )
31 26 30 syl 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> ( Unit ` F ) = ( K \ { ( 0g ` F ) } ) )
32 20 fveq2d 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> ( Unit ` F ) = ( Unit ` ( CCfld |`s K ) ) )
33 31 32 eqtr3d 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> ( K \ { ( 0g ` F ) } ) = ( Unit ` ( CCfld |`s K ) ) )
34 25 33 eleqtrd 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> X e. ( Unit ` ( CCfld |`s K ) ) )
35 eqid 
 |-  ( Unit ` CCfld ) = ( Unit ` CCfld )
36 eqid 
 |-  ( Unit ` ( CCfld |`s K ) ) = ( Unit ` ( CCfld |`s K ) )
37 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
38 15 35 36 37 subrgunit 
 |-  ( K e. ( SubRing ` CCfld ) -> ( X e. ( Unit ` ( CCfld |`s K ) ) <-> ( X e. ( Unit ` CCfld ) /\ X e. K /\ ( ( invr ` CCfld ) ` X ) e. K ) ) )
39 6 38 syl 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> ( X e. ( Unit ` ( CCfld |`s K ) ) <-> ( X e. ( Unit ` CCfld ) /\ X e. K /\ ( ( invr ` CCfld ) ` X ) e. K ) ) )
40 34 39 mpbid 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> ( X e. ( Unit ` CCfld ) /\ X e. K /\ ( ( invr ` CCfld ) ` X ) e. K ) )
41 40 simp3d 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> ( ( invr ` CCfld ) ` X ) e. K )
42 14 41 eqeltrrd 
 |-  ( ( ph /\ X e. K /\ X =/= 0 ) -> ( 1 / X ) e. K )