Metamath Proof Explorer

Theorem fldextrspunfld

Description: The ring generated by the union of two field extensions is a field. Part of the proof of Proposition 5, Chapter 5, of BourbakiAlg2 p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses fldextrspunfld.k 
|- K = ( L |`s F )
fldextrspunfld.i 
|- I = ( L |`s G )
fldextrspunfld.j 
|- J = ( L |`s H )
fldextrspunfld.2 
|- ( ph -> L e. Field )
fldextrspunfld.3 
|- ( ph -> F e. ( SubDRing ` I ) )
fldextrspunfld.4 
|- ( ph -> F e. ( SubDRing ` J ) )
fldextrspunfld.5 
|- ( ph -> G e. ( SubDRing ` L ) )
fldextrspunfld.6 
|- ( ph -> H e. ( SubDRing ` L ) )
fldextrspunfld.7 
|- ( ph -> ( J [:] K ) e. NN0 )
fldextrspunfld.n 
|- N = ( RingSpan ` L )
fldextrspunfld.c 
|- C = ( N ` ( G u. H ) )
fldextrspunfld.e 
|- E = ( L |`s C )
Assertion fldextrspunfld 
|- ( ph -> E e. Field )

Proof

Step Hyp Ref Expression
1 fldextrspunfld.k 
 |-  K = ( L |`s F )
2 fldextrspunfld.i 
 |-  I = ( L |`s G )
3 fldextrspunfld.j 
 |-  J = ( L |`s H )
4 fldextrspunfld.2 
 |-  ( ph -> L e. Field )
5 fldextrspunfld.3 
 |-  ( ph -> F e. ( SubDRing ` I ) )
6 fldextrspunfld.4 
 |-  ( ph -> F e. ( SubDRing ` J ) )
7 fldextrspunfld.5 
 |-  ( ph -> G e. ( SubDRing ` L ) )
8 fldextrspunfld.6 
 |-  ( ph -> H e. ( SubDRing ` L ) )
9 fldextrspunfld.7 
 |-  ( ph -> ( J [:] K ) e. NN0 )
10 fldextrspunfld.n 
 |-  N = ( RingSpan ` L )
11 fldextrspunfld.c 
 |-  C = ( N ` ( G u. H ) )
12 fldextrspunfld.e 
 |-  E = ( L |`s C )
13 eqid 
 |-  ( Scalar ` ( ( subringAlg ` E ) ` G ) ) = ( Scalar ` ( ( subringAlg ` E ) ` G ) )
14 4 flddrngd 
 |-  ( ph -> L e. DivRing )
15 14 drngringd 
 |-  ( ph -> L e. Ring )
16 eqidd 
 |-  ( ph -> ( Base ` L ) = ( Base ` L ) )
17 eqid 
 |-  ( Base ` L ) = ( Base ` L )
18 17 sdrgss 
 |-  ( G e. ( SubDRing ` L ) -> G C_ ( Base ` L ) )
19 7 18 syl 
 |-  ( ph -> G C_ ( Base ` L ) )
20 17 sdrgss 
 |-  ( H e. ( SubDRing ` L ) -> H C_ ( Base ` L ) )
21 8 20 syl 
 |-  ( ph -> H C_ ( Base ` L ) )
22 19 21 unssd 
 |-  ( ph -> ( G u. H ) C_ ( Base ` L ) )
23 10 a1i 
 |-  ( ph -> N = ( RingSpan ` L ) )
24 11 a1i 
 |-  ( ph -> C = ( N ` ( G u. H ) ) )
25 15 16 22 23 24 rgspncl 
 |-  ( ph -> C e. ( SubRing ` L ) )
26 4 25 subrfld 
 |-  ( ph -> ( L |`s C ) e. IDomn )
27 12 26 eqeltrid 
 |-  ( ph -> E e. IDomn )
28 27 idomcringd 
 |-  ( ph -> E e. CRing )
29 sdrgsubrg 
 |-  ( G e. ( SubDRing ` L ) -> G e. ( SubRing ` L ) )
30 7 29 syl 
 |-  ( ph -> G e. ( SubRing ` L ) )
31 15 16 22 23 24 rgspnssid 
 |-  ( ph -> ( G u. H ) C_ C )
32 31 unssad 
 |-  ( ph -> G C_ C )
33 12 subsubrg 
 |-  ( C e. ( SubRing ` L ) -> ( G e. ( SubRing ` E ) <-> ( G e. ( SubRing ` L ) /\ G C_ C ) ) )
34 33 biimpar 
 |-  ( ( C e. ( SubRing ` L ) /\ ( G e. ( SubRing ` L ) /\ G C_ C ) ) -> G e. ( SubRing ` E ) )
35 25 30 32 34 syl12anc 
 |-  ( ph -> G e. ( SubRing ` E ) )
36 eqid 
 |-  ( ( subringAlg ` E ) ` G ) = ( ( subringAlg ` E ) ` G )
37 36 sraassa 
 |-  ( ( E e. CRing /\ G e. ( SubRing ` E ) ) -> ( ( subringAlg ` E ) ` G ) e. AssAlg )
38 28 35 37 syl2anc 
 |-  ( ph -> ( ( subringAlg ` E ) ` G ) e. AssAlg )
39 eqid 
 |-  ( Base ` E ) = ( Base ` E )
40 17 subrgss 
 |-  ( C e. ( SubRing ` L ) -> C C_ ( Base ` L ) )
41 25 40 syl 
 |-  ( ph -> C C_ ( Base ` L ) )
42 12 17 ressbas2 
 |-  ( C C_ ( Base ` L ) -> C = ( Base ` E ) )
43 41 42 syl 
 |-  ( ph -> C = ( Base ` E ) )
44 32 43 sseqtrd 
 |-  ( ph -> G C_ ( Base ` E ) )
45 36 39 27 44 sraidom 
 |-  ( ph -> ( ( subringAlg ` E ) ` G ) e. IDomn )
46 ressabs 
 |-  ( ( C e. ( SubRing ` L ) /\ G C_ C ) -> ( ( L |`s C ) |`s G ) = ( L |`s G ) )
47 25 32 46 syl2anc 
 |-  ( ph -> ( ( L |`s C ) |`s G ) = ( L |`s G ) )
