fldextrspunlem1 - Mathbox for Thierry Arnoux

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

Theorem fldextrspunlem1 33677

Description: Lemma for fldextrspunfld 33678. 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
fldextrspunlem1	⊢ (𝜑 → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))

Proof of Theorem fldextrspunlem1 Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fldextrspunfld.6	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
2		fldextrspunfld.j	. . . . . 6 ⊢ 𝐽 = (𝐿 ↾_s 𝐻)
3	2	sdrgdrng 20706	. . . . 5 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐽 ∈ DivRing)
4	1, 3	syl 17	. . . 4 ⊢ (𝜑 → 𝐽 ∈ DivRing)
5		fldextrspunfld.4	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
6		eqid 2730	. . . . . 6 ⊢ (𝐽 ↾_s 𝐹) = (𝐽 ↾_s 𝐹)
7	6	sdrgdrng 20706	. . . . 5 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → (𝐽 ↾_s 𝐹) ∈ DivRing)
8	5, 7	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) ∈ DivRing)
9		sdrgsubrg 20707	. . . . . 6 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
10	1, 9	syl 17	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
11		fldextrspunfld.5	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
12		sdrgsubrg 20707	. . . . . . . 8 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
13	11, 12	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
14		fldextrspunfld.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
15		sdrgsubrg 20707	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐼) → 𝐹 ∈ (SubRing‘𝐼))
16	14, 15	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐼))
17		fldextrspunfld.i	. . . . . . . . 9 ⊢ 𝐼 = (𝐿 ↾_s 𝐺)
18	17	subsubrg 20514	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐿) → (𝐹 ∈ (SubRing‘𝐼) ↔ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺)))
19	18	biimpa 476	. . . . . . 7 ⊢ ((𝐺 ∈ (SubRing‘𝐿) ∧ 𝐹 ∈ (SubRing‘𝐼)) → (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺))
20	13, 16, 19	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺))
21	20	simpld 494	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿))
22		eqid 2730	. . . . . . . 8 ⊢ (Base‘𝐽) = (Base‘𝐽)
23	22	sdrgss 20709	. . . . . . 7 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
24	5, 23	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
25		eqid 2730	. . . . . . . . 9 ⊢ (Base‘𝐿) = (Base‘𝐿)
26	25	sdrgss 20709	. . . . . . . 8 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
27	1, 26	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
28	2, 25	ressbas2 17215	. . . . . . 7 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
29	27, 28	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
30	24, 29	sseqtrrd 3987	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ 𝐻)
31	2	subsubrg 20514	. . . . . 6 ⊢ (𝐻 ∈ (SubRing‘𝐿) → (𝐹 ∈ (SubRing‘𝐽) ↔ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐻)))
32	31	biimpar 477	. . . . 5 ⊢ ((𝐻 ∈ (SubRing‘𝐿) ∧ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐻)) → 𝐹 ∈ (SubRing‘𝐽))
33	10, 21, 30, 32	syl12anc 836	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐽))
34		eqid 2730	. . . . 5 ⊢ ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹)
35	34, 6	sralvec 33588	. . . 4 ⊢ ((𝐽 ∈ DivRing ∧ (𝐽 ↾_s 𝐹) ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐽)) → ((subringAlg ‘𝐽)‘𝐹) ∈ LVec)
36	4, 8, 33, 35	syl3anc 1373	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ LVec)
37		eqid 2730	. . . 4 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
38	37	lbsex 21082	. . 3 ⊢ (((subringAlg ‘𝐽)‘𝐹) ∈ LVec → (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ≠ ∅)
39	36, 38	syl 17	. 2 ⊢ (𝜑 → (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ≠ ∅)
40		fldextrspunfld.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ Field)
41		fldidom 20687	. . . . . . . . . . . 12 ⊢ (𝐿 ∈ Field → 𝐿 ∈ IDomn)
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ IDomn)
43	42	idomringd 20644	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ Ring)
44		eqidd 2731	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐿) = (Base‘𝐿))
45	25	sdrgss 20709	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
46	11, 45	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
47	46, 27	unssd 4158	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ (Base‘𝐿))
48		fldextrspunfld.n	. . . . . . . . . . 11 ⊢ 𝑁 = (RingSpan‘𝐿)
49	48	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 = (RingSpan‘𝐿))
50		fldextrspunfld.c	. . . . . . . . . . 11 ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))
51	50	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 = (𝑁‘(𝐺 ∪ 𝐻)))
52	43, 44, 47, 49, 51	rgspncl 20529	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝐿))
53	43, 44, 47, 49, 51	rgspnssid 20530	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ 𝐶)
54	53	unssad 4159	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ⊆ 𝐶)
55		fldextrspunfld.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐿 ↾_s 𝐶)
56	55	subsubrg 20514	. . . . . . . . . 10 ⊢ (𝐶 ∈ (SubRing‘𝐿) → (𝐺 ∈ (SubRing‘𝐸) ↔ (𝐺 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶)))
57	56	biimpar 477	. . . . . . . . 9 ⊢ ((𝐶 ∈ (SubRing‘𝐿) ∧ (𝐺 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶)) → 𝐺 ∈ (SubRing‘𝐸))
58	52, 13, 54, 57	syl12anc 836	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐸))
59		eqid 2730	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺)
60	59	sralmod 21101	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐸) → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
61	58, 60	syl 17	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
62		ressabs 17225	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶) → ((𝐿 ↾_s 𝐶) ↾_s 𝐺) = (𝐿 ↾_s 𝐺))
63	52, 54, 62	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 ↾_s 𝐶) ↾_s 𝐺) = (𝐿 ↾_s 𝐺))
64	55	oveq1i 7400	. . . . . . . . . 10 ⊢ (𝐸 ↾_s 𝐺) = ((𝐿 ↾_s 𝐶) ↾_s 𝐺)
65	63, 64, 17	3eqtr4g 2790	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s 𝐺) = 𝐼)
66		eqidd 2731	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺))
67	25	subrgss 20488	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ (SubRing‘𝐿) → 𝐶 ⊆ (Base‘𝐿))
68	52, 67	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ⊆ (Base‘𝐿))
69	55, 25	ressbas2 17215	. . . . . . . . . . . . 13 ⊢ (𝐶 ⊆ (Base‘𝐿) → 𝐶 = (Base‘𝐸))
70	68, 69	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 = (Base‘𝐸))
71	53, 70	sseqtrd 3986	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ (Base‘𝐸))
72	71	unssad 4159	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐸))
73	66, 72	srasca 21094	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s 𝐺) = (Scalar‘((subringAlg ‘𝐸)‘𝐺)))
74	65, 73	eqtr3d 2767	. . . . . . . 8 ⊢ (𝜑 → 𝐼 = (Scalar‘((subringAlg ‘𝐸)‘𝐺)))
75	17	sdrgdrng 20706	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐼 ∈ DivRing)
76	11, 75	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ DivRing)
77	74, 76	eqeltrrd 2830	. . . . . . 7 ⊢ (𝜑 → (Scalar‘((subringAlg ‘𝐸)‘𝐺)) ∈ DivRing)
78		eqid 2730	. . . . . . . 8 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐺)) = (Scalar‘((subringAlg ‘𝐸)‘𝐺))
79	78	islvec 21018	. . . . . . 7 ⊢ (((subringAlg ‘𝐸)‘𝐺) ∈ LVec ↔ (((subringAlg ‘𝐸)‘𝐺) ∈ LMod ∧ (Scalar‘((subringAlg ‘𝐸)‘𝐺)) ∈ DivRing))
80	61, 77, 79	sylanbrc 583	. . . . . 6 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) ∈ LVec)
81		eqid 2730	. . . . . . 7 ⊢ (LBasis‘((subringAlg ‘𝐸)‘𝐺)) = (LBasis‘((subringAlg ‘𝐸)‘𝐺))
82	81	lbsex 21082	. . . . . 6 ⊢ (((subringAlg ‘𝐸)‘𝐺) ∈ LVec → (LBasis‘((subringAlg ‘𝐸)‘𝐺)) ≠ ∅)
83	80, 82	syl 17	. . . . 5 ⊢ (𝜑 → (LBasis‘((subringAlg ‘𝐸)‘𝐺)) ≠ ∅)
84	83	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (LBasis‘((subringAlg ‘𝐸)‘𝐺)) ≠ ∅)
85	80	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) ∈ LVec)
86		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺)))
87	81	dimval 33603	. . . . . 6 ⊢ ((((subringAlg ‘𝐸)‘𝐺) ∈ LVec ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) = (♯‘𝑐))
88	85, 86, 87	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) = (♯‘𝑐))
89		eqid 2730	. . . . . 6 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐺)) = (Base‘((subringAlg ‘𝐸)‘𝐺))
90		eqid 2730	. . . . . 6 ⊢ (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘((subringAlg ‘𝐸)‘𝐺))
91		eqid 2730	. . . . . . . . . . . 12 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
92	91, 37	lbsss 20991	. . . . . . . . . . 11 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
93	92	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
94		eqidd 2731	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
95	94, 24	srabase 21091	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
96	29, 95	eqtrd 2765	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
97	96	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
98	93, 97	sseqtrrd 3987	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ 𝐻)
99	53	unssbd 4160	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ⊆ 𝐶)
100	99	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐻 ⊆ 𝐶)
101	98, 100	sstrd 3960	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ 𝐶)
102	70	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐶 = (Base‘𝐸))
103	101, 102	sseqtrd 3986	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘𝐸))
104		eqidd 2731	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺))
105	72	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐺 ⊆ (Base‘𝐸))
106	104, 105	srabase 21091	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘𝐺)))
107	103, 106	sseqtrd 3986	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
108	61	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
109	89, 90	lspssv 20896	. . . . . . . 8 ⊢ ((((subringAlg ‘𝐸)‘𝐺) ∈ LMod ∧ 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
110	108, 107, 109	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
111		fldextrspunfld.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (𝐿 ↾_s 𝐹)
112	40	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐿 ∈ Field)
113	14	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐹 ∈ (SubDRing‘𝐼))
114	5	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐹 ∈ (SubDRing‘𝐽))
115	11	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐺 ∈ (SubDRing‘𝐿))
116	1	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ∈ (SubDRing‘𝐿))
117		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
118		fldsdrgfld 20714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐿 ∈ Field ∧ 𝐻 ∈ (SubDRing‘𝐿)) → (𝐿 ↾_s 𝐻) ∈ Field)
119	40, 1, 118	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 ↾_s 𝐻) ∈ Field)
120	2, 119	eqeltrid 2833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ Field)
121		ressabs 17225	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐻 ∈ (SubDRing‘𝐿) ∧ 𝐹 ⊆ 𝐻) → ((𝐿 ↾_s 𝐻) ↾_s 𝐹) = (𝐿 ↾_s 𝐹))
122	1, 30, 121	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐿 ↾_s 𝐻) ↾_s 𝐹) = (𝐿 ↾_s 𝐹))
123	2	oveq1i 7400	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ↾_s 𝐹) = ((𝐿 ↾_s 𝐻) ↾_s 𝐹)
124	122, 123, 111	3eqtr4g 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) = 𝐾)
125		fldsdrgfld 20714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐽)) → (𝐽 ↾_s 𝐹) ∈ Field)
126	120, 5, 125	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) ∈ Field)
127	124, 126	eqeltrrd 2830	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ Field)
128	30, 27	sstrd 3960	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
129	111, 25	ressbas2 17215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ⊆ (Base‘𝐿) → 𝐹 = (Base‘𝐾))
130	128, 129	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
131	130	oveq2d 7406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) = (𝐽 ↾_s (Base‘𝐾)))
132	124, 131	eqtr3d 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (𝐽 ↾_s (Base‘𝐾)))
133	130, 33	eqeltrrd 2830	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐽))
134		brfldext 33648	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ Field ∧ 𝐾 ∈ Field) → (𝐽/_FldExt𝐾 ↔ (𝐾 = (𝐽 ↾_s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐽))))
135	134	biimpar 477	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Field ∧ 𝐾 ∈ Field) ∧ (𝐾 = (𝐽 ↾_s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐽))) → 𝐽/_FldExt𝐾)
136	120, 127, 132, 133, 135	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐽/_FldExt𝐾)
137	136	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐽/_FldExt𝐾)
138		extdgval 33656	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽/_FldExt𝐾 → (𝐽[:]𝐾) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
139	137, 138	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
140	130	fveq2d 6865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘(Base‘𝐾)))
141	140	fveq2d 6865	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
142	141	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
143	37	dimval 33603	. . . . . . . . . . . . . . . . 17 ⊢ ((((subringAlg ‘𝐽)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (♯‘𝑏))
144	36, 143	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (♯‘𝑏))
145	139, 142, 144	3eqtr2d 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) = (♯‘𝑏))
146		fldextrspunfld.7	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ₀)
147	146	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) ∈ ℕ₀)
148	145, 147	eqeltrrd 2830	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (♯‘𝑏) ∈ ℕ₀)
149		hashclb 14330	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → (𝑏 ∈ Fin ↔ (♯‘𝑏) ∈ ℕ₀))
150	149	biimpar 477	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ∧ (♯‘𝑏) ∈ ℕ₀) → 𝑏 ∈ Fin)
151	117, 148, 150	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ∈ Fin)
152	111, 17, 2, 112, 113, 114, 115, 116, 48, 50, 55, 117, 151	fldextrspunlsp 33676	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
153	152	eqimssd 4006	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
154	25, 55, 68, 54, 40	resssra 33590	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) = (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))
155	154	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)))
156	155	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)))
157	156	fveq1d 6863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) = ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏))
158	115, 12	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐺 ∈ (SubRing‘𝐿))
159		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺)
160	159	sralmod 21101	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ (SubRing‘𝐿) → ((subringAlg ‘𝐿)‘𝐺) ∈ LMod)
161	158, 160	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((subringAlg ‘𝐿)‘𝐺) ∈ LMod)
162	117, 92	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
163	96	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
164	162, 163	sseqtrrd 3987	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ 𝐻)
165	116, 26	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ⊆ (Base‘𝐿))
166	164, 165	sstrd 3960	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘𝐿))
167		eqidd 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺))
168	167, 46	srabase 21091	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
169	168	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
170	166, 169	sseqtrd 3986	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺)))
171		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (Base‘((subringAlg ‘𝐿)‘𝐺)) = (Base‘((subringAlg ‘𝐿)‘𝐺))
172		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)) = (LSubSp‘((subringAlg ‘𝐿)‘𝐺))
173		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (LSpan‘((subringAlg ‘𝐿)‘𝐺)) = (LSpan‘((subringAlg ‘𝐿)‘𝐺))
174	171, 172, 173	lspcl 20889	. . . . . . . . . . . . . . 15 ⊢ ((((subringAlg ‘𝐿)‘𝐺) ∈ LMod ∧ 𝑏 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
175	161, 170, 174	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
176	152, 175	eqeltrd 2829	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
177	99	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ⊆ 𝐶)
178	164, 177	sstrd 3960	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ 𝐶)
179		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶) = (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)
180		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))
181	179, 173, 180, 172	lsslsp 20928	. . . . . . . . . . . . 13 ⊢ ((((subringAlg ‘𝐿)‘𝐺) ∈ LMod ∧ 𝐶 ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)) ∧ 𝑏 ⊆ 𝐶) → ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏) = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
182	161, 176, 178, 181	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏) = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
183	157, 182	eqtr2d 2766	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) = ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
184	153, 183	sseqtrd 3986	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
185	184	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
186	102, 185	eqsstrrd 3985	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘𝐸) ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
187	106, 186	eqsstrrd 3985	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘((subringAlg ‘𝐸)‘𝐺)) ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
188	110, 187	eqssd 3967	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) = (Base‘((subringAlg ‘𝐸)‘𝐺)))
189	89, 81, 90, 85, 86, 107, 188	lbslelsp 33600	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (♯‘𝑐) ≤ (♯‘𝑏))
190	88, 189	eqbrtrd 5132	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (♯‘𝑏))
191	84, 190	n0limd 32408	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (♯‘𝑏))
192	191, 145	breqtrrd 5138	. 2 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))
193	39, 192	n0limd 32408	1 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2926 ∪ cun 3915 ⊆ wss 3917 ∅c0 4299 class class class wbr 5110 ‘cfv 6514 (class class class)co 7390 Fincfn 8921 ≤ cle 11216 ℕ₀cn0 12449 ♯chash 14302 Basecbs 17186 ↾_s cress 17207 Scalarcsca 17230 SubRingcsubrg 20485 RingSpancrgspn 20526 IDomncidom 20609 DivRingcdr 20645 Fieldcfield 20646 SubDRingcsdrg 20702 LModclmod 20773 LSubSpclss 20844 LSpanclspn 20884 LBasisclbs 20988 LVecclvec 21016 subringAlg csra 21085 dimcldim 33601 /_FldExtcfldext 33641 [:]cextdg 33643

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-reg 9552 ax-inf2 9601 ax-ac2 10423 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153 ax-addf 11154

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-iin 4961 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7656 df-rpss 7702 df-om 7846 df-1st 7971 df-2nd 7972 df-supp 8143 df-tpos 8208 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-er 8674 df-map 8804 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9320 df-sup 9400 df-inf 9401 df-oi 9470 df-r1 9724 df-rank 9725 df-dju 9861 df-card 9899 df-acn 9902 df-ac 10076 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-4 12258 df-5 12259 df-6 12260 df-7 12261 df-8 12262 df-9 12263 df-n0 12450 df-xnn0 12523 df-z 12537 df-dec 12657 df-uz 12801 df-rp 12959 df-fz 13476 df-fzo 13623 df-seq 13974 df-exp 14034 df-hash 14303 df-word 14486 df-lsw 14535 df-concat 14543 df-s1 14568 df-substr 14613 df-pfx 14643 df-s2 14821 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-clim 15461 df-sum 15660 df-struct 17124 df-sets 17141 df-slot 17159 df-ndx 17171 df-base 17187 df-ress 17208 df-plusg 17240 df-mulr 17241 df-starv 17242 df-sca 17243 df-vsca 17244 df-ip 17245 df-tset 17246 df-ple 17247 df-ocomp 17248 df-ds 17249 df-unif 17250 df-hom 17251 df-cco 17252 df-0g 17411 df-gsum 17412 df-prds 17417 df-pws 17419 df-mre 17554 df-mrc 17555 df-mri 17556 df-acs 17557 df-proset 18262 df-drs 18263 df-poset 18281 df-ipo 18494 df-mgm 18574 df-sgrp 18653 df-mnd 18669 df-mhm 18717 df-submnd 18718 df-grp 18875 df-minusg 18876 df-sbg 18877 df-mulg 19007 df-subg 19062 df-ghm 19152 df-cntz 19256 df-cmn 19719 df-abl 19720 df-mgp 20057 df-rng 20069 df-ur 20098 df-ring 20151 df-cring 20152 df-oppr 20253 df-dvdsr 20273 df-unit 20274 df-invr 20304 df-nzr 20429 df-subrng 20462 df-subrg 20486 df-rgspn 20527 df-rlreg 20610 df-domn 20611 df-idom 20612 df-drng 20647 df-field 20648 df-sdrg 20703 df-lmod 20775 df-lss 20845 df-lsp 20885 df-lmhm 20936 df-lbs 20989 df-lvec 21017 df-sra 21087 df-rgmod 21088 df-cnfld 21272 df-zring 21364 df-dsmm 21648 df-frlm 21663 df-uvc 21699 df-ind 32781 df-dim 33602 df-fldext 33644 df-extdg 33645

This theorem is referenced by: fldextrspunfld 33678 fldextrspundgle 33680

W3C validator