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	$⊢ φ \to L \in Field$
	fldextrspunfld.3	$⊢ φ \to F \in SubDRing (I)$
	fldextrspunfld.4	$⊢ φ \to F \in SubDRing (J)$
	fldextrspunfld.5	$⊢ φ \to G \in SubDRing (L)$
	fldextrspunfld.6	$⊢ φ \to H \in SubDRing (L)$
	fldextrspunfld.7	$⊢ φ \to J [. : .] K \in ℕ_{0}$
	fldextrspunfld.n	$⊢ N = RingSpan (L)$
	fldextrspunfld.c	$⊢ C = N (G \cup H)$
	fldextrspunfld.e	$⊢ E = L ↾_{𝑠} C$
Assertion	fldextrspunlem2	$⊢ φ \to C = L fldGen (G \cup 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	$⊢ φ \to L \in Field$
5		fldextrspunfld.3	$⊢ φ \to F \in SubDRing (I)$
6		fldextrspunfld.4	$⊢ φ \to F \in SubDRing (J)$
7		fldextrspunfld.5	$⊢ φ \to G \in SubDRing (L)$
8		fldextrspunfld.6	$⊢ φ \to H \in SubDRing (L)$
9		fldextrspunfld.7	$⊢ φ \to J [. : .] K \in ℕ_{0}$
10		fldextrspunfld.n	$⊢ N = RingSpan (L)$
11		fldextrspunfld.c	$⊢ C = N (G \cup H)$
12		fldextrspunfld.e	$⊢ E = L ↾_{𝑠} C$
13	4	flddrngd	$⊢ φ \to L \in DivRing$
14	13	drngringd	$⊢ φ \to L \in Ring$
15		eqidd	$⊢ φ \to {Base}_{L} = {Base}_{L}$
16		eqid	$⊢ {Base}_{L} = {Base}_{L}$
17	16	sdrgss	$⊢ G \in SubDRing (L) \to G \subseteq {Base}_{L}$
18	7 17	syl	$⊢ φ \to G \subseteq {Base}_{L}$
19	16	sdrgss	$⊢ H \in SubDRing (L) \to H \subseteq {Base}_{L}$
20	8 19	syl	$⊢ φ \to H \subseteq {Base}_{L}$
21	18 20	unssd	$⊢ φ \to G \cup H \subseteq {Base}_{L}$
22	10	a1i	$⊢ φ \to N = RingSpan (L)$
23	11	a1i	$⊢ φ \to C = N (G \cup H)$
24	16 13 21	fldgensdrg	$⊢ φ \to L fldGen (G \cup H) \in SubDRing (L)$
25		sdrgsubrg	$⊢ L fldGen (G \cup H) \in SubDRing (L) \to L fldGen (G \cup H) \in SubRing (L)$
26	24 25	syl	$⊢ φ \to L fldGen (G \cup H) \in SubRing (L)$
27	16 13 21	fldgenssid	$⊢ φ \to G \cup H \subseteq L fldGen (G \cup H)$
28	14 15 21 22 23 26 27	rgspnmin	$⊢ φ \to C \subseteq L fldGen (G \cup H)$
29	14 15 21 22 23	rgspncl	$⊢ φ \to C \in SubRing (L)$
30	1 2 3 4 5 6 7 8 9 10 11 12	fldextrspunfld	$⊢ φ \to E \in Field$
31	30	flddrngd	$⊢ φ \to E \in DivRing$
32	12 31	eqeltrrid	$⊢ φ \to L ↾_{𝑠} C \in DivRing$
33		issdrg	$⊢ C \in SubDRing (L) \leftrightarrow (L \in DivRing \land C \in SubRing (L) \land L ↾_{𝑠} C \in DivRing)$
34	13 29 32 33	syl3anbrc	$⊢ φ \to C \in SubDRing (L)$
35	14 15 21 22 23	rgspnssid	$⊢ φ \to G \cup H \subseteq C$
36	16 13 34 35	fldgenssp	$⊢ φ \to L fldGen (G \cup H) \subseteq C$
37	28 36	eqssd	$⊢ φ \to C = L fldGen (G \cup H)$

Metamath Proof Explorer

Theorem fldextrspunlem2

Proof