Metamath Proof Explorer


Theorem cphreccllem

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

Ref Expression
Hypotheses cphsubrglem.k K=BaseF
cphsubrglem.1 φF=fld𝑠A
cphsubrglem.2 φFDivRing
Assertion cphreccllem φXKX01XK

Proof

Step Hyp Ref Expression
1 cphsubrglem.k K=BaseF
2 cphsubrglem.1 φF=fld𝑠A
3 cphsubrglem.2 φFDivRing
4 1 2 3 cphsubrglem φF=fld𝑠KK=AKSubRingfld
5 4 simp3d φKSubRingfld
6 5 3ad2ant1 φXKX0KSubRingfld
7 cnfldbas =Basefld
8 7 subrgss KSubRingfldK
9 6 8 syl φXKX0K
10 simp2 φXKX0XK
11 9 10 sseldd φXKX0X
12 simp3 φXKX0X0
13 cnfldinv XX0invrfldX=1X
14 11 12 13 syl2anc φXKX0invrfldX=1X
15 eqid fld𝑠K=fld𝑠K
16 cnfld0 0=0fld
17 15 16 subrg0 KSubRingfld0=0fld𝑠K
18 6 17 syl φXKX00=0fld𝑠K
19 4 simp1d φF=fld𝑠K
20 19 3ad2ant1 φXKX0F=fld𝑠K
21 20 fveq2d φXKX00F=0fld𝑠K
22 18 21 eqtr4d φXKX00=0F
23 12 22 neeqtrd φXKX0X0F
24 eldifsn XK0FXKX0F
25 10 23 24 sylanbrc φXKX0XK0F
26 3 3ad2ant1 φXKX0FDivRing
27 eqid UnitF=UnitF
28 eqid 0F=0F
29 1 27 28 isdrng FDivRingFRingUnitF=K0F
30 29 simprbi FDivRingUnitF=K0F
31 26 30 syl φXKX0UnitF=K0F
32 20 fveq2d φXKX0UnitF=Unitfld𝑠K
33 31 32 eqtr3d φXKX0K0F=Unitfld𝑠K
34 25 33 eleqtrd φXKX0XUnitfld𝑠K
35 eqid Unitfld=Unitfld
36 eqid Unitfld𝑠K=Unitfld𝑠K
37 eqid invrfld=invrfld
38 15 35 36 37 subrgunit KSubRingfldXUnitfld𝑠KXUnitfldXKinvrfldXK
39 6 38 syl φXKX0XUnitfld𝑠KXUnitfldXKinvrfldXK
40 34 39 mpbid φXKX0XUnitfldXKinvrfldXK
41 40 simp3d φXKX0invrfldXK
42 14 41 eqeltrrd φXKX01XK