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 33819

Description: Lemma for fldextrspunfld 33820. 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 20767	. . . . 5 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐽 ∈ DivRing)
4	1, 3	syl 17	. . . 4 ⊢ (𝜑 → 𝐽 ∈ DivRing)
5		fldextrspunfld.4	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
6		eqid 2736	. . . . . 6 ⊢ (𝐽 ↾_s 𝐹) = (𝐽 ↾_s 𝐹)
7	6	sdrgdrng 20767	. . . . 5 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → (𝐽 ↾_s 𝐹) ∈ DivRing)
8	5, 7	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) ∈ DivRing)
9		sdrgsubrg 20768	. . . . . 6 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
10	1, 9	syl 17	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
11		fldextrspunfld.5	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
12		sdrgsubrg 20768	. . . . . . . 8 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
13	11, 12	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
14		fldextrspunfld.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
15		sdrgsubrg 20768	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐼) → 𝐹 ∈ (SubRing‘𝐼))
16	14, 15	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐼))
17		fldextrspunfld.i	. . . . . . . . 9 ⊢ 𝐼 = (𝐿 ↾_s 𝐺)
18	17	subsubrg 20575	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐿) → (𝐹 ∈ (SubRing‘𝐼) ↔ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺)))
19	18	biimpa 476	. . . . . . 7 ⊢ ((𝐺 ∈ (SubRing‘𝐿) ∧ 𝐹 ∈ (SubRing‘𝐼)) → (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺))
20	13, 16, 19	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺))
21	20	simpld 494	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿))
22		eqid 2736	. . . . . . . 8 ⊢ (Base‘𝐽) = (Base‘𝐽)
23	22	sdrgss 20770	. . . . . . 7 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
24	5, 23	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
25		eqid 2736	. . . . . . . . 9 ⊢ (Base‘𝐿) = (Base‘𝐿)
26	25	sdrgss 20770	. . . . . . . 8 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
27	1, 26	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
28	2, 25	ressbas2 17208	. . . . . . 7 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
29	27, 28	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
30	24, 29	sseqtrrd 3959	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ 𝐻)
31	2	subsubrg 20575	. . . . . 6 ⊢ (𝐻 ∈ (SubRing‘𝐿) → (𝐹 ∈ (SubRing‘𝐽) ↔ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐻)))
32	31	biimpar 477	. . . . 5 ⊢ ((𝐻 ∈ (SubRing‘𝐿) ∧ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐻)) → 𝐹 ∈ (SubRing‘𝐽))
33	10, 21, 30, 32	syl12anc 837	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐽))
34		eqid 2736	. . . . 5 ⊢ ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹)
35	34, 6	sralvec 33729	. . . 4 ⊢ ((𝐽 ∈ DivRing ∧ (𝐽 ↾_s 𝐹) ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐽)) → ((subringAlg ‘𝐽)‘𝐹) ∈ LVec)
36	4, 8, 33, 35	syl3anc 1374	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ LVec)
37		eqid 2736	. . . 4 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
38	37	lbsex 21163	. . 3 ⊢ (((subringAlg ‘𝐽)‘𝐹) ∈ LVec → (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ≠ ∅)
39	36, 38	syl 17	. 2 ⊢ (𝜑 → (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ≠ ∅)
40		fldextrspunfld.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ Field)
41		fldidom 20748	. . . . . . . . . . . 12 ⊢ (𝐿 ∈ Field → 𝐿 ∈ IDomn)
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ IDomn)
43	42	idomringd 20705	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ Ring)
44		eqidd 2737	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐿) = (Base‘𝐿))
45	25	sdrgss 20770	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
46	11, 45	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
47	46, 27	unssd 4132	. . . . . . . . . 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 20590	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝐿))
53	43, 44, 47, 49, 51	rgspnssid 20591	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ 𝐶)
54	53	unssad 4133	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ⊆ 𝐶)
55		fldextrspunfld.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐿 ↾_s 𝐶)
56	55	subsubrg 20575	. . . . . . . . . 10 ⊢ (𝐶 ∈ (SubRing‘𝐿) → (𝐺 ∈ (SubRing‘𝐸) ↔ (𝐺 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶)))
57	56	biimpar 477	. . . . . . . . 9 ⊢ ((𝐶 ∈ (SubRing‘𝐿) ∧ (𝐺 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶)) → 𝐺 ∈ (SubRing‘𝐸))
58	52, 13, 54, 57	syl12anc 837	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐸))
59		eqid 2736	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺)
60	59	sralmod 21182	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐸) → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
61	58, 60	syl 17	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
62		ressabs 17218	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶) → ((𝐿 ↾_s 𝐶) ↾_s 𝐺) = (𝐿 ↾_s 𝐺))
63	52, 54, 62	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 ↾_s 𝐶) ↾_s 𝐺) = (𝐿 ↾_s 𝐺))
64	55	oveq1i 7377	. . . . . . . . . 10 ⊢ (𝐸 ↾_s 𝐺) = ((𝐿 ↾_s 𝐶) ↾_s 𝐺)
65	63, 64, 17	3eqtr4g 2796	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s 𝐺) = 𝐼)
66		eqidd 2737	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺))
67	25	subrgss 20549	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ (SubRing‘𝐿) → 𝐶 ⊆ (Base‘𝐿))
68	52, 67	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ⊆ (Base‘𝐿))
69	55, 25	ressbas2 17208	. . . . . . . . . . . . 13 ⊢ (𝐶 ⊆ (Base‘𝐿) → 𝐶 = (Base‘𝐸))
70	68, 69	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 = (Base‘𝐸))
71	53, 70	sseqtrd 3958	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ (Base‘𝐸))
72	71	unssad 4133	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐸))
73	66, 72	srasca 21175	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s 𝐺) = (Scalar‘((subringAlg ‘𝐸)‘𝐺)))
74	65, 73	eqtr3d 2773	. . . . . . . 8 ⊢ (𝜑 → 𝐼 = (Scalar‘((subringAlg ‘𝐸)‘𝐺)))
75	17	sdrgdrng 20767	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐼 ∈ DivRing)
76	11, 75	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ DivRing)
77	74, 76	eqeltrrd 2837	. . . . . . 7 ⊢ (𝜑 → (Scalar‘((subringAlg ‘𝐸)‘𝐺)) ∈ DivRing)
78		eqid 2736	. . . . . . . 8 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐺)) = (Scalar‘((subringAlg ‘𝐸)‘𝐺))
79	78	islvec 21099	. . . . . . 7 ⊢ (((subringAlg ‘𝐸)‘𝐺) ∈ LVec ↔ (((subringAlg ‘𝐸)‘𝐺) ∈ LMod ∧ (Scalar‘((subringAlg ‘𝐸)‘𝐺)) ∈ DivRing))
80	61, 77, 79	sylanbrc 584	. . . . . 6 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) ∈ LVec)
81		eqid 2736	. . . . . . 7 ⊢ (LBasis‘((subringAlg ‘𝐸)‘𝐺)) = (LBasis‘((subringAlg ‘𝐸)‘𝐺))
82	81	lbsex 21163	. . . . . 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 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) ∈ LVec)
86		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺)))
87	81	dimval 33745	. . . . . 6 ⊢ ((((subringAlg ‘𝐸)‘𝐺) ∈ LVec ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) = (♯‘𝑐))
88	85, 86, 87	syl2anc 585	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) = (♯‘𝑐))
89		eqid 2736	. . . . . 6 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐺)) = (Base‘((subringAlg ‘𝐸)‘𝐺))
90		eqid 2736	. . . . . 6 ⊢ (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘((subringAlg ‘𝐸)‘𝐺))
91		eqid 2736	. . . . . . . . . . . 12 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
92	91, 37	lbsss 21072	. . . . . . . . . . 11 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
93	92	ad2antlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
94		eqidd 2737	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
95	94, 24	srabase 21172	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
96	29, 95	eqtrd 2771	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
97	96	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
98	93, 97	sseqtrrd 3959	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ 𝐻)
99	53	unssbd 4134	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ⊆ 𝐶)
100	99	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐻 ⊆ 𝐶)
101	98, 100	sstrd 3932	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ 𝐶)
102	70	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐶 = (Base‘𝐸))
103	101, 102	sseqtrd 3958	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘𝐸))
104		eqidd 2737	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺))
105	72	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐺 ⊆ (Base‘𝐸))
106	104, 105	srabase 21172	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘𝐺)))
107	103, 106	sseqtrd 3958	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
108	61	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
109	89, 90	lspssv 20978	. . . . . . . 8 ⊢ ((((subringAlg ‘𝐸)‘𝐺) ∈ LMod ∧ 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
110	108, 107, 109	syl2anc 585	. . . . . . 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 20775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐿 ∈ Field ∧ 𝐻 ∈ (SubDRing‘𝐿)) → (𝐿 ↾_s 𝐻) ∈ Field)
119	40, 1, 118	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 ↾_s 𝐻) ∈ Field)
120	2, 119	eqeltrid 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ Field)
121		ressabs 17218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐻 ∈ (SubDRing‘𝐿) ∧ 𝐹 ⊆ 𝐻) → ((𝐿 ↾_s 𝐻) ↾_s 𝐹) = (𝐿 ↾_s 𝐹))
122	1, 30, 121	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐿 ↾_s 𝐻) ↾_s 𝐹) = (𝐿 ↾_s 𝐹))
123	2	oveq1i 7377	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ↾_s 𝐹) = ((𝐿 ↾_s 𝐻) ↾_s 𝐹)
124	122, 123, 111	3eqtr4g 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) = 𝐾)
125		fldsdrgfld 20775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐽)) → (𝐽 ↾_s 𝐹) ∈ Field)
126	120, 5, 125	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) ∈ Field)
127	124, 126	eqeltrrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ Field)
128	30, 27	sstrd 3932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
129	111, 25	ressbas2 17208	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ⊆ (Base‘𝐿) → 𝐹 = (Base‘𝐾))
130	128, 129	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
131	130	oveq2d 7383	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) = (𝐽 ↾_s (Base‘𝐾)))
132	124, 131	eqtr3d 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (𝐽 ↾_s (Base‘𝐾)))
133	130, 33	eqeltrrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐽))
134		brfldext 33789	. . . . . . . . . . . . . . . . . . . 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 839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐽/_FldExt𝐾)
137	136	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐽/_FldExt𝐾)
138		extdgval 33797	. . . . . . . . . . . . . . . . 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 33745	. . . . . . . . . . . . . . . . 17 ⊢ ((((subringAlg ‘𝐽)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (♯‘𝑏))
144	36, 143	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (♯‘𝑏))
145	139, 142, 144	3eqtr2d 2777	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) = (♯‘𝑏))
146		fldextrspunfld.7	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ₀)
147	146	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) ∈ ℕ₀)
148	145, 147	eqeltrrd 2837	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (♯‘𝑏) ∈ ℕ₀)
149		hashclb 14320	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → (𝑏 ∈ Fin ↔ (♯‘𝑏) ∈ ℕ₀))
150	149	biimpar 477	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ∧ (♯‘𝑏) ∈ ℕ₀) → 𝑏 ∈ Fin)
151	117, 148, 150	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ∈ Fin)
152	111, 17, 2, 112, 113, 114, 115, 116, 48, 50, 55, 117, 151	fldextrspunlsp 33818	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
153	152	eqimssd 3978	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
154	25, 55, 68, 54, 40	resssra 33731	. . . . . . . . . . . . . . 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 2736	. . . . . . . . . . . . . . 15 ⊢ ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺)
160	159	sralmod 21182	. . . . . . . . . . . . . 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 3959	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ 𝐻)
165	116, 26	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ⊆ (Base‘𝐿))
166	164, 165	sstrd 3932	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘𝐿))
167		eqidd 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺))
168	167, 46	srabase 21172	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
169	168	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
170	166, 169	sseqtrd 3958	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺)))
171		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Base‘((subringAlg ‘𝐿)‘𝐺)) = (Base‘((subringAlg ‘𝐿)‘𝐺))
172		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)) = (LSubSp‘((subringAlg ‘𝐿)‘𝐺))
173		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (LSpan‘((subringAlg ‘𝐿)‘𝐺)) = (LSpan‘((subringAlg ‘𝐿)‘𝐺))
174	171, 172, 173	lspcl 20971	. . . . . . . . . . . . . . 15 ⊢ ((((subringAlg ‘𝐿)‘𝐺) ∈ LMod ∧ 𝑏 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
175	161, 170, 174	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
176	152, 175	eqeltrd 2836	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
177	99	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ⊆ 𝐶)
178	164, 177	sstrd 3932	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ 𝐶)
179		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶) = (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)
180		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))
181	179, 173, 180, 172	lsslsp 21010	. . . . . . . . . . . . 13 ⊢ ((((subringAlg ‘𝐿)‘𝐺) ∈ LMod ∧ 𝐶 ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)) ∧ 𝑏 ⊆ 𝐶) → ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏) = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
182	161, 176, 178, 181	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏) = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
183	157, 182	eqtr2d 2772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) = ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
184	153, 183	sseqtrd 3958	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
185	184	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
186	102, 185	eqsstrrd 3957	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘𝐸) ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
187	106, 186	eqsstrrd 3957	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘((subringAlg ‘𝐸)‘𝐺)) ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
188	110, 187	eqssd 3939	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) = (Base‘((subringAlg ‘𝐸)‘𝐺)))
189	89, 81, 90, 85, 86, 107, 188	lbslelsp 33742	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (♯‘𝑐) ≤ (♯‘𝑏))
190	88, 189	eqbrtrd 5107	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (♯‘𝑏))
191	84, 190	n0limd 32541	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (♯‘𝑏))
192	191, 145	breqtrrd 5113	. 2 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))
193	39, 192	n0limd 32541	1 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 ∪ cun 3887 ⊆ wss 3889 ∅c0 4273 class class class wbr 5085 ‘cfv 6498 (class class class)co 7367 Fincfn 8893 ≤ cle 11180 ℕ₀cn0 12437 ♯chash 14292 Basecbs 17179 ↾_s cress 17200 Scalarcsca 17223 SubRingcsubrg 20546 RingSpancrgspn 20587 IDomncidom 20670 DivRingcdr 20706 Fieldcfield 20707 SubDRingcsdrg 20763 LModclmod 20855 LSubSpclss 20926 LSpanclspn 20966 LBasisclbs 21069 LVecclvec 21097 subringAlg csra 21166 dimcldim 33743 /_FldExtcfldext 33782 [:]cextdg 33784

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-reg 9507 ax-inf2 9562 ax-ac2 10385 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-iin 4936 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 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 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-rpss 7677 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-tpos 8176 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-oadd 8409 df-er 8643 df-map 8775 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-sup 9355 df-inf 9356 df-oi 9425 df-r1 9688 df-rank 9689 df-dju 9825 df-card 9863 df-acn 9866 df-ac 10038 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-ind 12160 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-xnn0 12511 df-z 12525 df-dec 12645 df-uz 12789 df-rp 12943 df-fz 13462 df-fzo 13609 df-seq 13964 df-exp 14024 df-hash 14293 df-word 14476 df-lsw 14525 df-concat 14533 df-s1 14559 df-substr 14604 df-pfx 14634 df-s2 14810 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-clim 15450 df-sum 15649 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ocomp 17241 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-0g 17404 df-gsum 17405 df-prds 17410 df-pws 17412 df-mre 17548 df-mrc 17549 df-mri 17550 df-acs 17551 df-proset 18260 df-drs 18261 df-poset 18279 df-ipo 18494 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-mhm 18751 df-submnd 18752 df-grp 18912 df-minusg 18913 df-sbg 18914 df-mulg 19044 df-subg 19099 df-ghm 19188 df-cntz 19292 df-cmn 19757 df-abl 19758 df-mgp 20122 df-rng 20134 df-ur 20163 df-ring 20216 df-cring 20217 df-oppr 20317 df-dvdsr 20337 df-unit 20338 df-invr 20368 df-nzr 20490 df-subrng 20523 df-subrg 20547 df-rgspn 20588 df-rlreg 20671 df-domn 20672 df-idom 20673 df-drng 20708 df-field 20709 df-sdrg 20764 df-lmod 20857 df-lss 20927 df-lsp 20967 df-lmhm 21017 df-lbs 21070 df-lvec 21098 df-sra 21168 df-rgmod 21169 df-cnfld 21353 df-zring 21427 df-dsmm 21712 df-frlm 21727 df-uvc 21763 df-dim 33744 df-fldext 33785 df-extdg 33786

This theorem is referenced by: fldextrspunfld 33820 fldextrspundgle 33822

W3C validator