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 ↾ 𝑠 F
fldextrspunfld.i ⊢ I = L ↾ 𝑠 G
fldextrspunfld.j ⊢ J = L ↾ 𝑠 H
fldextrspunfld.2 ⊢ φ → L ∈ Field
fldextrspunfld.3 ⊢ φ → F ∈ SubDRing ⁡ I
fldextrspunfld.4 ⊢ φ → F ∈ SubDRing ⁡ J
fldextrspunfld.5 ⊢ φ → G ∈ SubDRing ⁡ L
fldextrspunfld.6 ⊢ φ → H ∈ SubDRing ⁡ L
fldextrspunfld.7 ⊢ φ → J .:. K ∈ ℕ 0
fldextrspunfld.n ⊢ N = RingSpan ⁡ L
fldextrspunfld.c ⊢ C = N ⁡ G ∪ H
fldextrspunfld.e ⊢ E = L ↾ 𝑠 C
Assertion fldextrspunfld ⊢ φ → E ∈ Field

Proof

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