48 12 oveq1i 
 |-  ( E |`s G ) = ( ( L |`s C ) |`s G )
49 47 48 2 3eqtr4g 
 |-  ( ph -> ( E |`s G ) = I )
50 eqidd 
 |-  ( ph -> ( ( subringAlg ` E ) ` G ) = ( ( subringAlg ` E ) ` G ) )
51 50 44 srasca 
 |-  ( ph -> ( E |`s G ) = ( Scalar ` ( ( subringAlg ` E ) ` G ) ) )
52 49 51 eqtr3d 
 |-  ( ph -> I = ( Scalar ` ( ( subringAlg ` E ) ` G ) ) )
53 2 sdrgdrng 
 |-  ( G e. ( SubDRing ` L ) -> I e. DivRing )
54 7 53 syl 
 |-  ( ph -> I e. DivRing )
55 52 54 eqeltrrd 
 |-  ( ph -> ( Scalar ` ( ( subringAlg ` E ) ` G ) ) e. DivRing )
56 36 sralmod 
 |-  ( G e. ( SubRing ` E ) -> ( ( subringAlg ` E ) ` G ) e. LMod )
57 35 56 syl 
 |-  ( ph -> ( ( subringAlg ` E ) ` G ) e. LMod )
58 13 islvec 
 |-  ( ( ( subringAlg ` E ) ` G ) e. LVec <-> ( ( ( subringAlg ` E ) ` G ) e. LMod /\ ( Scalar ` ( ( subringAlg ` E ) ` G ) ) e. DivRing ) )
59 57 55 58 sylanbrc 
 |-  ( ph -> ( ( subringAlg ` E ) ` G ) e. LVec )
60 dimcl 
 |-  ( ( ( subringAlg ` E ) ` G ) e. LVec -> ( dim ` ( ( subringAlg ` E ) ` G ) ) e. NN0* )
61 59 60 syl 
 |-  ( ph -> ( dim ` ( ( subringAlg ` E ) ` G ) ) e. NN0* )
62 1 2 3 4 5 6 7 8 9 10 11 12 fldextrspunlem1 
 |-  ( ph -> ( dim ` ( ( subringAlg ` E ) ` G ) ) <_ ( J [:] K ) )
63 xnn0lenn0nn0 
 |-  ( ( ( dim ` ( ( subringAlg ` E ) ` G ) ) e. NN0* /\ ( J [:] K ) e. NN0 /\ ( dim ` ( ( subringAlg ` E ) ` G ) ) <_ ( J [:] K ) ) -> ( dim ` ( ( subringAlg ` E ) ` G ) ) e. NN0 )
64 61 9 62 63 syl3anc 
 |-  ( ph -> ( dim ` ( ( subringAlg ` E ) ` G ) ) e. NN0 )
65 13 38 45 55 64 assafld 
 |-  ( ph -> ( ( subringAlg ` E ) ` G ) e. Field )
66 50 44 srabase 
 |-  ( ph -> ( Base ` E ) = ( Base ` ( ( subringAlg ` E ) ` G ) ) )
67 43 66 eqtrd 
 |-  ( ph -> C = ( Base ` ( ( subringAlg ` E ) ` G ) ) )
68 50 44 sraaddg 
 |-  ( ph -> ( +g ` E ) = ( +g ` ( ( subringAlg ` E ) ` G ) ) )
69 68 oveqdr 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` E ) y ) = ( x ( +g ` ( ( subringAlg ` E ) ` G ) ) y ) )
70 50 44 sramulr 
 |-  ( ph -> ( .r ` E ) = ( .r ` ( ( subringAlg ` E ) ` G ) ) )
71 70 oveqdr 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( .r ` E ) y ) = ( x ( .r ` ( ( subringAlg ` E ) ` G ) ) y ) )
72 43 67 69 71 fldpropd 
 |-  ( ph -> ( E e. Field <-> ( ( subringAlg ` E ) ` G ) e. Field ) )
73 65 72 mpbird 
 |-  ( ph -> E e. Field )