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 ⊢ 𝐾 = ( 𝐿 ↾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 fldextrspunfld ( 𝜑 → 𝐸 ∈ Field )

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 eqid ⊢ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) )
14 4 flddrngd ⊢ ( 𝜑 → 𝐿 ∈ DivRing )
15 14 drngringd ⊢ ( 𝜑 → 𝐿 ∈ Ring )
16 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 ) )
17 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
18 17 sdrgss ⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
19 7 18 syl ⊢ ( 𝜑 → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
20 17 sdrgss ⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
21 8 20 syl ⊢ ( 𝜑 → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
22 19 21 unssd ⊢ ( 𝜑 → ( 𝐺 ∪ 𝐻 ) ⊆ ( Base ‘ 𝐿 ) )
23 10 a1i ⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝐿 ) )
24 11 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
25 15 16 22 23 24 rgspncl ⊢ ( 𝜑 → 𝐶 ∈ ( SubRing ‘ 𝐿 ) )
26 4 25 subrfld ⊢ ( 𝜑 → ( 𝐿 ↾s 𝐶 ) ∈ IDomn )
27 12 26 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ IDomn )
28 27 idomcringd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
29 sdrgsubrg ⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐺 ∈ ( SubRing ‘ 𝐿 ) )
30 7 29 syl ⊢ ( 𝜑 → 𝐺 ∈ ( SubRing ‘ 𝐿 ) )
31 15 16 22 23 24 rgspnssid ⊢ ( 𝜑 → ( 𝐺 ∪ 𝐻 ) ⊆ 𝐶 )
32 31 unssad ⊢ ( 𝜑 → 𝐺 ⊆ 𝐶 )
33 12 subsubrg ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝐿 ) → ( 𝐺 ∈ ( SubRing ‘ 𝐸 ) ↔ ( 𝐺 ∈ ( SubRing ‘ 𝐿 ) ∧ 𝐺 ⊆ 𝐶 ) ) )
34 33 biimpar ⊢ ( ( 𝐶 ∈ ( SubRing ‘ 𝐿 ) ∧ ( 𝐺 ∈ ( SubRing ‘ 𝐿 ) ∧ 𝐺 ⊆ 𝐶 ) ) → 𝐺 ∈ ( SubRing ‘ 𝐸 ) )
35 25 30 32 34 syl12anc ⊢ ( 𝜑 → 𝐺 ∈ ( SubRing ‘ 𝐸 ) )
36 eqid ⊢ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) = ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 )
37 36 sraassa ⊢ ( ( 𝐸 ∈ CRing ∧ 𝐺 ∈ ( SubRing ‘ 𝐸 ) ) → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ AssAlg )
38 28 35 37 syl2anc ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ AssAlg )
39 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
40 17 subrgss ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝐿 ) → 𝐶 ⊆ ( Base ‘ 𝐿 ) )
41 25 40 syl ⊢ ( 𝜑 → 𝐶 ⊆ ( Base ‘ 𝐿 ) )
42 12 17 ressbas2 ⊢ ( 𝐶 ⊆ ( Base ‘ 𝐿 ) → 𝐶 = ( Base ‘ 𝐸 ) )
43 41 42 syl ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝐸 ) )
44 32 43 sseqtrd ⊢ ( 𝜑 → 𝐺 ⊆ ( Base ‘ 𝐸 ) )
45 36 39 27 44 sraidom ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ IDomn )
46 ressabs ⊢ ( ( 𝐶 ∈ ( SubRing ‘ 𝐿 ) ∧ 𝐺 ⊆ 𝐶 ) → ( ( 𝐿 ↾s 𝐶 ) ↾s 𝐺 ) = ( 𝐿 ↾s 𝐺 ) )
47 25 32 46 syl2anc ⊢ ( 𝜑 → ( ( 𝐿 ↾s 𝐶 ) ↾s 𝐺 ) = ( 𝐿 ↾s 𝐺 ) )
48 12 oveq1i ⊢ ( 𝐸 ↾s 𝐺 ) = ( ( 𝐿 ↾s 𝐶 ) ↾s 𝐺 )
49 47 48 2 3eqtr4g ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐺 ) = 𝐼 )
50 eqidd ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) = ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) )
51 50 44 srasca ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐺 ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) )
52 49 51 eqtr3d ⊢ ( 𝜑 → 𝐼 = ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) )
53 2 sdrgdrng ⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐼 ∈ DivRing )
54 7 53 syl ⊢ ( 𝜑 → 𝐼 ∈ DivRing )
55 52 54 eqeltrrd ⊢ ( 𝜑 → ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) ∈ DivRing )
56 36 sralmod ⊢ ( 𝐺 ∈ ( SubRing ‘ 𝐸 ) → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ LMod )
57 35 56 syl ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ LMod )
58 13 islvec ⊢ ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ LVec ↔ ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ LMod ∧ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) ∈ DivRing ) )
59 57 55 58 sylanbrc ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ LVec )
60 dimcl ⊢ ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ LVec → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) ∈ ℕ0* )
61 59 60 syl ⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) ∈ ℕ0* )
62 1 2 3 4 5 6 7 8 9 10 11 12 fldextrspunlem1 ⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) ≤ ( 𝐽 [:] 𝐾 ) )
63 xnn0lenn0nn0 ⊢ ( ( ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) ∈ ℕ0* ∧ ( 𝐽 [:] 𝐾 ) ∈ ℕ0 ∧ ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) ≤ ( 𝐽 [:] 𝐾 ) ) → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) ∈ ℕ0 )
64 61 9 62 63 syl3anc ⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) ∈ ℕ0 )
65 13 38 45 55 64 assafld ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ Field )
66 50 44 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) )
67 43 66 eqtrd ⊢ ( 𝜑 → 𝐶 = ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) )
68 50 44 sraaddg ⊢ ( 𝜑 → ( +g ‘ 𝐸 ) = ( +g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) )
69 68 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝐸 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) 𝑦 ) )
70 50 44 sramulr ⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( .r ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) )
71 70 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( .r ‘ 𝐸 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) 𝑦 ) )
72 43 67 69 71 fldpropd ⊢ ( 𝜑 → ( 𝐸 ∈ Field ↔ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ∈ Field ) )
73 65 72 mpbird ⊢ ( 𝜑 → 𝐸 ∈ Field )