Metamath Proof Explorer

Theorem fldgenfldext

Description: A subfield F extended with a set A forms a field extension. (Contributed by Thierry Arnoux, 22-Jun-2025)

Ref Expression
Hypotheses fldgenfldext.b 
|- B = ( Base ` E )
fldgenfldext.k 
|- K = ( E |`s F )
fldgenfldext.l 
|- L = ( E |`s ( E fldGen ( F u. A ) ) )
fldgenfldext.e 
|- ( ph -> E e. Field )
fldgenfldext.f 
|- ( ph -> F e. ( SubDRing ` E ) )
fldgenfldext.1 
|- ( ph -> A C_ B )
Assertion fldgenfldext 
|- ( ph -> L /FldExt K )

Proof

Step Hyp Ref Expression
1 fldgenfldext.b 
 |-  B = ( Base ` E )
2 fldgenfldext.k 
 |-  K = ( E |`s F )
3 fldgenfldext.l 
 |-  L = ( E |`s ( E fldGen ( F u. A ) ) )
4 fldgenfldext.e 
 |-  ( ph -> E e. Field )
5 fldgenfldext.f 
 |-  ( ph -> F e. ( SubDRing ` E ) )
6 fldgenfldext.1 
 |-  ( ph -> A C_ B )
7 1 sdrgss 
 |-  ( F e. ( SubDRing ` E ) -> F C_ B )
8 5 7 syl 
 |-  ( ph -> F C_ B )
9 8 6 unssd 
 |-  ( ph -> ( F u. A ) C_ B )
10 1 4 9 fldgenfld 
 |-  ( ph -> ( E |`s ( E fldGen ( F u. A ) ) ) e. Field )
11 3 10 eqeltrid 
 |-  ( ph -> L e. Field )
