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 33643

Description: Lemma for fldextrspunfld 33644. 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 20675	. . . . 5 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐽 ∈ DivRing)
4	1, 3	syl 17	. . . 4 ⊢ (𝜑 → 𝐽 ∈ DivRing)
5		fldextrspunfld.4	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
6		eqid 2729	. . . . . 6 ⊢ (𝐽 ↾_s 𝐹) = (𝐽 ↾_s 𝐹)
7	6	sdrgdrng 20675	. . . . 5 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → (𝐽 ↾_s 𝐹) ∈ DivRing)
8	5, 7	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) ∈ DivRing)
9		sdrgsubrg 20676	. . . . . 6 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
10	1, 9	syl 17	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
11		fldextrspunfld.5	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
12		sdrgsubrg 20676	. . . . . . . 8 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
13	11, 12	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
14		fldextrspunfld.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
15		sdrgsubrg 20676	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐼) → 𝐹 ∈ (SubRing‘𝐼))
16	14, 15	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐼))
17		fldextrspunfld.i	. . . . . . . . 9 ⊢ 𝐼 = (𝐿 ↾_s 𝐺)
18	17	subsubrg 20483	. . . . . . . 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 2729	. . . . . . . 8 ⊢ (Base‘𝐽) = (Base‘𝐽)
23	22	sdrgss 20678	. . . . . . 7 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
24	5, 23	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
25		eqid 2729	. . . . . . . . 9 ⊢ (Base‘𝐿) = (Base‘𝐿)
26	25	sdrgss 20678	. . . . . . . 8 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
27	1, 26	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
28	2, 25	ressbas2 17184	. . . . . . 7 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
29	27, 28	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
30	24, 29	sseqtrrd 3981	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ 𝐻)
31	2	subsubrg 20483	. . . . . 6 ⊢ (𝐻 ∈ (SubRing‘𝐿) → (𝐹 ∈ (SubRing‘𝐽) ↔ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐻)))
32	31	biimpar 477	. . . . 5 ⊢ ((𝐻 ∈ (SubRing‘𝐿) ∧ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐻)) → 𝐹 ∈ (SubRing‘𝐽))
33	10, 21, 30, 32	syl12anc 836	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐽))
34		eqid 2729	. . . . 5 ⊢ ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹)
35	34, 6	sralvec 33554	. . . 4 ⊢ ((𝐽 ∈ DivRing ∧ (𝐽 ↾_s 𝐹) ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐽)) → ((subringAlg ‘𝐽)‘𝐹) ∈ LVec)
36	4, 8, 33, 35	syl3anc 1373	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ LVec)
37		eqid 2729	. . . 4 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
38	37	lbsex 21051	. . 3 ⊢ (((subringAlg ‘𝐽)‘𝐹) ∈ LVec → (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ≠ ∅)
39	36, 38	syl 17	. 2 ⊢ (𝜑 → (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ≠ ∅)
40		fldextrspunfld.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ Field)
41		fldidom 20656	. . . . . . . . . . . 12 ⊢ (𝐿 ∈ Field → 𝐿 ∈ IDomn)
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ IDomn)
43	42	idomringd 20613	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ Ring)
44		eqidd 2730	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐿) = (Base‘𝐿))
45	25	sdrgss 20678	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
46	11, 45	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
47	46, 27	unssd 4151	. . . . . . . . . 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 20498	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝐿))
53	43, 44, 47, 49, 51	rgspnssid 20499	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ 𝐶)
54	53	unssad 4152	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ⊆ 𝐶)
55		fldextrspunfld.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐿 ↾_s 𝐶)
56	55	subsubrg 20483	. . . . . . . . . 10 ⊢ (𝐶 ∈ (SubRing‘𝐿) → (𝐺 ∈ (SubRing‘𝐸) ↔ (𝐺 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶)))
57	56	biimpar 477	. . . . . . . . 9 ⊢ ((𝐶 ∈ (SubRing‘𝐿) ∧ (𝐺 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶)) → 𝐺 ∈ (SubRing‘𝐸))
58	52, 13, 54, 57	syl12anc 836	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐸))
59		eqid 2729	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺)
60	59	sralmod 21070	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐸) → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
61	58, 60	syl 17	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
62		ressabs 17194	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶) → ((𝐿 ↾_s 𝐶) ↾_s 𝐺) = (𝐿 ↾_s 𝐺))
63	52, 54, 62	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 ↾_s 𝐶) ↾_s 𝐺) = (𝐿 ↾_s 𝐺))
64	55	oveq1i 7379	. . . . . . . . . 10 ⊢ (𝐸 ↾_s 𝐺) = ((𝐿 ↾_s 𝐶) ↾_s 𝐺)
65	63, 64, 17	3eqtr4g 2789	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s 𝐺) = 𝐼)
66		eqidd 2730	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺))
67	25	subrgss 20457	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ (SubRing‘𝐿) → 𝐶 ⊆ (Base‘𝐿))
68	52, 67	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ⊆ (Base‘𝐿))
69	55, 25	ressbas2 17184	. . . . . . . . . . . . 13 ⊢ (𝐶 ⊆ (Base‘𝐿) → 𝐶 = (Base‘𝐸))
70	68, 69	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 = (Base‘𝐸))
71	53, 70	sseqtrd 3980	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ (Base‘𝐸))
72	71	unssad 4152	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐸))
73	66, 72	srasca 21063	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s 𝐺) = (Scalar‘((subringAlg ‘𝐸)‘𝐺)))
74	65, 73	eqtr3d 2766	. . . . . . . 8 ⊢ (𝜑 → 𝐼 = (Scalar‘((subringAlg ‘𝐸)‘𝐺)))
75	17	sdrgdrng 20675	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐼 ∈ DivRing)
76	11, 75	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ DivRing)
77	74, 76	eqeltrrd 2829	. . . . . . 7 ⊢ (𝜑 → (Scalar‘((subringAlg ‘𝐸)‘𝐺)) ∈ DivRing)
78		eqid 2729	. . . . . . . 8 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐺)) = (Scalar‘((subringAlg ‘𝐸)‘𝐺))
79	78	islvec 20987	. . . . . . 7 ⊢ (((subringAlg ‘𝐸)‘𝐺) ∈ LVec ↔ (((subringAlg ‘𝐸)‘𝐺) ∈ LMod ∧ (Scalar‘((subringAlg ‘𝐸)‘𝐺)) ∈ DivRing))
80	61, 77, 79	sylanbrc 583	. . . . . 6 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) ∈ LVec)
81		eqid 2729	. . . . . . 7 ⊢ (LBasis‘((subringAlg ‘𝐸)‘𝐺)) = (LBasis‘((subringAlg ‘𝐸)‘𝐺))
82	81	lbsex 21051	. . . . . 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 33569	. . . . . 6 ⊢ ((((subringAlg ‘𝐸)‘𝐺) ∈ LVec ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) = (♯‘𝑐))
88	85, 86, 87	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) = (♯‘𝑐))
89		eqid 2729	. . . . . 6 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐺)) = (Base‘((subringAlg ‘𝐸)‘𝐺))
90		eqid 2729	. . . . . 6 ⊢ (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘((subringAlg ‘𝐸)‘𝐺))
91		eqid 2729	. . . . . . . . . . . 12 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
92	91, 37	lbsss 20960	. . . . . . . . . . 11 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
93	92	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
94		eqidd 2730	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
95	94, 24	srabase 21060	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
96	29, 95	eqtrd 2764	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
97	96	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
98	93, 97	sseqtrrd 3981	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ 𝐻)
99	53	unssbd 4153	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ⊆ 𝐶)
100	99	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐻 ⊆ 𝐶)
101	98, 100	sstrd 3954	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ 𝐶)
102	70	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐶 = (Base‘𝐸))
103	101, 102	sseqtrd 3980	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘𝐸))
104		eqidd 2730	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺))
105	72	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐺 ⊆ (Base‘𝐸))
106	104, 105	srabase 21060	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘𝐺)))
107	103, 106	sseqtrd 3980	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
108	61	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
109	89, 90	lspssv 20865	. . . . . . . 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 20683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐿 ∈ Field ∧ 𝐻 ∈ (SubDRing‘𝐿)) → (𝐿 ↾_s 𝐻) ∈ Field)
119	40, 1, 118	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 ↾_s 𝐻) ∈ Field)
120	2, 119	eqeltrid 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ Field)
121		ressabs 17194	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐻 ∈ (SubDRing‘𝐿) ∧ 𝐹 ⊆ 𝐻) → ((𝐿 ↾_s 𝐻) ↾_s 𝐹) = (𝐿 ↾_s 𝐹))
122	1, 30, 121	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐿 ↾_s 𝐻) ↾_s 𝐹) = (𝐿 ↾_s 𝐹))
123	2	oveq1i 7379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ↾_s 𝐹) = ((𝐿 ↾_s 𝐻) ↾_s 𝐹)
124	122, 123, 111	3eqtr4g 2789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) = 𝐾)
125		fldsdrgfld 20683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐽)) → (𝐽 ↾_s 𝐹) ∈ Field)
126	120, 5, 125	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) ∈ Field)
127	124, 126	eqeltrrd 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ Field)
128	30, 27	sstrd 3954	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
129	111, 25	ressbas2 17184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ⊆ (Base‘𝐿) → 𝐹 = (Base‘𝐾))
130	128, 129	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
131	130	oveq2d 7385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) = (𝐽 ↾_s (Base‘𝐾)))
132	124, 131	eqtr3d 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (𝐽 ↾_s (Base‘𝐾)))
133	130, 33	eqeltrrd 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐽))
134		brfldext 33614	. . . . . . . . . . . . . . . . . . . 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 33622	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽/_FldExt𝐾 → (𝐽[:]𝐾) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
139	137, 138	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
140	130	fveq2d 6844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘(Base‘𝐾)))
141	140	fveq2d 6844	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
142	141	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
143	37	dimval 33569	. . . . . . . . . . . . . . . . 17 ⊢ ((((subringAlg ‘𝐽)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (♯‘𝑏))
144	36, 143	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (♯‘𝑏))
145	139, 142, 144	3eqtr2d 2770	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) = (♯‘𝑏))
146		fldextrspunfld.7	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ₀)
147	146	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) ∈ ℕ₀)
148	145, 147	eqeltrrd 2829	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (♯‘𝑏) ∈ ℕ₀)
149		hashclb 14299	. . . . . . . . . . . . . . 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 33642	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
153	152	eqimssd 4000	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
154	25, 55, 68, 54, 40	resssra 33556	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) = (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))
155	154	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)))
156	155	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)))
157	156	fveq1d 6842	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) = ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏))
158	115, 12	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐺 ∈ (SubRing‘𝐿))
159		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺)
160	159	sralmod 21070	. . . . . . . . . . . . . 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 3981	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ 𝐻)
165	116, 26	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ⊆ (Base‘𝐿))
166	164, 165	sstrd 3954	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘𝐿))
167		eqidd 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺))
168	167, 46	srabase 21060	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
169	168	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
170	166, 169	sseqtrd 3980	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺)))
171		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (Base‘((subringAlg ‘𝐿)‘𝐺)) = (Base‘((subringAlg ‘𝐿)‘𝐺))
172		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)) = (LSubSp‘((subringAlg ‘𝐿)‘𝐺))
173		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (LSpan‘((subringAlg ‘𝐿)‘𝐺)) = (LSpan‘((subringAlg ‘𝐿)‘𝐺))
174	171, 172, 173	lspcl 20858	. . . . . . . . . . . . . . 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 2828	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
177	99	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ⊆ 𝐶)
178	164, 177	sstrd 3954	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ 𝐶)
179		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶) = (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)
180		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))
181	179, 173, 180, 172	lsslsp 20897	. . . . . . . . . . . . 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 2765	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) = ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
184	153, 183	sseqtrd 3980	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
185	184	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
186	102, 185	eqsstrrd 3979	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘𝐸) ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
187	106, 186	eqsstrrd 3979	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘((subringAlg ‘𝐸)‘𝐺)) ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
188	110, 187	eqssd 3961	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) = (Base‘((subringAlg ‘𝐸)‘𝐺)))
189	89, 81, 90, 85, 86, 107, 188	lbslelsp 33566	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (♯‘𝑐) ≤ (♯‘𝑏))
190	88, 189	eqbrtrd 5124	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (♯‘𝑏))
191	84, 190	n0limd 32374	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (♯‘𝑏))
192	191, 145	breqtrrd 5130	. 2 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))
193	39, 192	n0limd 32374	1 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∪ cun 3909 ⊆ wss 3911 ∅c0 4292 class class class wbr 5102 ‘cfv 6499 (class class class)co 7369 Fincfn 8895 ≤ cle 11185 ℕ₀cn0 12418 ♯chash 14271 Basecbs 17155 ↾_s cress 17176 Scalarcsca 17199 SubRingcsubrg 20454 RingSpancrgspn 20495 IDomncidom 20578 DivRingcdr 20614 Fieldcfield 20615 SubDRingcsdrg 20671 LModclmod 20742 LSubSpclss 20813 LSpanclspn 20853 LBasisclbs 20957 LVecclvec 20985 subringAlg csra 21054 dimcldim 33567 /_FldExtcfldext 33607 [:]cextdg 33609

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 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-reg 9521 ax-inf2 9570 ax-ac2 10392 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122 ax-addf 11123

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 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-of 7633 df-rpss 7679 df-om 7823 df-1st 7947 df-2nd 7948 df-supp 8117 df-tpos 8182 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-oadd 8415 df-er 8648 df-map 8778 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9289 df-sup 9369 df-inf 9370 df-oi 9439 df-r1 9693 df-rank 9694 df-dju 9830 df-card 9868 df-acn 9871 df-ac 10045 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-6 12229 df-7 12230 df-8 12231 df-9 12232 df-n0 12419 df-xnn0 12492 df-z 12506 df-dec 12626 df-uz 12770 df-rp 12928 df-fz 13445 df-fzo 13592 df-seq 13943 df-exp 14003 df-hash 14272 df-word 14455 df-lsw 14504 df-concat 14512 df-s1 14537 df-substr 14582 df-pfx 14612 df-s2 14790 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-clim 15430 df-sum 15629 df-struct 17093 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-starv 17211 df-sca 17212 df-vsca 17213 df-ip 17214 df-tset 17215 df-ple 17216 df-ocomp 17217 df-ds 17218 df-unif 17219 df-hom 17220 df-cco 17221 df-0g 17380 df-gsum 17381 df-prds 17386 df-pws 17388 df-mre 17523 df-mrc 17524 df-mri 17525 df-acs 17526 df-proset 18231 df-drs 18232 df-poset 18250 df-ipo 18463 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-mhm 18686 df-submnd 18687 df-grp 18844 df-minusg 18845 df-sbg 18846 df-mulg 18976 df-subg 19031 df-ghm 19121 df-cntz 19225 df-cmn 19688 df-abl 19689 df-mgp 20026 df-rng 20038 df-ur 20067 df-ring 20120 df-cring 20121 df-oppr 20222 df-dvdsr 20242 df-unit 20243 df-invr 20273 df-nzr 20398 df-subrng 20431 df-subrg 20455 df-rgspn 20496 df-rlreg 20579 df-domn 20580 df-idom 20581 df-drng 20616 df-field 20617 df-sdrg 20672 df-lmod 20744 df-lss 20814 df-lsp 20854 df-lmhm 20905 df-lbs 20958 df-lvec 20986 df-sra 21056 df-rgmod 21057 df-cnfld 21241 df-zring 21333 df-dsmm 21617 df-frlm 21632 df-uvc 21668 df-ind 32747 df-dim 33568 df-fldext 33610 df-extdg 33611

This theorem is referenced by: fldextrspunfld 33644 fldextrspundgle 33646

W3C validator