fldextrspunlem2 - Mathbox for Thierry Arnoux

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

Theorem fldextrspunlem2 34357

Description: 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	⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ₀)
fldextrspunfld.n	⊢ 𝑁 = (RingSpan‘𝐿)
fldextrspunfld.c	⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))
fldextrspunfld.e	⊢ 𝐸 = (𝐿 ↾_s 𝐶)

**Assertion**
Ref	Expression
fldextrspunlem2	⊢ (𝜑 → 𝐶 = (𝐿 fldGen (𝐺 ∪ 𝐻)))

**Proof of Theorem fldextrspunlem2**
Step	Hyp	Ref	Expression
1		fldextrspunfld.2	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ Field)
2	1	flddrngd 21001	. . . 4 ⊢ (𝜑 → 𝐿 ∈ DivRing)
3	2	drngringd 20995	. . 3 ⊢ (𝜑 → 𝐿 ∈ Ring)
4		eqidd 2761	. . 3 ⊢ (𝜑 → (Base‘𝐿) = (Base‘𝐿))
5		fldextrspunfld.5	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
6		eqid 2760	. . . . . 6 ⊢ (Base‘𝐿) = (Base‘𝐿)
7	6	sdrgss 21057	. . . . 5 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
8	5, 7	syl 18	. . . 4 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
9		fldextrspunfld.6	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
10	6	sdrgss 21057	. . . . 5 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
11	9, 10	syl 18	. . . 4 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
12	8, 11	unssd 4189	. . 3 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ (Base‘𝐿))
13		fldextrspunfld.n	. . . 4 ⊢ 𝑁 = (RingSpan‘𝐿)
14	13	a1i 11	. . 3 ⊢ (𝜑 → 𝑁 = (RingSpan‘𝐿))
15		fldextrspunfld.c	. . . 4 ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))
16	15	a1i 11	. . 3 ⊢ (𝜑 → 𝐶 = (𝑁‘(𝐺 ∪ 𝐻)))
17	6, 2, 12	fldgensdrg 33924	. . . 4 ⊢ (𝜑 → (𝐿 fldGen (𝐺 ∪ 𝐻)) ∈ (SubDRing‘𝐿))
18		sdrgsubrg 21055	. . . 4 ⊢ ((𝐿 fldGen (𝐺 ∪ 𝐻)) ∈ (SubDRing‘𝐿) → (𝐿 fldGen (𝐺 ∪ 𝐻)) ∈ (SubRing‘𝐿))
19	17, 18	syl 18	. . 3 ⊢ (𝜑 → (𝐿 fldGen (𝐺 ∪ 𝐻)) ∈ (SubRing‘𝐿))
20	6, 2, 12	fldgenssid 33923	. . 3 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ (𝐿 fldGen (𝐺 ∪ 𝐻)))
21	3, 4, 12, 14, 16, 19, 20	rgspnmin 20874	. 2 ⊢ (𝜑 → 𝐶 ⊆ (𝐿 fldGen (𝐺 ∪ 𝐻)))
22	3, 4, 12, 14, 16	rgspncl 20872	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝐿))
23		fldextrspunfld.e	. . . . 5 ⊢ 𝐸 = (𝐿 ↾_s 𝐶)
24		fldextrspunfld.k	. . . . . . 7 ⊢ 𝐾 = (𝐿 ↾_s 𝐹)
25		fldextrspunfld.i	. . . . . . 7 ⊢ 𝐼 = (𝐿 ↾_s 𝐺)
26		fldextrspunfld.j	. . . . . . 7 ⊢ 𝐽 = (𝐿 ↾_s 𝐻)
27		fldextrspunfld.3	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
28		fldextrspunfld.4	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
29		fldextrspunfld.7	. . . . . . 7 ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ₀)
30	24, 25, 26, 1, 27, 28, 5, 9, 29, 13, 15, 23	fldextrspunfld 34356	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ Field)
31	30	flddrngd 21001	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ DivRing)
32	23, 31	eqeltrrid 2865	. . . 4 ⊢ (𝜑 → (𝐿 ↾_s 𝐶) ∈ DivRing)
33		issdrg 21052	. . . 4 ⊢ (𝐶 ∈ (SubDRing‘𝐿) ↔ (𝐿 ∈ DivRing ∧ 𝐶 ∈ (SubRing‘𝐿) ∧ (𝐿 ↾_s 𝐶) ∈ DivRing))
34	2, 22, 32, 33	syl3anbrc 1362	. . 3 ⊢ (𝜑 → 𝐶 ∈ (SubDRing‘𝐿))
35	3, 4, 12, 14, 16	rgspnssid 20873	. . 3 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ 𝐶)
36	6, 2, 34, 35	fldgenssp 33928	. 2 ⊢ (𝜑 → (𝐿 fldGen (𝐺 ∪ 𝐻)) ⊆ 𝐶)
37	21, 36	eqssd 3926	1 ⊢ (𝜑 → 𝐶 = (𝐿 fldGen (𝐺 ∪ 𝐻)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1569 ∈ wcel 2144 ⊆ wss 3896 ∪ cun 4148 ‘cfv 6541 (class class class)co 7422 ℕ₀cn0 12611 Basecbs 17394 ↾_s cress 17415 SubRingcsubrg 20828 RingSpancrgspn 20869 DivRingcdr 20987 Fieldcfield 20988 SubDRingcsdrg 21050 fldGen cfldgen 33920 [:]cextdg 34320

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 7753 ax-inf2 9647 ax-ac2 10546 ax-cnex 11261 ax-resscn 11262 ax-1cn 11263 ax-icn 11264 ax-addcl 11265 ax-addrcl 11266 ax-mulcl 11267 ax-mulrcl 11268 ax-mulcom 11269 ax-addass 11270 ax-mulass 11271 ax-distr 11272 ax-i2m1 11273 ax-1ne0 11274 ax-1rid 11275 ax-rnegex 11276 ax-rrecex 11277 ax-cnre 11278 ax-pre-lttri 11279 ax-pre-lttrn 11280 ax-pre-ltadd 11281 ax-pre-mulgt0 11282 ax-pre-sup 11283 ax-addf 11284

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 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 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 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 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 7379 df-ov 7425 df-oprab 7426 df-mpo 7427 df-of 7695 df-rpss 7741 df-om 7880 df-1st 8003 df-2nd 8004 df-supp 8182 df-tpos 8248 df-frecs 8304 df-wrecs 8335 df-recs 8384 df-rdg 8423 df-1o 8481 df-2o 8482 df-oadd 8485 df-er 8722 df-map 8854 df-ixp 8931 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-fsupp 9359 df-sup 9439 df-inf 9440 df-oi 9509 df-dju 9987 df-card 10025 df-acn 10028 df-ac 10200 df-pnf 11350 df-mnf 11351 df-xr 11352 df-ltxr 11353 df-le 11354 df-sub 11548 df-neg 11549 df-div 11979 df-ind 12326 df-nn 12341 df-2 12410 df-3 12411 df-4 12412 df-5 12413 df-6 12414 df-7 12415 df-8 12416 df-9 12417 df-n0 12612 df-xnn0 12685 df-z 12699 df-dec 12820 df-uz 12971 df-rp 13126 df-xadd 13247 df-fz 13645 df-fzo 13794 df-seq 14150 df-exp 14210 df-hash 14480 df-word 14664 df-lsw 14713 df-concat 14721 df-s1 14748 df-substr 14795 df-pfx 14827 df-s2 15005 df-cj 15273 df-re 15274 df-im 15275 df-sqrt 15409 df-abs 15410 df-clim 15662 df-sum 15861 df-struct 17332 df-sets 17349 df-slot 17367 df-ndx 17379 df-base 17395 df-ress 17416 df-plusg 17448 df-mulr 17449 df-starv 17450 df-sca 17451 df-vsca 17452 df-ip 17453 df-tset 17454 df-ple 17455 df-ocomp 17456 df-ds 17457 df-unif 17458 df-hom 17459 df-cco 17460 df-0g 17619 df-gsum 17620 df-prds 17625 df-pws 17627 df-mre 17763 df-mrc 17764 df-mri 17765 df-acs 17766 df-proset 18475 df-drs 18476 df-poset 18494 df-ipo 18709 df-mgm 18823 df-sgrp 18915 df-mnd 18931 df-mhm 18985 df-submnd 18986 df-grp 19154 df-minusg 19155 df-sbg 19156 df-mulg 19285 df-subg 19340 df-ghm 19435 df-cntz 19538 df-cntr 19539 df-lsm 19857 df-cmn 20003 df-abl 20004 df-mgp 20368 df-rng 20382 df-ur 20415 df-ring 20468 df-cring 20469 df-oppr 20574 df-dvdsr 20594 df-unit 20595 df-invr 20625 df-dvr 20638 df-nzr 20770 df-subrng 20805 df-subrg 20829 df-rgspn 20870 df-rlreg 20953 df-domn 20954 df-idom 20955 df-drng 20989 df-field 20990 df-sdrg 21051 df-lmod 21144 df-lss 21214 df-lsp 21254 df-lmhm 21304 df-lmim 21305 df-lbs 21357 df-lvec 21385 df-sra 21455 df-rgmod 21456 df-cnfld 21686 df-zring 21760 df-dsmm 22045 df-frlm 22060 df-uvc 22096 df-lindf 22119 df-linds 22120 df-assa 22168 df-fldgen 33921 df-dim 34280 df-fldext 34321 df-extdg 34322

This theorem is used by: fldextrspundgle 34358 fldextrspundgdvdslem 34360 fldextrspundgdvds 34361

W3C validator