12 fldsdrgfld 
 |-  ( ( E e. Field /\ F e. ( SubDRing ` E ) ) -> ( E |`s F ) e. Field )
13 4 5 12 syl2anc 
 |-  ( ph -> ( E |`s F ) e. Field )
14 2 13 eqeltrid 
 |-  ( ph -> K e. Field )
15 3 oveq1i 
 |-  ( L |`s F ) = ( ( E |`s ( E fldGen ( F u. A ) ) ) |`s F )
16 ovexd 
 |-  ( ph -> ( E fldGen ( F u. A ) ) e. _V )
17 ressress 
 |-  ( ( ( E fldGen ( F u. A ) ) e. _V /\ F e. ( SubDRing ` E ) ) -> ( ( E |`s ( E fldGen ( F u. A ) ) ) |`s F ) = ( E |`s ( ( E fldGen ( F u. A ) ) i^i F ) ) )
18 16 5 17 syl2anc 
 |-  ( ph -> ( ( E |`s ( E fldGen ( F u. A ) ) ) |`s F ) = ( E |`s ( ( E fldGen ( F u. A ) ) i^i F ) ) )
19 15 18 eqtrid 
 |-  ( ph -> ( L |`s F ) = ( E |`s ( ( E fldGen ( F u. A ) ) i^i F ) ) )
20 4 flddrngd 
 |-  ( ph -> E e. DivRing )
21 1 20 9 fldgenssid 
 |-  ( ph -> ( F u. A ) C_ ( E fldGen ( F u. A ) ) )
22 21 unssad 
 |-  ( ph -> F C_ ( E fldGen ( F u. A ) ) )
23 sseqin2 
 |-  ( F C_ ( E fldGen ( F u. A ) ) <-> ( ( E fldGen ( F u. A ) ) i^i F ) = F )
24 22 23 sylib 
 |-  ( ph -> ( ( E fldGen ( F u. A ) ) i^i F ) = F )
25 24 oveq2d 
 |-  ( ph -> ( E |`s ( ( E fldGen ( F u. A ) ) i^i F ) ) = ( E |`s F ) )
26 19 25 eqtrd 
 |-  ( ph -> ( L |`s F ) = ( E |`s F ) )
27 2 1 ressbas2 
 |-  ( F C_ B -> F = ( Base ` K ) )
28 8 27 syl 
 |-  ( ph -> F = ( Base ` K ) )
29 28 oveq2d 
 |-  ( ph -> ( L |`s F ) = ( L |`s ( Base ` K ) ) )
30 26 29 eqtr3d 
 |-  ( ph -> ( E |`s F ) = ( L |`s ( Base ` K ) ) )
31 2 30 eqtrid 
 |-  ( ph -> K = ( L |`s ( Base ` K ) ) )
32 11 fldcrngd 
 |-  ( ph -> L e. CRing )
33 32 crngringd 
 |-  ( ph -> L e. Ring )
34 14 fldcrngd 
 |-  ( ph -> K e. CRing )
35 34 crngringd 
 |-  ( ph -> K e. Ring )
36 2 35 eqeltrrid 
 |-  ( ph -> ( E |`s F ) e. Ring )
37 26 36 eqeltrd 
 |-  ( ph -> ( L |`s F ) e. Ring )
38 1 20 9 fldgenssv 
 |-  ( ph -> ( E fldGen ( F u. A ) ) C_ B )
39 3 1 ressbas2 
 |-  ( ( E fldGen ( F u. A ) ) C_ B -> ( E fldGen ( F u. A ) ) = ( Base ` L ) )
40 38 39 syl 
 |-  ( ph -> ( E fldGen ( F u. A ) ) = ( Base ` L ) )
41 22 40 sseqtrd 
 |-  ( ph -> F C_ ( Base ` L ) )
42 20 drngringd 
 |-  ( ph -> E e. Ring )
43 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
44 eqid 
 |-  ( 1r ` E ) = ( 1r ` E )
45 44 subrg1cl 
 |-  ( F e. ( SubRing ` E ) -> ( 1r ` E ) e. F )
46 5 43 45 3syl 
 |-  ( ph -> ( 1r ` E ) e. F )
47 22 46 sseldd 
 |-  ( ph -> ( 1r ` E ) e. ( E fldGen ( F u. A ) ) )
48 3 1 44 ress1r 
 |-  ( ( E e. Ring /\ ( 1r ` E ) e. ( E fldGen ( F u. A ) ) /\ ( E fldGen ( F u. A ) ) C_ B ) -> ( 1r ` E ) = ( 1r ` L ) )
49 42 47 38 48 syl3anc 
 |-  ( ph -> ( 1r ` E ) = ( 1r ` L ) )
50 49 46 eqeltrrd 
 |-  ( ph -> ( 1r ` L ) e. F )
51 41 50 jca 
 |-  ( ph -> ( F C_ ( Base ` L ) /\ ( 1r ` L ) e. F ) )
52 eqid 
 |-  ( Base ` L ) = ( Base ` L )
53 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
54 52 53 issubrg 
 |-  ( F e. ( SubRing ` L ) <-> ( ( L e. Ring /\ ( L |`s F ) e. Ring ) /\ ( F C_ ( Base ` L ) /\ ( 1r ` L ) e. F ) ) )
55 33 37 51 54 syl21anbrc 
 |-  ( ph -> F e. ( SubRing ` L ) )
56 28 55 eqeltrrd 
 |-  ( ph -> ( Base ` K ) e. ( SubRing ` L ) )
57 brfldext 
 |-  ( ( L e. Field /\ K e. Field ) -> ( L /FldExt K <-> ( K = ( L |`s ( Base ` K ) ) /\ ( Base ` K ) e. ( SubRing ` L ) ) ) )
58 57 biimpar 
 |-  ( ( ( L e. Field /\ K e. Field ) /\ ( K = ( L |`s ( Base ` K ) ) /\ ( Base ` K ) e. ( SubRing ` L ) ) ) -> L /FldExt K )
59 11 14 31 56 58 syl22anc 
 |-  ( ph -> L /FldExt K )