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 33933

Description: Lemma for fldextrspunfld 33934. 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 20827	. . . . 5 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐽 ∈ DivRing)
4	1, 3	syl 17	. . . 4 ⊢ (𝜑 → 𝐽 ∈ DivRing)
5		fldextrspunfld.4	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
6		eqid 2761	. . . . . 6 ⊢ (𝐽 ↾_s 𝐹) = (𝐽 ↾_s 𝐹)
7	6	sdrgdrng 20827	. . . . 5 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → (𝐽 ↾_s 𝐹) ∈ DivRing)
8	5, 7	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) ∈ DivRing)
9		sdrgsubrg 20828	. . . . . 6 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
10	1, 9	syl 17	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
11		fldextrspunfld.5	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
12		sdrgsubrg 20828	. . . . . . . 8 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
13	11, 12	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
14		fldextrspunfld.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
15		sdrgsubrg 20828	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐼) → 𝐹 ∈ (SubRing‘𝐼))
16	14, 15	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐼))
17		fldextrspunfld.i	. . . . . . . . 9 ⊢ 𝐼 = (𝐿 ↾_s 𝐺)
18	17	subsubrg 20635	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐿) → (𝐹 ∈ (SubRing‘𝐼) ↔ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺)))
19	18	biimpa 480	. . . . . . 7 ⊢ ((𝐺 ∈ (SubRing‘𝐿) ∧ 𝐹 ∈ (SubRing‘𝐼)) → (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺))
20	13, 16, 19	syl2anc 593	. . . . . 6 ⊢ (𝜑 → (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺))
21	20	simpld 498	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿))
22		eqid 2761	. . . . . . . 8 ⊢ (Base‘𝐽) = (Base‘𝐽)
23	22	sdrgss 20830	. . . . . . 7 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
24	5, 23	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
25		eqid 2761	. . . . . . . . 9 ⊢ (Base‘𝐿) = (Base‘𝐿)
26	25	sdrgss 20830	. . . . . . . 8 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
27	1, 26	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
28	2, 25	ressbas2 17265	. . . . . . 7 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
29	27, 28	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
30	24, 29	sseqtrrd 3971	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ 𝐻)
31	2	subsubrg 20635	. . . . . 6 ⊢ (𝐻 ∈ (SubRing‘𝐿) → (𝐹 ∈ (SubRing‘𝐽) ↔ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐻)))
32	31	biimpar 481	. . . . 5 ⊢ ((𝐻 ∈ (SubRing‘𝐿) ∧ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐻)) → 𝐹 ∈ (SubRing‘𝐽))
33	10, 21, 30, 32	syl12anc 847	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐽))
34		eqid 2761	. . . . 5 ⊢ ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹)
35	34, 6	sralvec 33843	. . . 4 ⊢ ((𝐽 ∈ DivRing ∧ (𝐽 ↾_s 𝐹) ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐽)) → ((subringAlg ‘𝐽)‘𝐹) ∈ LVec)
36	4, 8, 33, 35	syl3anc 1389	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ LVec)
37		eqid 2761	. . . 4 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
38	37	lbsex 21223	. . 3 ⊢ (((subringAlg ‘𝐽)‘𝐹) ∈ LVec → (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ≠ ∅)
39	36, 38	syl 17	. 2 ⊢ (𝜑 → (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ≠ ∅)
40		fldextrspunfld.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ Field)
41		fldidom 20808	. . . . . . . . . . . 12 ⊢ (𝐿 ∈ Field → 𝐿 ∈ IDomn)
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ IDomn)
43	42	idomringd 20765	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ Ring)
44		eqidd 2762	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐿) = (Base‘𝐿))
45	25	sdrgss 20830	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
46	11, 45	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
47	46, 27	unssd 4142	. . . . . . . . . 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 20650	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝐿))
53	43, 44, 47, 49, 51	rgspnssid 20651	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ 𝐶)
54	53	unssad 4143	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ⊆ 𝐶)
55		fldextrspunfld.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐿 ↾_s 𝐶)
56	55	subsubrg 20635	. . . . . . . . . 10 ⊢ (𝐶 ∈ (SubRing‘𝐿) → (𝐺 ∈ (SubRing‘𝐸) ↔ (𝐺 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶)))
57	56	biimpar 481	. . . . . . . . 9 ⊢ ((𝐶 ∈ (SubRing‘𝐿) ∧ (𝐺 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶)) → 𝐺 ∈ (SubRing‘𝐸))
58	52, 13, 54, 57	syl12anc 847	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐸))
59		eqid 2761	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺)
60	59	sralmod 21242	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐸) → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
61	58, 60	syl 17	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
62		ressabs 17275	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶) → ((𝐿 ↾_s 𝐶) ↾_s 𝐺) = (𝐿 ↾_s 𝐺))
63	52, 54, 62	syl2anc 593	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 ↾_s 𝐶) ↾_s 𝐺) = (𝐿 ↾_s 𝐺))
64	55	oveq1i 7401	. . . . . . . . . 10 ⊢ (𝐸 ↾_s 𝐺) = ((𝐿 ↾_s 𝐶) ↾_s 𝐺)
65	63, 64, 17	3eqtr4g 2821	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s 𝐺) = 𝐼)
66		eqidd 2762	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺))
67	25	subrgss 20609	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ (SubRing‘𝐿) → 𝐶 ⊆ (Base‘𝐿))
68	52, 67	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ⊆ (Base‘𝐿))
69	55, 25	ressbas2 17265	. . . . . . . . . . . . 13 ⊢ (𝐶 ⊆ (Base‘𝐿) → 𝐶 = (Base‘𝐸))
70	68, 69	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 = (Base‘𝐸))
71	53, 70	sseqtrd 3970	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ (Base‘𝐸))
72	71	unssad 4143	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐸))
73	66, 72	srasca 21235	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s 𝐺) = (Scalar‘((subringAlg ‘𝐸)‘𝐺)))
74	65, 73	eqtr3d 2798	. . . . . . . 8 ⊢ (𝜑 → 𝐼 = (Scalar‘((subringAlg ‘𝐸)‘𝐺)))
75	17	sdrgdrng 20827	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐼 ∈ DivRing)
76	11, 75	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ DivRing)
77	74, 76	eqeltrrd 2862	. . . . . . 7 ⊢ (𝜑 → (Scalar‘((subringAlg ‘𝐸)‘𝐺)) ∈ DivRing)
78		eqid 2761	. . . . . . . 8 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐺)) = (Scalar‘((subringAlg ‘𝐸)‘𝐺))
79	78	islvec 21159	. . . . . . 7 ⊢ (((subringAlg ‘𝐸)‘𝐺) ∈ LVec ↔ (((subringAlg ‘𝐸)‘𝐺) ∈ LMod ∧ (Scalar‘((subringAlg ‘𝐸)‘𝐺)) ∈ DivRing))
80	61, 77, 79	sylanbrc 592	. . . . . 6 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) ∈ LVec)
81		eqid 2761	. . . . . . 7 ⊢ (LBasis‘((subringAlg ‘𝐸)‘𝐺)) = (LBasis‘((subringAlg ‘𝐸)‘𝐺))
82	81	lbsex 21223	. . . . . 6 ⊢ (((subringAlg ‘𝐸)‘𝐺) ∈ LVec → (LBasis‘((subringAlg ‘𝐸)‘𝐺)) ≠ ∅)
83	80, 82	syl 17	. . . . 5 ⊢ (𝜑 → (LBasis‘((subringAlg ‘𝐸)‘𝐺)) ≠ ∅)
84	83	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (LBasis‘((subringAlg ‘𝐸)‘𝐺)) ≠ ∅)
85	80	ad2antrr 736	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) ∈ LVec)
86		simpr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺)))
87	81	dimval 33859	. . . . . 6 ⊢ ((((subringAlg ‘𝐸)‘𝐺) ∈ LVec ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) = (♯‘𝑐))
88	85, 86, 87	syl2anc 593	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) = (♯‘𝑐))
89		eqid 2761	. . . . . 6 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐺)) = (Base‘((subringAlg ‘𝐸)‘𝐺))
90		eqid 2761	. . . . . 6 ⊢ (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘((subringAlg ‘𝐸)‘𝐺))
91		eqid 2761	. . . . . . . . . . . 12 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
92	91, 37	lbsss 21132	. . . . . . . . . . 11 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
93	92	ad2antlr 737	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
94		eqidd 2762	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
95	94, 24	srabase 21232	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
96	29, 95	eqtrd 2796	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
97	96	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
98	93, 97	sseqtrrd 3971	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ 𝐻)
99	53	unssbd 4144	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ⊆ 𝐶)
100	99	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐻 ⊆ 𝐶)
101	98, 100	sstrd 3944	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ 𝐶)
102	70	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐶 = (Base‘𝐸))
103	101, 102	sseqtrd 3970	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘𝐸))
104		eqidd 2762	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺))
105	72	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐺 ⊆ (Base‘𝐸))
106	104, 105	srabase 21232	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘𝐺)))
107	103, 106	sseqtrd 3970	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
108	61	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
109	89, 90	lspssv 21038	. . . . . . . 8 ⊢ ((((subringAlg ‘𝐸)‘𝐺) ∈ LMod ∧ 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
110	108, 107, 109	syl2anc 593	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
111		fldextrspunfld.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (𝐿 ↾_s 𝐹)
112	40	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐿 ∈ Field)
113	14	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐹 ∈ (SubDRing‘𝐼))
114	5	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐹 ∈ (SubDRing‘𝐽))
115	11	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐺 ∈ (SubDRing‘𝐿))
116	1	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ∈ (SubDRing‘𝐿))
117		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
118		fldsdrgfld 20835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐿 ∈ Field ∧ 𝐻 ∈ (SubDRing‘𝐿)) → (𝐿 ↾_s 𝐻) ∈ Field)
119	40, 1, 118	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 ↾_s 𝐻) ∈ Field)
120	2, 119	eqeltrid 2865	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ Field)
121		ressabs 17275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐻 ∈ (SubDRing‘𝐿) ∧ 𝐹 ⊆ 𝐻) → ((𝐿 ↾_s 𝐻) ↾_s 𝐹) = (𝐿 ↾_s 𝐹))
122	1, 30, 121	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐿 ↾_s 𝐻) ↾_s 𝐹) = (𝐿 ↾_s 𝐹))
123	2	oveq1i 7401	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ↾_s 𝐹) = ((𝐿 ↾_s 𝐻) ↾_s 𝐹)
124	122, 123, 111	3eqtr4g 2821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) = 𝐾)
125		fldsdrgfld 20835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐽)) → (𝐽 ↾_s 𝐹) ∈ Field)
126	120, 5, 125	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) ∈ Field)
127	124, 126	eqeltrrd 2862	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ Field)
128	30, 27	sstrd 3944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
129	111, 25	ressbas2 17265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ⊆ (Base‘𝐿) → 𝐹 = (Base‘𝐾))
130	128, 129	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
131	130	oveq2d 7407	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) = (𝐽 ↾_s (Base‘𝐾)))
132	124, 131	eqtr3d 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (𝐽 ↾_s (Base‘𝐾)))
133	130, 33	eqeltrrd 2862	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐽))
134		brfldext 33903	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ Field ∧ 𝐾 ∈ Field) → (𝐽/_FldExt𝐾 ↔ (𝐾 = (𝐽 ↾_s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐽))))
135	134	biimpar 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Field ∧ 𝐾 ∈ Field) ∧ (𝐾 = (𝐽 ↾_s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐽))) → 𝐽/_FldExt𝐾)
136	120, 127, 132, 133, 135	syl22anc 849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐽/_FldExt𝐾)
137	136	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐽/_FldExt𝐾)
138		extdgval 33911	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽/_FldExt𝐾 → (𝐽[:]𝐾) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
139	137, 138	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
140	130	fveq2d 6866	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘(Base‘𝐾)))
141	140	fveq2d 6866	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
142	141	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
143	37	dimval 33859	. . . . . . . . . . . . . . . . 17 ⊢ ((((subringAlg ‘𝐽)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (♯‘𝑏))
144	36, 143	sylan 589	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (♯‘𝑏))
145	139, 142, 144	3eqtr2d 2802	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) = (♯‘𝑏))
146		fldextrspunfld.7	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ₀)
147	146	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) ∈ ℕ₀)
148	145, 147	eqeltrrd 2862	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (♯‘𝑏) ∈ ℕ₀)
149		hashclb 14365	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → (𝑏 ∈ Fin ↔ (♯‘𝑏) ∈ ℕ₀))
150	149	biimpar 481	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ∧ (♯‘𝑏) ∈ ℕ₀) → 𝑏 ∈ Fin)
151	117, 148, 150	syl2anc 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ∈ Fin)
152	111, 17, 2, 112, 113, 114, 115, 116, 48, 50, 55, 117, 151	fldextrspunlsp 33932	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
153	152	eqimssd 3990	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
154	25, 55, 68, 54, 40	resssra 33845	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) = (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))
155	154	fveq2d 6866	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)))
156	155	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)))
157	156	fveq1d 6864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) = ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏))
158	115, 12	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐺 ∈ (SubRing‘𝐿))
159		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺)
160	159	sralmod 21242	. . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
164	162, 163	sseqtrrd 3971	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ 𝐻)
165	116, 26	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ⊆ (Base‘𝐿))
166	164, 165	sstrd 3944	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘𝐿))
167		eqidd 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺))
168	167, 46	srabase 21232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
169	168	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
170	166, 169	sseqtrd 3970	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺)))
171		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (Base‘((subringAlg ‘𝐿)‘𝐺)) = (Base‘((subringAlg ‘𝐿)‘𝐺))
172		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)) = (LSubSp‘((subringAlg ‘𝐿)‘𝐺))
173		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (LSpan‘((subringAlg ‘𝐿)‘𝐺)) = (LSpan‘((subringAlg ‘𝐿)‘𝐺))
174	171, 172, 173	lspcl 21031	. . . . . . . . . . . . . . 15 ⊢ ((((subringAlg ‘𝐿)‘𝐺) ∈ LMod ∧ 𝑏 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
175	161, 170, 174	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
176	152, 175	eqeltrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
177	99	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ⊆ 𝐶)
178	164, 177	sstrd 3944	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ 𝐶)
179		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶) = (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)
180		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))
181	179, 173, 180, 172	lsslsp 21070	. . . . . . . . . . . . 13 ⊢ ((((subringAlg ‘𝐿)‘𝐺) ∈ LMod ∧ 𝐶 ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)) ∧ 𝑏 ⊆ 𝐶) → ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏) = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
182	161, 176, 178, 181	syl3anc 1389	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏) = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
183	157, 182	eqtr2d 2797	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) = ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
184	153, 183	sseqtrd 3970	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
185	184	adantr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
186	102, 185	eqsstrrd 3969	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘𝐸) ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
187	106, 186	eqsstrrd 3969	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘((subringAlg ‘𝐸)‘𝐺)) ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
188	110, 187	eqssd 3951	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) = (Base‘((subringAlg ‘𝐸)‘𝐺)))
189	89, 81, 90, 85, 86, 107, 188	lbslelsp 33856	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (♯‘𝑐) ≤ (♯‘𝑏))
190	88, 189	eqbrtrd 5119	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (♯‘𝑏))
191	84, 190	n0limd 32630	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (♯‘𝑏))
192	191, 145	breqtrrd 5125	. 2 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))
193	39, 192	n0limd 32630	1 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∪ cun 3900 ⊆ wss 3902 ∅c0 4283 class class class wbr 5097 ‘cfv 6516 (class class class)co 7391 Fincfn 8921 ≤ cle 11211 ℕ₀cn0 12475 ♯chash 14337 Basecbs 17236 ↾_s cress 17257 Scalarcsca 17280 SubRingcsubrg 20606 RingSpancrgspn 20647 IDomncidom 20730 DivRingcdr 20766 Fieldcfield 20767 SubDRingcsdrg 20823 LModclmod 20915 LSubSpclss 20986 LSpanclspn 21026 LBasisclbs 21129 LVecclvec 21157 subringAlg csra 21226 dimcldim 33857 /_FldExtcfldext 33896 [:]cextdg 33898

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-reg 9534 ax-inf2 9590 ax-ac2 10414 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145 ax-addf 11146

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-of 7655 df-rpss 7701 df-om 7842 df-1st 7965 df-2nd 7966 df-supp 8135 df-tpos 8200 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-2o 8432 df-oadd 8435 df-er 8672 df-map 8804 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9302 df-sup 9382 df-inf 9383 df-oi 9452 df-r1 9716 df-rank 9717 df-dju 9853 df-card 9891 df-acn 9894 df-ac 10066 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-ind 12190 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-7 12279 df-8 12280 df-9 12281 df-n0 12476 df-xnn0 12549 df-z 12563 df-dec 12683 df-uz 12834 df-rp 12988 df-fz 13507 df-fzo 13654 df-seq 14009 df-exp 14069 df-hash 14338 df-word 14521 df-lsw 14570 df-concat 14578 df-s1 14604 df-substr 14649 df-pfx 14679 df-s2 14855 df-cj 15117 df-re 15118 df-im 15119 df-sqrt 15253 df-abs 15254 df-clim 15506 df-sum 15705 df-struct 17174 df-sets 17191 df-slot 17209 df-ndx 17221 df-base 17237 df-ress 17258 df-plusg 17290 df-mulr 17291 df-starv 17292 df-sca 17293 df-vsca 17294 df-ip 17295 df-tset 17296 df-ple 17297 df-ocomp 17298 df-ds 17299 df-unif 17300 df-hom 17301 df-cco 17302 df-0g 17461 df-gsum 17462 df-prds 17467 df-pws 17469 df-mre 17605 df-mrc 17606 df-mri 17607 df-acs 17608 df-proset 18317 df-drs 18318 df-poset 18336 df-ipo 18551 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-mhm 18808 df-submnd 18809 df-grp 18969 df-minusg 18970 df-sbg 18971 df-mulg 19101 df-subg 19156 df-ghm 19245 df-cntz 19348 df-cmn 19813 df-abl 19814 df-mgp 20178 df-rng 20190 df-ur 20219 df-ring 20272 df-cring 20273 df-oppr 20373 df-dvdsr 20393 df-unit 20394 df-invr 20424 df-nzr 20550 df-subrng 20583 df-subrg 20607 df-rgspn 20648 df-rlreg 20731 df-domn 20732 df-idom 20733 df-drng 20768 df-field 20769 df-sdrg 20824 df-lmod 20917 df-lss 20987 df-lsp 21027 df-lmhm 21077 df-lbs 21130 df-lvec 21158 df-sra 21228 df-rgmod 21229 df-cnfld 21413 df-zring 21487 df-dsmm 21772 df-frlm 21787 df-uvc 21823 df-dim 33858 df-fldext 33899 df-extdg 33900

This theorem is referenced by: fldextrspunfld 33934 fldextrspundgle 33936

W3C validator