Metamath Proof Explorer


Theorem cphsubrglem

Description: Lemma for cphsubrg . (Contributed by Mario Carneiro, 9-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 cphsubrglem.k K=BaseF
2 cphsubrglem.1 φF=fld𝑠A
3 cphsubrglem.2 φFDivRing
4 2 fveq2d φBaseF=Basefld𝑠A
5 drngring FDivRingFRing
6 3 5 syl φFRing
7 2 6 eqeltrrd φfld𝑠ARing
8 eqid Basefld𝑠A=Basefld𝑠A
9 eqid 0fld𝑠A=0fld𝑠A
10 8 9 ring0cl fld𝑠ARing0fld𝑠ABasefld𝑠A
11 reldmress Reldom𝑠
12 eqid fld𝑠A=fld𝑠A
13 11 12 8 elbasov 0fld𝑠ABasefld𝑠AfldVAV
14 7 10 13 3syl φfldVAV
15 14 simprd φAV
16 cnfldbas =Basefld
17 12 16 ressbas AVA=Basefld𝑠A
18 15 17 syl φA=Basefld𝑠A
19 4 18 eqtr4d φBaseF=A
20 1 19 eqtrid φK=A
21 20 oveq2d φfld𝑠K=fld𝑠A
22 16 ressinbas AVfld𝑠A=fld𝑠A
23 15 22 syl φfld𝑠A=fld𝑠A
24 21 23 eqtr4d φfld𝑠K=fld𝑠A
25 2 24 eqtr4d φF=fld𝑠K
26 25 6 eqeltrrd φfld𝑠KRing
27 cnring fldRing
28 26 27 jctil φfldRingfld𝑠KRing
29 12 16 ressbasss Basefld𝑠A
30 4 29 eqsstrdi φBaseF
31 1 30 eqsstrid φK
32 eqid 0F=0F
33 eqid 1F=1F
34 32 33 drngunz FDivRing1F0F
35 3 34 syl φ1F0F
36 25 fveq2d φ0F=0fld𝑠K
37 ringgrp fldRingfldGrp
38 27 37 mp1i φfldGrp
39 ringgrp fld𝑠KRingfld𝑠KGrp
40 26 39 syl φfld𝑠KGrp
41 16 issubg KSubGrpfldfldGrpKfld𝑠KGrp
42 38 31 40 41 syl3anbrc φKSubGrpfld
43 eqid fld𝑠K=fld𝑠K
44 cnfld0 0=0fld
45 43 44 subg0 KSubGrpfld0=0fld𝑠K
46 42 45 syl φ0=0fld𝑠K
47 36 46 eqtr4d φ0F=0
48 35 47 neeqtrd φ1F0
49 48 neneqd φ¬1F=0
50 1 33 ringidcl FRing1FK
51 6 50 syl φ1FK
52 31 51 sseldd φ1F
53 52 sqvald φ1F2=1F1F
54 25 fveq2d φ1F=1fld𝑠K
55 54 oveq1d φ1F1F=1fld𝑠K1F
56 25 fveq2d φBaseF=Basefld𝑠K
57 1 56 eqtrid φK=Basefld𝑠K
58 51 57 eleqtrd φ1FBasefld𝑠K
59 eqid Basefld𝑠K=Basefld𝑠K
60 1 fvexi KV
61 cnfldmul ×=fld
62 43 61 ressmulr KV×=fld𝑠K
63 60 62 ax-mp ×=fld𝑠K
64 eqid 1fld𝑠K=1fld𝑠K
65 59 63 64 ringlidm fld𝑠KRing1FBasefld𝑠K1fld𝑠K1F=1F
66 26 58 65 syl2anc φ1fld𝑠K1F=1F
67 53 55 66 3eqtrd φ1F2=1F
68 sq01 1F1F2=1F1F=01F=1
69 52 68 syl φ1F2=1F1F=01F=1
70 67 69 mpbid φ1F=01F=1
71 70 ord φ¬1F=01F=1
72 49 71 mpd φ1F=1
73 72 51 eqeltrrd φ1K
74 31 73 jca φK1K
75 cnfld1 1=1fld
76 16 75 issubrg KSubRingfldfldRingfld𝑠KRingK1K
77 28 74 76 sylanbrc φKSubRingfld
78 25 20 77 3jca φF=fld𝑠KK=AKSubRingfld