fldext2rspun - Mathbox for Thierry Arnoux

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

Theorem fldext2rspun 34314

Description: Given two field extensions 𝐼 / 𝐾 and 𝐽 / 𝐾, 𝐼 / 𝐾 being a quadratic extension, and the degree of 𝐽 / 𝐾 being a power of 2, the degree of the extension 𝐸 / 𝐾 is a power of 2 , 𝐸 being the composite field 𝐼𝐽. (Contributed by Thierry Arnoux, 19-Oct-2025.)

**Hypotheses**
Ref	Expression
fldextrspun.k	⊢ 𝐾 = (𝐿 ↾_s 𝐹)
fldextrspun.i	⊢ 𝐼 = (𝐿 ↾_s 𝐺)
fldextrspun.j	⊢ 𝐽 = (𝐿 ↾_s 𝐻)
fldextrspun.2	⊢ (𝜑 → 𝐿 ∈ Field)
fldextrspun.3	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
fldextrspun.4	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
fldextrspun.5	⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
fldextrspun.6	⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
fldext2rspun.n	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
fldext2rspun.1	⊢ (𝜑 → (𝐼[:]𝐾) = 2)
fldext2rspun.2	⊢ (𝜑 → (𝐽[:]𝐾) = (2↑𝑁))
fldext2rspun.e	⊢ 𝐸 = (𝐿 ↾_s (𝐿 fldGen (𝐺 ∪ 𝐻)))

**Assertion**
Ref	Expression
fldext2rspun	⊢ (𝜑 → ∃𝑛 ∈ ℕ₀ (𝐸[:]𝐾) = (2↑𝑛))

Distinct variable groups: 𝑛,𝐸 𝑛,𝐾 𝑛,𝑁 𝜑,𝑛 Allowed substitution hints: 𝐹(𝑛) 𝐺(𝑛) 𝐻(𝑛) 𝐼(𝑛) 𝐽(𝑛) 𝐿(𝑛)

