fldextrspundgle - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fldextrspundgle		Structured version Visualization version GIF version

Theorem fldextrspundgle 33670

Description: Inequality involving the degree of two different field extensions 𝐼 and 𝐽 of a same field 𝐹. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
fldextrspundgle	⊢ (𝜑 → (𝐸[:]𝐼) ≤ (𝐽[:]𝐾))

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2107 ∪ cun 3929 ⊆ wss 3931 class class class wbr 5123 ‘cfv 6541 (class class class)co 7413 ≤ cle 11278 ℕ₀cn0 12509 Basecbs 17230 ↾_s cress 17253 RingSpancrgspn 20579 Fieldcfield 20699 SubDRingcsdrg 20756 subringAlg csra 21139 fldGen cfldgen 33257 dimcldim 33589 /_FldExtcfldext 33629 [:]cextdg 33632

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-reg 9614 ax-inf2 9663 ax-ac2 10485 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-pre-sup 11215 ax-addf 11216

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7679 df-rpss 7725 df-om 7870 df-1st 7996 df-2nd 7997 df-supp 8168 df-tpos 8233 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-oadd 8492 df-er 8727 df-map 8850 df-ixp 8920 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-fsupp 9384 df-sup 9464 df-inf 9465 df-oi 9532 df-r1 9786 df-rank 9787 df-dju 9923 df-card 9961 df-acn 9964 df-ac 10138 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-div 11903 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-7 12316 df-8 12317 df-9 12318 df-n0 12510 df-xnn0 12583 df-z 12597 df-dec 12717 df-uz 12861 df-rp 13017 df-xadd 13137 df-fz 13530 df-fzo 13677 df-seq 14025 df-exp 14085 df-hash 14353 df-word 14536 df-lsw 14584 df-concat 14592 df-s1 14617 df-substr 14662 df-pfx 14692 df-s2 14870 df-cj 15121 df-re 15122 df-im 15123 df-sqrt 15257 df-abs 15258 df-clim 15507 df-sum 15706 df-struct 17167 df-sets 17184 df-slot 17202 df-ndx 17214 df-base 17231 df-ress 17254 df-plusg 17287 df-mulr 17288 df-starv 17289 df-sca 17290 df-vsca 17291 df-ip 17292 df-tset 17293 df-ple 17294 df-ocomp 17295 df-ds 17296 df-unif 17297 df-hom 17298 df-cco 17299 df-0g 17458 df-gsum 17459 df-prds 17464 df-pws 17466 df-mre 17601 df-mrc 17602 df-mri 17603 df-acs 17604 df-proset 18311 df-drs 18312 df-poset 18330 df-ipo 18543 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-mhm 18766 df-submnd 18767 df-grp 18924 df-minusg 18925 df-sbg 18926 df-mulg 19056 df-subg 19111 df-ghm 19201 df-cntz 19305 df-cntr 19306 df-lsm 19623 df-cmn 19769 df-abl 19770 df-mgp 20107 df-rng 20119 df-ur 20148 df-ring 20201 df-cring 20202 df-oppr 20303 df-dvdsr 20326 df-unit 20327 df-invr 20357 df-dvr 20370 df-nzr 20482 df-subrng 20515 df-subrg 20539 df-rgspn 20580 df-rlreg 20663 df-domn 20664 df-idom 20665 df-drng 20700 df-field 20701 df-sdrg 20757 df-lmod 20829 df-lss 20899 df-lsp 20939 df-lmhm 20990 df-lmim 20991 df-lbs 21043 df-lvec 21071 df-sra 21141 df-rgmod 21142 df-cnfld 21328 df-zring 21421 df-dsmm 21707 df-frlm 21722 df-uvc 21758 df-lindf 21781 df-linds 21782 df-assa 21828 df-ind 32781 df-fldgen 33258 df-dim 33590 df-fldext 33633 df-extdg 33634

This theorem is referenced by: fldextrspundglemul 33671

W3C validator