This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 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 fldextrspunlem2 ⊢ φ → C = L fldGen G ∪ H

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 4 flddrngd ⊢ φ → L ∈ DivRing
14 13 drngringd ⊢ φ → L ∈ Ring
15 eqidd ⊢ φ → Base L = Base L
16 eqid ⊢ Base L = Base L
17 16 sdrgss ⊢ G ∈ SubDRing ⁡ L → G ⊆ Base L
18 7 17 syl ⊢ φ → G ⊆ Base L
19 16 sdrgss ⊢ H ∈ SubDRing ⁡ L → H ⊆ Base L
20 8 19 syl ⊢ φ → H ⊆ Base L
21 18 20 unssd ⊢ φ → G ∪ H ⊆ Base L
22 10 a1i ⊢ φ → N = RingSpan ⁡ L
23 11 a1i ⊢ φ → C = N ⁡ G ∪ H
24 16 13 21 fldgensdrg ⊢ φ → L fldGen G ∪ H ∈ SubDRing ⁡ L
25 sdrgsubrg ⊢ L fldGen G ∪ H ∈ SubDRing ⁡ L → L fldGen G ∪ H ∈ SubRing ⁡ L
26 24 25 syl ⊢ φ → L fldGen G ∪ H ∈ SubRing ⁡ L
27 16 13 21 fldgenssid ⊢ φ → G ∪ H ⊆ L fldGen G ∪ H
28 14 15 21 22 23 26 27 rgspnmin ⊢ φ → C ⊆ L fldGen G ∪ H
29 14 15 21 22 23 rgspncl ⊢ φ → C ∈ SubRing ⁡ L
30 1 2 3 4 5 6 7 8 9 10 11 12 fldextrspunfld ⊢ φ → E ∈ Field
31 30 flddrngd ⊢ φ → E ∈ DivRing
32 12 31 eqeltrrid ⊢ φ → L ↾ 𝑠 C ∈ DivRing
33 issdrg ⊢ C ∈ SubDRing ⁡ L ↔ L ∈ DivRing ∧ C ∈ SubRing ⁡ L ∧ L ↾ 𝑠 C ∈ DivRing
34 13 29 32 33 syl3anbrc ⊢ φ → C ∈ SubDRing ⁡ L
35 14 15 21 22 23 rgspnssid ⊢ φ → G ∪ H ⊆ C
36 16 13 34 35 fldgenssp ⊢ φ → L fldGen G ∪ H ⊆ C
37 28 36 eqssd ⊢ φ → C = L fldGen G ∪ H