fldextrspundgle

Description: Inequality involving the degree of two different field extensions I and J of a same field F . 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	⊢ 𝐾 = ( 𝐿 ↾_s 𝐹 )
	fldextrspunfld.i	⊢ 𝐼 = ( 𝐿 ↾_s 𝐺 )
	fldextrspunfld.j	⊢ 𝐽 = ( 𝐿 ↾_s 𝐻 )
	fldextrspunfld.2	⊢ ( 𝜑 → 𝐿 ∈ Field )
	fldextrspunfld.3	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
	fldextrspunfld.4	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
	fldextrspunfld.5	⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
	fldextrspunfld.6	⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
	fldextrspunfld.7	⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ₀ )
	fldextrspundgle.1	⊢ 𝐸 = ( 𝐿 ↾_s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
Assertion	fldextrspundgle	⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ≤ ( 𝐽 [:] 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		fldextrspunfld.k	⊢ 𝐾 = ( 𝐿 ↾_s 𝐹 )
2		fldextrspunfld.i	⊢ 𝐼 = ( 𝐿 ↾_s 𝐺 )
3		fldextrspunfld.j	⊢ 𝐽 = ( 𝐿 ↾_s 𝐻 )
4		fldextrspunfld.2	⊢ ( 𝜑 → 𝐿 ∈ Field )
5		fldextrspunfld.3	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
6		fldextrspunfld.4	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
7		fldextrspunfld.5	⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
8		fldextrspunfld.6	⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
9		fldextrspunfld.7	⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ₀ )
10		fldextrspundgle.1	⊢ 𝐸 = ( 𝐿 ↾_s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
11		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
12	11	sdrgss	⊢ ( 𝐻 ∈ ( SubDRing ‘ 𝐿 ) → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
13	8 12	syl	⊢ ( 𝜑 → 𝐻 ⊆ ( Base ‘ 𝐿 ) )
14	11 2 10 4 7 13	fldgenfldext	⊢ ( 𝜑 → 𝐸 /_FldExt 𝐼 )
15		extdgval	⊢ ( 𝐸 /_FldExt 𝐼 → ( 𝐸 [:] 𝐼 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐼 ) ) ) )
16	14 15	syl	⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐼 ) ) ) )
17		eqid	⊢ ( RingSpan ‘ 𝐿 ) = ( RingSpan ‘ 𝐿 )
18		eqid	⊢ ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) = ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) )
19		eqid	⊢ ( 𝐿 ↾_s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) = ( 𝐿 ↾_s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) )
20	1 2 3 4 5 6 7 8 9 17 18 19	fldextrspunlem2	⊢ ( 𝜑 → ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) = ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) )
21	20	oveq2d	⊢ ( 𝜑 → ( 𝐿 ↾_s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) = ( 𝐿 ↾_s ( 𝐿 fldGen ( 𝐺 ∪ 𝐻 ) ) ) )
22	21 10	eqtr4di	⊢ ( 𝜑 → ( 𝐿 ↾_s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) = 𝐸 )
23	22	fveq2d	⊢ ( 𝜑 → ( subringAlg ‘ ( 𝐿 ↾_s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) ) = ( subringAlg ‘ 𝐸 ) )
24	11	sdrgss	⊢ ( 𝐺 ∈ ( SubDRing ‘ 𝐿 ) → 𝐺 ⊆ ( Base ‘ 𝐿 ) )
25	2 11	ressbas2	⊢ ( 𝐺 ⊆ ( Base ‘ 𝐿 ) → 𝐺 = ( Base ‘ 𝐼 ) )
26	7 24 25	3syl	⊢ ( 𝜑 → 𝐺 = ( Base ‘ 𝐼 ) )
27	23 26	fveq12d	⊢ ( 𝜑 → ( ( subringAlg ‘ ( 𝐿 ↾_s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) ) ‘ 𝐺 ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐼 ) ) )
28	27	fveq2d	⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ ( 𝐿 ↾_s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) ) ‘ 𝐺 ) ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐼 ) ) ) )
29	1 2 3 4 5 6 7 8 9 17 18 19	fldextrspunlem1	⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ ( 𝐿 ↾_s ( ( RingSpan ‘ 𝐿 ) ‘ ( 𝐺 ∪ 𝐻 ) ) ) ) ‘ 𝐺 ) ) ≤ ( 𝐽 [:] 𝐾 ) )
30	28 29	eqbrtrrd	⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐼 ) ) ) ≤ ( 𝐽 [:] 𝐾 ) )
31	16 30	eqbrtrd	⊢ ( 𝜑 → ( 𝐸 [:] 𝐼 ) ≤ ( 𝐽 [:] 𝐾 ) )

Metamath Proof Explorer

Theorem fldextrspundgle

Proof