Metamath Proof Explorer


Theorem cphsubrglem

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

Ref Expression
Hypotheses cphsubrglem.k โŠข ๐พ = ( Base โ€˜ ๐น )
cphsubrglem.1 โŠข ( ๐œ‘ โ†’ ๐น = ( โ„‚fld โ†พs ๐ด ) )
cphsubrglem.2 โŠข ( ๐œ‘ โ†’ ๐น โˆˆ DivRing )
Assertion cphsubrglem ( ๐œ‘ โ†’ ( ๐น = ( โ„‚fld โ†พs ๐พ ) โˆง ๐พ = ( ๐ด โˆฉ โ„‚ ) โˆง ๐พ โˆˆ ( SubRing โ€˜ โ„‚fld ) ) )

Proof

Step Hyp Ref Expression
1 cphsubrglem.k โŠข ๐พ = ( Base โ€˜ ๐น )
2 cphsubrglem.1 โŠข ( ๐œ‘ โ†’ ๐น = ( โ„‚fld โ†พs ๐ด ) )
3 cphsubrglem.2 โŠข ( ๐œ‘ โ†’ ๐น โˆˆ DivRing )
4 2 fveq2d โŠข ( ๐œ‘ โ†’ ( Base โ€˜ ๐น ) = ( Base โ€˜ ( โ„‚fld โ†พs ๐ด ) ) )
5 drngring โŠข ( ๐น โˆˆ DivRing โ†’ ๐น โˆˆ Ring )
6 3 5 syl โŠข ( ๐œ‘ โ†’ ๐น โˆˆ Ring )
7 2 6 eqeltrrd โŠข ( ๐œ‘ โ†’ ( โ„‚fld โ†พs ๐ด ) โˆˆ Ring )
8 eqid โŠข ( Base โ€˜ ( โ„‚fld โ†พs ๐ด ) ) = ( Base โ€˜ ( โ„‚fld โ†พs ๐ด ) )
9 eqid โŠข ( 0g โ€˜ ( โ„‚fld โ†พs ๐ด ) ) = ( 0g โ€˜ ( โ„‚fld โ†พs ๐ด ) )
10 8 9 ring0cl โŠข ( ( โ„‚fld โ†พs ๐ด ) โˆˆ Ring โ†’ ( 0g โ€˜ ( โ„‚fld โ†พs ๐ด ) ) โˆˆ ( Base โ€˜ ( โ„‚fld โ†พs ๐ด ) ) )
11 reldmress โŠข Rel dom โ†พs
12 eqid โŠข ( โ„‚fld โ†พs ๐ด ) = ( โ„‚fld โ†พs ๐ด )
13 11 12 8 elbasov โŠข ( ( 0g โ€˜ ( โ„‚fld โ†พs ๐ด ) ) โˆˆ ( Base โ€˜ ( โ„‚fld โ†พs ๐ด ) ) โ†’ ( โ„‚fld โˆˆ V โˆง ๐ด โˆˆ V ) )
14 7 10 13 3syl โŠข ( ๐œ‘ โ†’ ( โ„‚fld โˆˆ V โˆง ๐ด โˆˆ V ) )
15 14 simprd โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ V )
16 cnfldbas โŠข โ„‚ = ( Base โ€˜ โ„‚fld )
17 12 16 ressbas โŠข ( ๐ด โˆˆ V โ†’ ( ๐ด โˆฉ โ„‚ ) = ( Base โ€˜ ( โ„‚fld โ†พs ๐ด ) ) )
18 15 17 syl โŠข ( ๐œ‘ โ†’ ( ๐ด โˆฉ โ„‚ ) = ( Base โ€˜ ( โ„‚fld โ†พs ๐ด ) ) )
19 4 18 eqtr4d โŠข ( ๐œ‘ โ†’ ( Base โ€˜ ๐น ) = ( ๐ด โˆฉ โ„‚ ) )
20 1 19 eqtrid โŠข ( ๐œ‘ โ†’ ๐พ = ( ๐ด โˆฉ โ„‚ ) )
21 20 oveq2d โŠข ( ๐œ‘ โ†’ ( โ„‚fld โ†พs ๐พ ) = ( โ„‚fld โ†พs ( ๐ด โˆฉ โ„‚ ) ) )
22 16 ressinbas โŠข ( ๐ด โˆˆ V โ†’ ( โ„‚fld โ†พs ๐ด ) = ( โ„‚fld โ†พs ( ๐ด โˆฉ โ„‚ ) ) )
23 15 22 syl โŠข ( ๐œ‘ โ†’ ( โ„‚fld โ†พs ๐ด ) = ( โ„‚fld โ†พs ( ๐ด โˆฉ โ„‚ ) ) )
24 21 23 eqtr4d โŠข ( ๐œ‘ โ†’ ( โ„‚fld โ†พs ๐พ ) = ( โ„‚fld โ†พs ๐ด ) )
25 2 24 eqtr4d โŠข ( ๐œ‘ โ†’ ๐น = ( โ„‚fld โ†พs ๐พ ) )
26 25 6 eqeltrrd โŠข ( ๐œ‘ โ†’ ( โ„‚fld โ†พs ๐พ ) โˆˆ Ring )
27 cnring โŠข โ„‚fld โˆˆ Ring
28 26 27 jctil โŠข ( ๐œ‘ โ†’ ( โ„‚fld โˆˆ Ring โˆง ( โ„‚fld โ†พs ๐พ ) โˆˆ Ring ) )
29 12 16 ressbasss โŠข ( Base โ€˜ ( โ„‚fld โ†พs ๐ด ) ) โŠ† โ„‚
30 4 29 eqsstrdi โŠข ( ๐œ‘ โ†’ ( Base โ€˜ ๐น ) โŠ† โ„‚ )
31 1 30 eqsstrid โŠข ( ๐œ‘ โ†’ ๐พ โŠ† โ„‚ )
32 eqid โŠข ( 0g โ€˜ ๐น ) = ( 0g โ€˜ ๐น )
33 eqid โŠข ( 1r โ€˜ ๐น ) = ( 1r โ€˜ ๐น )
34 32 33 drngunz โŠข ( ๐น โˆˆ DivRing โ†’ ( 1r โ€˜ ๐น ) โ‰  ( 0g โ€˜ ๐น ) )
35 3 34 syl โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐น ) โ‰  ( 0g โ€˜ ๐น ) )
36 25 fveq2d โŠข ( ๐œ‘ โ†’ ( 0g โ€˜ ๐น ) = ( 0g โ€˜ ( โ„‚fld โ†พs ๐พ ) ) )
37 ringgrp โŠข ( โ„‚fld โˆˆ Ring โ†’ โ„‚fld โˆˆ Grp )
38 27 37 mp1i โŠข ( ๐œ‘ โ†’ โ„‚fld โˆˆ Grp )
39 ringgrp โŠข ( ( โ„‚fld โ†พs ๐พ ) โˆˆ Ring โ†’ ( โ„‚fld โ†พs ๐พ ) โˆˆ Grp )
40 26 39 syl โŠข ( ๐œ‘ โ†’ ( โ„‚fld โ†พs ๐พ ) โˆˆ Grp )
41 16 issubg โŠข ( ๐พ โˆˆ ( SubGrp โ€˜ โ„‚fld ) โ†” ( โ„‚fld โˆˆ Grp โˆง ๐พ โŠ† โ„‚ โˆง ( โ„‚fld โ†พs ๐พ ) โˆˆ Grp ) )
42 38 31 40 41 syl3anbrc โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ ( SubGrp โ€˜ โ„‚fld ) )
43 eqid โŠข ( โ„‚fld โ†พs ๐พ ) = ( โ„‚fld โ†พs ๐พ )
44 cnfld0 โŠข 0 = ( 0g โ€˜ โ„‚fld )
45 43 44 subg0 โŠข ( ๐พ โˆˆ ( SubGrp โ€˜ โ„‚fld ) โ†’ 0 = ( 0g โ€˜ ( โ„‚fld โ†พs ๐พ ) ) )
46 42 45 syl โŠข ( ๐œ‘ โ†’ 0 = ( 0g โ€˜ ( โ„‚fld โ†พs ๐พ ) ) )
47 36 46 eqtr4d โŠข ( ๐œ‘ โ†’ ( 0g โ€˜ ๐น ) = 0 )
48 35 47 neeqtrd โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐น ) โ‰  0 )
49 48 neneqd โŠข ( ๐œ‘ โ†’ ยฌ ( 1r โ€˜ ๐น ) = 0 )
50 1 33 ringidcl โŠข ( ๐น โˆˆ Ring โ†’ ( 1r โ€˜ ๐น ) โˆˆ ๐พ )
51 6 50 syl โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐น ) โˆˆ ๐พ )
52 31 51 sseldd โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐น ) โˆˆ โ„‚ )
53 52 sqvald โŠข ( ๐œ‘ โ†’ ( ( 1r โ€˜ ๐น ) โ†‘ 2 ) = ( ( 1r โ€˜ ๐น ) ยท ( 1r โ€˜ ๐น ) ) )
54 25 fveq2d โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐น ) = ( 1r โ€˜ ( โ„‚fld โ†พs ๐พ ) ) )
55 54 oveq1d โŠข ( ๐œ‘ โ†’ ( ( 1r โ€˜ ๐น ) ยท ( 1r โ€˜ ๐น ) ) = ( ( 1r โ€˜ ( โ„‚fld โ†พs ๐พ ) ) ยท ( 1r โ€˜ ๐น ) ) )
56 25 fveq2d โŠข ( ๐œ‘ โ†’ ( Base โ€˜ ๐น ) = ( Base โ€˜ ( โ„‚fld โ†พs ๐พ ) ) )
57 1 56 eqtrid โŠข ( ๐œ‘ โ†’ ๐พ = ( Base โ€˜ ( โ„‚fld โ†พs ๐พ ) ) )
58 51 57 eleqtrd โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐น ) โˆˆ ( Base โ€˜ ( โ„‚fld โ†พs ๐พ ) ) )
59 eqid โŠข ( Base โ€˜ ( โ„‚fld โ†พs ๐พ ) ) = ( Base โ€˜ ( โ„‚fld โ†พs ๐พ ) )
60 1 fvexi โŠข ๐พ โˆˆ V
61 cnfldmul โŠข ยท = ( .r โ€˜ โ„‚fld )
62 43 61 ressmulr โŠข ( ๐พ โˆˆ V โ†’ ยท = ( .r โ€˜ ( โ„‚fld โ†พs ๐พ ) ) )
63 60 62 ax-mp โŠข ยท = ( .r โ€˜ ( โ„‚fld โ†พs ๐พ ) )
64 eqid โŠข ( 1r โ€˜ ( โ„‚fld โ†พs ๐พ ) ) = ( 1r โ€˜ ( โ„‚fld โ†พs ๐พ ) )
65 59 63 64 ringlidm โŠข ( ( ( โ„‚fld โ†พs ๐พ ) โˆˆ Ring โˆง ( 1r โ€˜ ๐น ) โˆˆ ( Base โ€˜ ( โ„‚fld โ†พs ๐พ ) ) ) โ†’ ( ( 1r โ€˜ ( โ„‚fld โ†พs ๐พ ) ) ยท ( 1r โ€˜ ๐น ) ) = ( 1r โ€˜ ๐น ) )
66 26 58 65 syl2anc โŠข ( ๐œ‘ โ†’ ( ( 1r โ€˜ ( โ„‚fld โ†พs ๐พ ) ) ยท ( 1r โ€˜ ๐น ) ) = ( 1r โ€˜ ๐น ) )
67 53 55 66 3eqtrd โŠข ( ๐œ‘ โ†’ ( ( 1r โ€˜ ๐น ) โ†‘ 2 ) = ( 1r โ€˜ ๐น ) )
68 sq01 โŠข ( ( 1r โ€˜ ๐น ) โˆˆ โ„‚ โ†’ ( ( ( 1r โ€˜ ๐น ) โ†‘ 2 ) = ( 1r โ€˜ ๐น ) โ†” ( ( 1r โ€˜ ๐น ) = 0 โˆจ ( 1r โ€˜ ๐น ) = 1 ) ) )
69 52 68 syl โŠข ( ๐œ‘ โ†’ ( ( ( 1r โ€˜ ๐น ) โ†‘ 2 ) = ( 1r โ€˜ ๐น ) โ†” ( ( 1r โ€˜ ๐น ) = 0 โˆจ ( 1r โ€˜ ๐น ) = 1 ) ) )
70 67 69 mpbid โŠข ( ๐œ‘ โ†’ ( ( 1r โ€˜ ๐น ) = 0 โˆจ ( 1r โ€˜ ๐น ) = 1 ) )
71 70 ord โŠข ( ๐œ‘ โ†’ ( ยฌ ( 1r โ€˜ ๐น ) = 0 โ†’ ( 1r โ€˜ ๐น ) = 1 ) )
72 49 71 mpd โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐น ) = 1 )
73 72 51 eqeltrrd โŠข ( ๐œ‘ โ†’ 1 โˆˆ ๐พ )
74 31 73 jca โŠข ( ๐œ‘ โ†’ ( ๐พ โŠ† โ„‚ โˆง 1 โˆˆ ๐พ ) )
75 cnfld1 โŠข 1 = ( 1r โ€˜ โ„‚fld )
76 16 75 issubrg โŠข ( ๐พ โˆˆ ( SubRing โ€˜ โ„‚fld ) โ†” ( ( โ„‚fld โˆˆ Ring โˆง ( โ„‚fld โ†พs ๐พ ) โˆˆ Ring ) โˆง ( ๐พ โŠ† โ„‚ โˆง 1 โˆˆ ๐พ ) ) )
77 28 74 76 sylanbrc โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ ( SubRing โ€˜ โ„‚fld ) )
78 25 20 77 3jca โŠข ( ๐œ‘ โ†’ ( ๐น = ( โ„‚fld โ†พs ๐พ ) โˆง ๐พ = ( ๐ด โˆฉ โ„‚ ) โˆง ๐พ โˆˆ ( SubRing โ€˜ โ„‚fld ) ) )