Metamath Proof Explorer

Theorem fldgenfldext

Description: A subfield F extended with a set A forms a field extension. (Contributed by Thierry Arnoux, 22-Jun-2025)

Ref Expression
Hypotheses fldgenfldext.b ⊢ B = Base E
fldgenfldext.k ⊢ K = E ↾ 𝑠 F
fldgenfldext.l ⊢ L = E ↾ 𝑠 E fldGen F ∪ A
fldgenfldext.e ⊢ φ → E ∈ Field
fldgenfldext.f ⊢ φ → F ∈ SubDRing ⁡ E
fldgenfldext.1 ⊢ φ → A ⊆ B
Assertion fldgenfldext ⊢ φ → L /FldExt K

Proof

Step Hyp Ref Expression
1 fldgenfldext.b ⊢ B = Base E
2 fldgenfldext.k ⊢ K = E ↾ 𝑠 F
3 fldgenfldext.l ⊢ L = E ↾ 𝑠 E fldGen F ∪ A
4 fldgenfldext.e ⊢ φ → E ∈ Field
5 fldgenfldext.f ⊢ φ → F ∈ SubDRing ⁡ E
6 fldgenfldext.1 ⊢ φ → A ⊆ B
7 1 sdrgss ⊢ F ∈ SubDRing ⁡ E → F ⊆ B
8 5 7 syl ⊢ φ → F ⊆ B
9 8 6 unssd ⊢ φ → F ∪ A ⊆ B
10 1 4 9 fldgenfld ⊢ φ → E ↾ 𝑠 E fldGen F ∪ A ∈ Field
11 3 10 eqeltrid ⊢ φ → L ∈ Field
12 fldsdrgfld ⊢ E ∈ Field ∧ F ∈ SubDRing ⁡ E → E ↾ 𝑠 F ∈ Field
13 4 5 12 syl2anc ⊢ φ → E ↾ 𝑠 F ∈ Field
14 2 13 eqeltrid ⊢ φ → K ∈ Field
15 3 oveq1i ⊢ L ↾ 𝑠 F = E ↾ 𝑠 E fldGen F ∪ A ↾ 𝑠 F
16 ovexd ⊢ φ → E fldGen F ∪ A ∈ V
17 ressress ⊢ E fldGen F ∪ A ∈ V ∧ F ∈ SubDRing ⁡ E → E ↾ 𝑠 E fldGen F ∪ A ↾ 𝑠 F = E ↾ 𝑠 E fldGen F ∪ A ∩ F
18 16 5 17 syl2anc ⊢ φ → E ↾ 𝑠 E fldGen F ∪ A ↾ 𝑠 F = E ↾ 𝑠 E fldGen F ∪ A ∩ F
19 15 18 eqtrid ⊢ φ → L ↾ 𝑠 F = E ↾ 𝑠 E fldGen F ∪ A ∩ F
20 4 flddrngd ⊢ φ → E ∈ DivRing
21 1 20 9 fldgenssid ⊢ φ → F ∪ A ⊆ E fldGen F ∪ A
22 21 unssad ⊢ φ → F ⊆ E fldGen F ∪ A
23 sseqin2 ⊢ F ⊆ E fldGen F ∪ A ↔ E fldGen F ∪ A ∩ F = F
24 22 23 sylib ⊢ φ → E fldGen F ∪ A ∩ F = F
25 24 oveq2d ⊢ φ → E ↾ 𝑠 E fldGen F ∪ A ∩ F = E ↾ 𝑠 F
26 19 25 eqtrd ⊢ φ → L ↾ 𝑠 F = E ↾ 𝑠 F
27 2 1 ressbas2 ⊢ F ⊆ B → F = Base K
28 8 27 syl ⊢ φ → F = Base K
29 28 oveq2d ⊢ φ → L ↾ 𝑠 F = L ↾ 𝑠 Base K
30 26 29 eqtr3d ⊢ φ → E ↾ 𝑠 F = L ↾ 𝑠 Base K
31 2 30 eqtrid ⊢ φ → K = L ↾ 𝑠 Base K
32 11 fldcrngd ⊢ φ → L ∈ CRing
33 32 crngringd ⊢ φ → L ∈ Ring
34 14 fldcrngd ⊢ φ → K ∈ CRing
35 34 crngringd ⊢ φ → K ∈ Ring
36 2 35 eqeltrrid ⊢ φ → E ↾ 𝑠 F ∈ Ring
37 26 36 eqeltrd ⊢ φ → L ↾ 𝑠 F ∈ Ring
38 1 20 9 fldgenssv ⊢ φ → E fldGen F ∪ A ⊆ B
39 3 1 ressbas2 ⊢ E fldGen F ∪ A ⊆ B → E fldGen F ∪ A = Base L
40 38 39 syl ⊢ φ → E fldGen F ∪ A = Base L
41 22 40 sseqtrd ⊢ φ → F ⊆ Base L
42 20 drngringd ⊢ φ → E ∈ Ring
43 sdrgsubrg ⊢ F ∈ SubDRing ⁡ E → F ∈ SubRing ⁡ E
44 eqid ⊢ 1 E = 1 E
45 44 subrg1cl ⊢ F ∈ SubRing ⁡ E → 1 E ∈ F
46 5 43 45 3syl ⊢ φ → 1 E ∈ F
47 22 46 sseldd ⊢ φ → 1 E ∈ E fldGen F ∪ A
48 3 1 44 ress1r ⊢ E ∈ Ring ∧ 1 E ∈ E fldGen F ∪ A ∧ E fldGen F ∪ A ⊆ B → 1 E = 1 L
49 42 47 38 48 syl3anc ⊢ φ → 1 E = 1 L
50 49 46 eqeltrrd ⊢ φ → 1 L ∈ F
51 41 50 jca ⊢ φ → F ⊆ Base L ∧ 1 L ∈ F
52 eqid ⊢ Base L = Base L
53 eqid ⊢ 1 L = 1 L
54 52 53 issubrg ⊢ F ∈ SubRing ⁡ L ↔ L ∈ Ring ∧ L ↾ 𝑠 F ∈ Ring ∧ F ⊆ Base L ∧ 1 L ∈ F
55 33 37 51 54 syl21anbrc ⊢ φ → F ∈ SubRing ⁡ L
56 28 55 eqeltrrd ⊢ φ → Base K ∈ SubRing ⁡ L
57 brfldext ⊢ L ∈ Field ∧ K ∈ Field → L /FldExt K ↔ K = L ↾ 𝑠 Base K ∧ Base K ∈ SubRing ⁡ L
58 57 biimpar ⊢ L ∈ Field ∧ K ∈ Field ∧ K = L ↾ 𝑠 Base K ∧ Base K ∈ SubRing ⁡ L → L /FldExt K
59 11 14 31 56 58 syl22anc ⊢ φ → L /FldExt K