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 ⊢ 𝐾 = ( 𝐿 ↾s 𝐹 )
fldextrspunfld.i ⊢ 𝐼 = ( 𝐿 ↾s 𝐺 )
fldextrspunfld.j ⊢ 𝐽 = ( 𝐿 ↾s 𝐻 )
fldextrspunfld.2 ⊢ ( 𝜑 → 𝐿 ∈ Field )
fldextrspunfld.3 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
fldextrspunfld.4 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
fldextrspunfld.5 ⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
fldextrspunfld.6 ⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
fldextrspunfld.7 ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ0 )
fldextrspunfld.n ⊢ 𝑁 = ( RingSpan ‘ 𝐿 )
fldextrspunfld.c ⊢ 𝐶 = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) )
fldextrspunfld.e ⊢ 𝐸 = ( 𝐿 ↾s 𝐶 )
Assertion fldextrspunlem2 ( 𝜑 → 𝐶 = ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 fldextrspunfld.k ⊢ 𝐾 = ( 𝐿 ↾s 𝐹 )
2 fldextrspunfld.i ⊢ 𝐼 = ( 𝐿 ↾s 𝐺 )
3 fldextrspunfld.j ⊢ 𝐽 = ( 𝐿 ↾s 𝐻 )
4 fldextrspunfld.2 ⊢ ( 𝜑 → 𝐿 ∈ Field )
5 fldextrspunfld.3 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
6 fldextrspunfld.4 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
7 fldextrspunfld.5 ⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
8 fldextrspunfld.6 ⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
9 fldextrspunfld.7 ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ0 )
10 fldextrspunfld.n ⊢ 𝑁 = ( RingSpan ‘ 𝐿 )
11 fldextrspunfld.c ⊢ 𝐶 = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) )
12 fldextrspunfld.e ⊢ 𝐸 = ( 𝐿 ↾s 𝐶 )
13 4 flddrngd ⊢ ( 𝜑 → 𝐿 ∈ DivRing )
14 13 drngringd ⊢ ( 𝜑 → 𝐿 ∈ Ring )
15 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 ) )
16 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
17 16 sdrgss ⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
18 7 17 syl ⊢ ( 𝜑 → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
19 16 sdrgss ⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
20 8 19 syl ⊢ ( 𝜑 → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
21 18 20 unssd ⊢ ( 𝜑 → ( 𝐺 ∪ 𝐻 ) ⊆ ( Base ‘ 𝐿 ) )
22 10 a1i ⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝐿 ) )
23 11 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
24 16 13 21 fldgensdrg ⊢ ( 𝜑 → ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ∈ ( SubDRing ‘ 𝐿 ) )
25 sdrgsubrg ⊢ ( ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ∈ ( SubDRing ‘ 𝐿 ) → ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ∈ ( SubRing ‘ 𝐿 ) )
26 24 25 syl ⊢ ( 𝜑 → ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ∈ ( SubRing ‘ 𝐿 ) )
27 16 13 21 fldgenssid ⊢ ( 𝜑 → ( 𝐺 ∪ 𝐻 ) ⊆ ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
28 14 15 21 22 23 26 27 rgspnmin ⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
29 14 15 21 22 23 rgspncl ⊢ ( 𝜑 → 𝐶 ∈ ( SubRing ‘ 𝐿 ) )
30 1 2 3 4 5 6 7 8 9 10 11 12 fldextrspunfld ⊢ ( 𝜑 → 𝐸 ∈ Field )
31 30 flddrngd ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
32 12 31 eqeltrrid ⊢ ( 𝜑 → ( 𝐿 ↾s 𝐶 ) ∈ DivRing )
33 issdrg ⊢ ( 𝐶 ∈ ( SubDRing ‘ 𝐿 ) ↔ ( 𝐿 ∈ DivRing ∧ 𝐶 ∈ ( SubRing ‘ 𝐿 ) ∧ ( 𝐿 ↾s 𝐶 ) ∈ DivRing ) )
34 13 29 32 33 syl3anbrc ⊢ ( 𝜑 → 𝐶 ∈ ( SubDRing ‘ 𝐿 ) )
35 14 15 21 22 23 rgspnssid ⊢ ( 𝜑 → ( 𝐺 ∪ 𝐻 ) ⊆ 𝐶 )
36 16 13 34 35 fldgenssp ⊢ ( 𝜑 → ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ⊆ 𝐶 )
37 28 36 eqssd ⊢ ( 𝜑 → 𝐶 = ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )