Metamath Proof Explorer

Theorem fldextrspunlem2

Description: 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 fldextrspunlem2 
|- ( ph -> C = ( L fldGen ( G u. H ) ) )

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 4 flddrngd 
 |-  ( ph -> L e. DivRing )
14 13 drngringd 
 |-  ( ph -> L e. Ring )
15 eqidd 
 |-  ( ph -> ( Base ` L ) = ( Base ` L ) )
16 eqid 
 |-  ( Base ` L ) = ( Base ` L )
17 16 sdrgss 
 |-  ( G e. ( SubDRing ` L ) -> G C_ ( Base ` L ) )
18 7 17 syl 
 |-  ( ph -> G C_ ( Base ` L ) )
19 16 sdrgss 
 |-  ( H e. ( SubDRing ` L ) -> H C_ ( Base ` L ) )
20 8 19 syl 
 |-  ( ph -> H C_ ( Base ` L ) )
21 18 20 unssd 
 |-  ( ph -> ( G u. H ) C_ ( Base ` L ) )
22 10 a1i 
 |-  ( ph -> N = ( RingSpan ` L ) )
23 11 a1i 
 |-  ( ph -> C = ( N ` ( G u. H ) ) )
24 16 13 21 fldgensdrg 
 |-  ( ph -> ( L fldGen ( G u. H ) ) e. ( SubDRing ` L ) )
25 sdrgsubrg 
 |-  ( ( L fldGen ( G u. H ) ) e. ( SubDRing ` L ) -> ( L fldGen ( G u. H ) ) e. ( SubRing ` L ) )
26 24 25 syl 
 |-  ( ph -> ( L fldGen ( G u. H ) ) e. ( SubRing ` L ) )
27 16 13 21 fldgenssid 
 |-  ( ph -> ( G u. H ) C_ ( L fldGen ( G u. H ) ) )
28 14 15 21 22 23 26 27 rgspnmin 
 |-  ( ph -> C C_ ( L fldGen ( G u. H ) ) )
29 14 15 21 22 23 rgspncl 
 |-  ( ph -> C e. ( SubRing ` L ) )
30 1 2 3 4 5 6 7 8 9 10 11 12 fldextrspunfld 
 |-  ( ph -> E e. Field )
31 30 flddrngd 
 |-  ( ph -> E e. DivRing )
32 12 31 eqeltrrid 
 |-  ( ph -> ( L |`s C ) e. DivRing )
33 issdrg 
 |-  ( C e. ( SubDRing ` L ) <-> ( L e. DivRing /\ C e. ( SubRing ` L ) /\ ( L |`s C ) e. DivRing ) )
34 13 29 32 33 syl3anbrc 
 |-  ( ph -> C e. ( SubDRing ` L ) )
35 14 15 21 22 23 rgspnssid 
 |-  ( ph -> ( G u. H ) C_ C )
36 16 13 34 35 fldgenssp 
 |-  ( ph -> ( L fldGen ( G u. H ) ) C_ C )
37 28 36 eqssd 
 |-  ( ph -> C = ( L fldGen ( G u. H ) ) )