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 ⊢ 𝐵 = ( Base ‘ 𝐸 )
fldgenfldext.k ⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
fldgenfldext.l ⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ 𝐴 ) ) )
fldgenfldext.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
fldgenfldext.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
fldgenfldext.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion fldgenfldext ( 𝜑 → 𝐿 /FldExt 𝐾 )

Proof

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