**Proof of Theorem fldext2rspun**
Step	Hyp	Ref	Expression
1		eqid 2760	. . . . . 6 ⊢ (Base‘𝐿) = (Base‘𝐿)
2		fldextrspun.i	. . . . . 6 ⊢ 𝐼 = (𝐿 ↾_s 𝐺)
3		fldext2rspun.e	. . . . . 6 ⊢ 𝐸 = (𝐿 ↾_s (𝐿 fldGen (𝐺 ∪ 𝐻)))
4		fldextrspun.2	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ Field)
5		fldextrspun.5	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
6		fldextrspun.6	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
7	1	sdrgss 21050	. . . . . . 7 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
8	6, 7	syl 18	. . . . . 6 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
9	1, 2, 3, 4, 5, 8	fldgenfldext 34300	. . . . 5 ⊢ (𝜑 → 𝐸/_FldExt𝐼)
10		fldextrspun.3	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
11		fldextrspun.k	. . . . . 6 ⊢ 𝐾 = (𝐿 ↾_s 𝐹)
12	2, 4, 5, 10, 11	fldsdrgfldext2 34294	. . . . 5 ⊢ (𝜑 → 𝐼/_FldExt𝐾)
13		extdgmul 34295	. . . . 5 ⊢ ((𝐸/_FldExt𝐼 ∧ 𝐼/_FldExt𝐾) → (𝐸[:]𝐾) = ((𝐸[:]𝐼) ·_e (𝐼[:]𝐾)))
14	9, 12, 13	syl2anc 596	. . . 4 ⊢ (𝜑 → (𝐸[:]𝐾) = ((𝐸[:]𝐼) ·_e (𝐼[:]𝐾)))
15		fldextrspun.j	. . . . . . . . 9 ⊢ 𝐽 = (𝐿 ↾_s 𝐻)
16		fldextrspun.4	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
17		fldext2rspun.2	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽[:]𝐾) = (2↑𝑁))
18		2nn 12416	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ
19	18	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℕ)
20		fldext2rspun.n	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
21	19, 20	nnexpcld 14389	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑𝑁) ∈ ℕ)
22	17, 21	eqeltrd 2860	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ)
23	22	nnnn0d 12667	. . . . . . . . 9 ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ₀)
24		fldext2rspun.1	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼[:]𝐾) = 2)
25	24, 18	eqeltrdi 2868	. . . . . . . . 9 ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ)
26	11, 2, 15, 4, 10, 16, 5, 6, 23, 3, 25	fldextrspundgdvdslem 34312	. . . . . . . 8 ⊢ (𝜑 → (𝐸[:]𝐼) ∈ ℕ₀)
27		elnn0 12608	. . . . . . . 8 ⊢ ((𝐸[:]𝐼) ∈ ℕ₀ ↔ ((𝐸[:]𝐼) ∈ ℕ ∨ (𝐸[:]𝐼) = 0))
28	26, 27	sylib 221	. . . . . . 7 ⊢ (𝜑 → ((𝐸[:]𝐼) ∈ ℕ ∨ (𝐸[:]𝐼) = 0))
29		extdggt0 34289	. . . . . . . . . 10 ⊢ (𝐸/_FldExt𝐼 → 0 < (𝐸[:]𝐼))
30	9, 29	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 0 < (𝐸[:]𝐼))
31	30	gt0ne0d 11880	. . . . . . . 8 ⊢ (𝜑 → (𝐸[:]𝐼) ≠ 0)
32	31	neneqd 2960	. . . . . . 7 ⊢ (𝜑 → ¬ (𝐸[:]𝐼) = 0)
33	28, 32	olcnd 891	. . . . . 6 ⊢ (𝜑 → (𝐸[:]𝐼) ∈ ℕ)
34	33	nnred 12350	. . . . 5 ⊢ (𝜑 → (𝐸[:]𝐼) ∈ ℝ)
35	25	nnred 12350	. . . . 5 ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℝ)
36		rexmul 13401	. . . . 5 ⊢ (((𝐸[:]𝐼) ∈ ℝ ∧ (𝐼[:]𝐾) ∈ ℝ) → ((𝐸[:]𝐼) ·_e (𝐼[:]𝐾)) = ((𝐸[:]𝐼) · (𝐼[:]𝐾)))
37	34, 35, 36	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝐸[:]𝐼) ·_e (𝐼[:]𝐾)) = ((𝐸[:]𝐼) · (𝐼[:]𝐾)))
38	14, 37	eqtrd 2795	. . 3 ⊢ (𝜑 → (𝐸[:]𝐾) = ((𝐸[:]𝐼) · (𝐼[:]𝐾)))
39	33, 25	nnmulcld 12391	. . 3 ⊢ (𝜑 → ((𝐸[:]𝐼) · (𝐼[:]𝐾)) ∈ ℕ)
40	38, 39	eqeltrd 2860	. 2 ⊢ (𝜑 → (𝐸[:]𝐾) ∈ ℕ)
41		2nn0 12623	. . . . 5 ⊢ 2 ∈ ℕ₀
42	24, 41	eqeltrdi 2868	. . . 4 ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ₀)
43		uncom 4157	. . . . . . 7 ⊢ (𝐺 ∪ 𝐻) = (𝐻 ∪ 𝐺)
44	43	oveq2i 7431	. . . . . 6 ⊢ (𝐿 fldGen (𝐺 ∪ 𝐻)) = (𝐿 fldGen (𝐻 ∪ 𝐺))
45	44	oveq2i 7431	. . . . 5 ⊢ (𝐿 ↾_s (𝐿 fldGen (𝐺 ∪ 𝐻))) = (𝐿 ↾_s (𝐿 fldGen (𝐻 ∪ 𝐺)))
46	3, 45	eqtri 2783	. . . 4 ⊢ 𝐸 = (𝐿 ↾_s (𝐿 fldGen (𝐻 ∪ 𝐺)))
47	11, 15, 2, 4, 16, 10, 6, 5, 42, 46, 22	fldextrspundgdvds 34313	. . 3 ⊢ (𝜑 → (𝐽[:]𝐾) ∥ (𝐸[:]𝐾))
48	17, 47	eqbrtrrd 5128	. 2 ⊢ (𝜑 → (2↑𝑁) ∥ (𝐸[:]𝐾))
49	11, 2, 15, 4, 10, 16, 5, 6, 23, 3	fldextrspundglemul 34311	. . 3 ⊢ (𝜑 → (𝐸[:]𝐾) ≤ ((𝐼[:]𝐾) ·_e (𝐽[:]𝐾)))
50	22	nnred 12350	. . . . 5 ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℝ)
51		rexmul 13401	. . . . 5 ⊢ (((𝐼[:]𝐾) ∈ ℝ ∧ (𝐽[:]𝐾) ∈ ℝ) → ((𝐼[:]𝐾) ·_e (𝐽[:]𝐾)) = ((𝐼[:]𝐾) · (𝐽[:]𝐾)))
52	35, 50, 51	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝐼[:]𝐾) ·_e (𝐽[:]𝐾)) = ((𝐼[:]𝐾) · (𝐽[:]𝐾)))
53	24, 17	oveq12d 7438	. . . 4 ⊢ (𝜑 → ((𝐼[:]𝐾) · (𝐽[:]𝐾)) = (2 · (2↑𝑁)))
54		2cnd 12421	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
55	54, 20	expcld 14289	. . . . . 6 ⊢ (𝜑 → (2↑𝑁) ∈ ℂ)
56	54, 55	mulcomd 11330	. . . . 5 ⊢ (𝜑 → (2 · (2↑𝑁)) = ((2↑𝑁) · 2))
57	54, 20	expp1d 14290	. . . . 5 ⊢ (𝜑 → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2))
58	56, 57	eqtr4d 2798	. . . 4 ⊢ (𝜑 → (2 · (2↑𝑁)) = (2↑(𝑁 + 1)))
59	52, 53, 58	3eqtrd 2799	. . 3 ⊢ (𝜑 → ((𝐼[:]𝐾) ·_e (𝐽[:]𝐾)) = (2↑(𝑁 + 1)))
60	49, 59	breqtrd 5130	. 2 ⊢ (𝜑 → (𝐸[:]𝐾) ≤ (2↑(𝑁 + 1)))
61	40, 20, 48, 60	2exple2exp 33425	1 ⊢ (𝜑 → ∃𝑛 ∈ ℕ₀ (𝐸[:]𝐾) = (2↑𝑛))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∨ wo 861 = wceq 1569 ∈ wcel 2144 ∃wrex 3086 ⊆ wss 3895 ∪ cun 4149 class class class wbr 5102 ‘cfv 6538 (class class class)co 7420 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 < clt 11343 ≤ cle 11344 ℕcn 12335 2c2 12397 ℕ₀cn0 12606 ·_e cxmu 13240 ↑cexp 14204 ∥ cdvds 16422 Basecbs 17387 ↾_s cress 17408 Fieldcfield 20981 SubDRingcsdrg 21043 fldGen cfldgen 33872 /_FldExtcfldext 34270 [:]cextdg 34272

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-reg 9586 ax-inf2 9642 ax-ac2 10541 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278 ax-addf 11279

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-rpss 7739 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-tpos 8243 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-oadd 8480 df-er 8717 df-map 8849 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fsupp 9354 df-sup 9434 df-inf 9435 df-oi 9504 df-r1 9768 df-rank 9769 df-scott 9929 df-dju 9982 df-card 10020 df-acn 10023 df-ac 10195 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-ind 12321 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-xnn0 12680 df-z 12694 df-dec 12815 df-uz 12966 df-rp 13121 df-xneg 13241 df-xadd 13242 df-xmul 13243 df-icc 13483 df-fz 13640 df-fzo 13789 df-seq 14145 df-exp 14205 df-hash 14475 df-word 14659 df-lsw 14708 df-concat 14716 df-s1 14743 df-substr 14789 df-pfx 14821 df-s2 14999 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-clim 15655 df-sum 15854 df-dvds 16423 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-starv 17443 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ocomp 17449 df-ds 17450 df-unif 17451 df-hom 17452 df-cco 17453 df-0g 17612 df-gsum 17613 df-prds 17618 df-pws 17620 df-mre 17756 df-mrc 17757 df-mri 17758 df-acs 17759 df-proset 18468 df-drs 18469 df-poset 18487 df-ipo 18702 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-mhm 18978 df-submnd 18979 df-grp 19147 df-minusg 19148 df-sbg 19149 df-mulg 19278 df-subg 19333 df-ghm 19428 df-cntz 19531 df-cntr 19532 df-lsm 19850 df-cmn 19996 df-abl 19997 df-mgp 20361 df-rng 20375 df-ur 20408 df-ring 20461 df-cring 20462 df-oppr 20567 df-dvdsr 20587 df-unit 20588 df-invr 20618 df-dvr 20631 df-nzr 20763 df-subrng 20798 df-subrg 20822 df-rgspn 20863 df-rlreg 20946 df-domn 20947 df-idom 20948 df-drng 20982 df-field 20983 df-sdrg 21044 df-lmod 21137 df-lss 21207 df-lsp 21247 df-lmhm 21297 df-lmim 21298 df-lbs 21350 df-lvec 21378 df-sra 21448 df-rgmod 21449 df-cnfld 21679 df-zring 21753 df-dsmm 22038 df-frlm 22053 df-uvc 22089 df-lindf 22112 df-linds 22113 df-assa 22161 df-fldgen 33873 df-dim 34232 df-fldext 34273 df-extdg 34274

This theorem is used by: (None)

W3C validator