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 33859

Description: Lemma for fldextrspunfld 33860. 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 20762	. . . . 5 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐽 ∈ DivRing)
4	1, 3	syl 17	. . . 4 ⊢ (𝜑 → 𝐽 ∈ DivRing)
5		fldextrspunfld.4	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
6		eqid 2739	. . . . . 6 ⊢ (𝐽 ↾_s 𝐹) = (𝐽 ↾_s 𝐹)
7	6	sdrgdrng 20762	. . . . 5 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → (𝐽 ↾_s 𝐹) ∈ DivRing)
8	5, 7	syl 17	. . . 4 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) ∈ DivRing)
9		sdrgsubrg 20763	. . . . . 6 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
10	1, 9	syl 17	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
11		fldextrspunfld.5	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
12		sdrgsubrg 20763	. . . . . . . 8 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
13	11, 12	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
14		fldextrspunfld.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
15		sdrgsubrg 20763	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐼) → 𝐹 ∈ (SubRing‘𝐼))
16	14, 15	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐼))
17		fldextrspunfld.i	. . . . . . . . 9 ⊢ 𝐼 = (𝐿 ↾_s 𝐺)
18	17	subsubrg 20570	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐿) → (𝐹 ∈ (SubRing‘𝐼) ↔ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺)))
19	18	biimpa 477	. . . . . . 7 ⊢ ((𝐺 ∈ (SubRing‘𝐿) ∧ 𝐹 ∈ (SubRing‘𝐼)) → (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺))
20	13, 16, 19	syl2anc 590	. . . . . 6 ⊢ (𝜑 → (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐺))
21	20	simpld 495	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿))
22		eqid 2739	. . . . . . . 8 ⊢ (Base‘𝐽) = (Base‘𝐽)
23	22	sdrgss 20765	. . . . . . 7 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
24	5, 23	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
25		eqid 2739	. . . . . . . . 9 ⊢ (Base‘𝐿) = (Base‘𝐿)
26	25	sdrgss 20765	. . . . . . . 8 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
27	1, 26	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
28	2, 25	ressbas2 17199	. . . . . . 7 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
29	27, 28	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
30	24, 29	sseqtrrd 3952	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ 𝐻)
31	2	subsubrg 20570	. . . . . 6 ⊢ (𝐻 ∈ (SubRing‘𝐿) → (𝐹 ∈ (SubRing‘𝐽) ↔ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐻)))
32	31	biimpar 478	. . . . 5 ⊢ ((𝐻 ∈ (SubRing‘𝐿) ∧ (𝐹 ∈ (SubRing‘𝐿) ∧ 𝐹 ⊆ 𝐻)) → 𝐹 ∈ (SubRing‘𝐽))
33	10, 21, 30, 32	syl12anc 842	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐽))
34		eqid 2739	. . . . 5 ⊢ ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹)
35	34, 6	sralvec 33769	. . . 4 ⊢ ((𝐽 ∈ DivRing ∧ (𝐽 ↾_s 𝐹) ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐽)) → ((subringAlg ‘𝐽)‘𝐹) ∈ LVec)
36	4, 8, 33, 35	syl3anc 1379	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ LVec)
37		eqid 2739	. . . 4 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
38	37	lbsex 21158	. . 3 ⊢ (((subringAlg ‘𝐽)‘𝐹) ∈ LVec → (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ≠ ∅)
39	36, 38	syl 17	. 2 ⊢ (𝜑 → (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ≠ ∅)
40		fldextrspunfld.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ Field)
41		fldidom 20743	. . . . . . . . . . . 12 ⊢ (𝐿 ∈ Field → 𝐿 ∈ IDomn)
42	40, 41	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ IDomn)
43	42	idomringd 20700	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ Ring)
44		eqidd 2740	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐿) = (Base‘𝐿))
45	25	sdrgss 20765	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
46	11, 45	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
47	46, 27	unssd 4121	. . . . . . . . . 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 20585	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝐿))
53	43, 44, 47, 49, 51	rgspnssid 20586	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ 𝐶)
54	53	unssad 4122	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ⊆ 𝐶)
55		fldextrspunfld.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐿 ↾_s 𝐶)
56	55	subsubrg 20570	. . . . . . . . . 10 ⊢ (𝐶 ∈ (SubRing‘𝐿) → (𝐺 ∈ (SubRing‘𝐸) ↔ (𝐺 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶)))
57	56	biimpar 478	. . . . . . . . 9 ⊢ ((𝐶 ∈ (SubRing‘𝐿) ∧ (𝐺 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶)) → 𝐺 ∈ (SubRing‘𝐸))
58	52, 13, 54, 57	syl12anc 842	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐸))
59		eqid 2739	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺)
60	59	sralmod 21177	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐸) → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
61	58, 60	syl 17	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
62		ressabs 17209	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (SubRing‘𝐿) ∧ 𝐺 ⊆ 𝐶) → ((𝐿 ↾_s 𝐶) ↾_s 𝐺) = (𝐿 ↾_s 𝐺))
63	52, 54, 62	syl2anc 590	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 ↾_s 𝐶) ↾_s 𝐺) = (𝐿 ↾_s 𝐺))
64	55	oveq1i 7366	. . . . . . . . . 10 ⊢ (𝐸 ↾_s 𝐺) = ((𝐿 ↾_s 𝐶) ↾_s 𝐺)
65	63, 64, 17	3eqtr4g 2799	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s 𝐺) = 𝐼)
66		eqidd 2740	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺))
67	25	subrgss 20544	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ (SubRing‘𝐿) → 𝐶 ⊆ (Base‘𝐿))
68	52, 67	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ⊆ (Base‘𝐿))
69	55, 25	ressbas2 17199	. . . . . . . . . . . . 13 ⊢ (𝐶 ⊆ (Base‘𝐿) → 𝐶 = (Base‘𝐸))
70	68, 69	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 = (Base‘𝐸))
71	53, 70	sseqtrd 3951	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 ∪ 𝐻) ⊆ (Base‘𝐸))
72	71	unssad 4122	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐸))
73	66, 72	srasca 21170	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾_s 𝐺) = (Scalar‘((subringAlg ‘𝐸)‘𝐺)))
74	65, 73	eqtr3d 2776	. . . . . . . 8 ⊢ (𝜑 → 𝐼 = (Scalar‘((subringAlg ‘𝐸)‘𝐺)))
75	17	sdrgdrng 20762	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐼 ∈ DivRing)
76	11, 75	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ DivRing)
77	74, 76	eqeltrrd 2840	. . . . . . 7 ⊢ (𝜑 → (Scalar‘((subringAlg ‘𝐸)‘𝐺)) ∈ DivRing)
78		eqid 2739	. . . . . . . 8 ⊢ (Scalar‘((subringAlg ‘𝐸)‘𝐺)) = (Scalar‘((subringAlg ‘𝐸)‘𝐺))
79	78	islvec 21094	. . . . . . 7 ⊢ (((subringAlg ‘𝐸)‘𝐺) ∈ LVec ↔ (((subringAlg ‘𝐸)‘𝐺) ∈ LMod ∧ (Scalar‘((subringAlg ‘𝐸)‘𝐺)) ∈ DivRing))
80	61, 77, 79	sylanbrc 589	. . . . . 6 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) ∈ LVec)
81		eqid 2739	. . . . . . 7 ⊢ (LBasis‘((subringAlg ‘𝐸)‘𝐺)) = (LBasis‘((subringAlg ‘𝐸)‘𝐺))
82	81	lbsex 21158	. . . . . 6 ⊢ (((subringAlg ‘𝐸)‘𝐺) ∈ LVec → (LBasis‘((subringAlg ‘𝐸)‘𝐺)) ≠ ∅)
83	80, 82	syl 17	. . . . 5 ⊢ (𝜑 → (LBasis‘((subringAlg ‘𝐸)‘𝐺)) ≠ ∅)
84	83	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (LBasis‘((subringAlg ‘𝐸)‘𝐺)) ≠ ∅)
85	80	ad2antrr 732	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) ∈ LVec)
86		simpr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺)))
87	81	dimval 33785	. . . . . 6 ⊢ ((((subringAlg ‘𝐸)‘𝐺) ∈ LVec ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) = (♯‘𝑐))
88	85, 86, 87	syl2anc 590	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) = (♯‘𝑐))
89		eqid 2739	. . . . . 6 ⊢ (Base‘((subringAlg ‘𝐸)‘𝐺)) = (Base‘((subringAlg ‘𝐸)‘𝐺))
90		eqid 2739	. . . . . 6 ⊢ (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘((subringAlg ‘𝐸)‘𝐺))
91		eqid 2739	. . . . . . . . . . . 12 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
92	91, 37	lbsss 21067	. . . . . . . . . . 11 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
93	92	ad2antlr 733	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
94		eqidd 2740	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
95	94, 24	srabase 21167	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
96	29, 95	eqtrd 2774	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
97	96	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
98	93, 97	sseqtrrd 3952	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ 𝐻)
99	53	unssbd 4123	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ⊆ 𝐶)
100	99	ad2antrr 732	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐻 ⊆ 𝐶)
101	98, 100	sstrd 3925	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ 𝐶)
102	70	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐶 = (Base‘𝐸))
103	101, 102	sseqtrd 3951	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘𝐸))
104		eqidd 2740	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) = ((subringAlg ‘𝐸)‘𝐺))
105	72	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐺 ⊆ (Base‘𝐸))
106	104, 105	srabase 21167	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘𝐺)))
107	103, 106	sseqtrd 3951	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
108	61	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((subringAlg ‘𝐸)‘𝐺) ∈ LMod)
109	89, 90	lspssv 20973	. . . . . . . 8 ⊢ ((((subringAlg ‘𝐸)‘𝐺) ∈ LMod ∧ 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
110	108, 107, 109	syl2anc 590	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) ⊆ (Base‘((subringAlg ‘𝐸)‘𝐺)))
111		fldextrspunfld.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (𝐿 ↾_s 𝐹)
112	40	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐿 ∈ Field)
113	14	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐹 ∈ (SubDRing‘𝐼))
114	5	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐹 ∈ (SubDRing‘𝐽))
115	11	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐺 ∈ (SubDRing‘𝐿))
116	1	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ∈ (SubDRing‘𝐿))
117		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
118		fldsdrgfld 20770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐿 ∈ Field ∧ 𝐻 ∈ (SubDRing‘𝐿)) → (𝐿 ↾_s 𝐻) ∈ Field)
119	40, 1, 118	syl2anc 590	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 ↾_s 𝐻) ∈ Field)
120	2, 119	eqeltrid 2843	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ Field)
121		ressabs 17209	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐻 ∈ (SubDRing‘𝐿) ∧ 𝐹 ⊆ 𝐻) → ((𝐿 ↾_s 𝐻) ↾_s 𝐹) = (𝐿 ↾_s 𝐹))
122	1, 30, 121	syl2anc 590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐿 ↾_s 𝐻) ↾_s 𝐹) = (𝐿 ↾_s 𝐹))
123	2	oveq1i 7366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ↾_s 𝐹) = ((𝐿 ↾_s 𝐻) ↾_s 𝐹)
124	122, 123, 111	3eqtr4g 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) = 𝐾)
125		fldsdrgfld 20770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐽)) → (𝐽 ↾_s 𝐹) ∈ Field)
126	120, 5, 125	syl2anc 590	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) ∈ Field)
127	124, 126	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ Field)
128	30, 27	sstrd 3925	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
129	111, 25	ressbas2 17199	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ⊆ (Base‘𝐿) → 𝐹 = (Base‘𝐾))
130	128, 129	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
131	130	oveq2d 7372	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐽 ↾_s 𝐹) = (𝐽 ↾_s (Base‘𝐾)))
132	124, 131	eqtr3d 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 = (𝐽 ↾_s (Base‘𝐾)))
133	130, 33	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐽))
134		brfldext 33829	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ Field ∧ 𝐾 ∈ Field) → (𝐽/_FldExt𝐾 ↔ (𝐾 = (𝐽 ↾_s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐽))))
135	134	biimpar 478	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Field ∧ 𝐾 ∈ Field) ∧ (𝐾 = (𝐽 ↾_s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐽))) → 𝐽/_FldExt𝐾)
136	120, 127, 132, 133, 135	syl22anc 844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐽/_FldExt𝐾)
137	136	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐽/_FldExt𝐾)
138		extdgval 33837	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽/_FldExt𝐾 → (𝐽[:]𝐾) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
139	137, 138	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
140	130	fveq2d 6831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘(Base‘𝐾)))
141	140	fveq2d 6831	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
142	141	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (dim‘((subringAlg ‘𝐽)‘(Base‘𝐾))))
143	37	dimval 33785	. . . . . . . . . . . . . . . . 17 ⊢ ((((subringAlg ‘𝐽)‘𝐹) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (♯‘𝑏))
144	36, 143	sylan 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐽)‘𝐹)) = (♯‘𝑏))
145	139, 142, 144	3eqtr2d 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) = (♯‘𝑏))
146		fldextrspunfld.7	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ₀)
147	146	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (𝐽[:]𝐾) ∈ ℕ₀)
148	145, 147	eqeltrrd 2840	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (♯‘𝑏) ∈ ℕ₀)
149		hashclb 14311	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → (𝑏 ∈ Fin ↔ (♯‘𝑏) ∈ ℕ₀))
150	149	biimpar 478	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) ∧ (♯‘𝑏) ∈ ℕ₀) → 𝑏 ∈ Fin)
151	117, 148, 150	syl2anc 590	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ∈ Fin)
152	111, 17, 2, 112, 113, 114, 115, 116, 48, 50, 55, 117, 151	fldextrspunlsp 33858	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
153	152	eqimssd 3971	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
154	25, 55, 68, 54, 40	resssra 33771	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐺) = (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))
155	154	fveq2d 6831	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)))
156	155	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (LSpan‘((subringAlg ‘𝐸)‘𝐺)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)))
157	156	fveq1d 6829	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) = ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏))
158	115, 12	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐺 ∈ (SubRing‘𝐿))
159		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺)
160	159	sralmod 21177	. . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
164	162, 163	sseqtrrd 3952	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ 𝐻)
165	116, 26	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ⊆ (Base‘𝐿))
166	164, 165	sstrd 3925	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘𝐿))
167		eqidd 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺))
168	167, 46	srabase 21167	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
169	168	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
170	166, 169	sseqtrd 3951	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺)))
171		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ (Base‘((subringAlg ‘𝐿)‘𝐺)) = (Base‘((subringAlg ‘𝐿)‘𝐺))
172		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)) = (LSubSp‘((subringAlg ‘𝐿)‘𝐺))
173		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ (LSpan‘((subringAlg ‘𝐿)‘𝐺)) = (LSpan‘((subringAlg ‘𝐿)‘𝐺))
174	171, 172, 173	lspcl 20966	. . . . . . . . . . . . . . 15 ⊢ ((((subringAlg ‘𝐿)‘𝐺) ∈ LMod ∧ 𝑏 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
175	161, 170, 174	syl2anc 590	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
176	152, 175	eqeltrd 2839	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)))
177	99	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐻 ⊆ 𝐶)
178	164, 177	sstrd 3925	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝑏 ⊆ 𝐶)
179		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶) = (((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)
180		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶)) = (LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))
181	179, 173, 180, 172	lsslsp 21005	. . . . . . . . . . . . 13 ⊢ ((((subringAlg ‘𝐿)‘𝐺) ∈ LMod ∧ 𝐶 ∈ (LSubSp‘((subringAlg ‘𝐿)‘𝐺)) ∧ 𝑏 ⊆ 𝐶) → ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏) = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
182	161, 176, 178, 181	syl3anc 1379	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘(((subringAlg ‘𝐿)‘𝐺) ↾_s 𝐶))‘𝑏) = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏))
183	157, 182	eqtr2d 2775	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝑏) = ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
184	153, 183	sseqtrd 3951	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
185	184	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → 𝐶 ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
186	102, 185	eqsstrrd 3950	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘𝐸) ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
187	106, 186	eqsstrrd 3950	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (Base‘((subringAlg ‘𝐸)‘𝐺)) ⊆ ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏))
188	110, 187	eqssd 3932	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → ((LSpan‘((subringAlg ‘𝐸)‘𝐺))‘𝑏) = (Base‘((subringAlg ‘𝐸)‘𝐺)))
189	89, 81, 90, 85, 86, 107, 188	lbslelsp 33782	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (♯‘𝑐) ≤ (♯‘𝑏))
190	88, 189	eqbrtrd 5094	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑐 ∈ (LBasis‘((subringAlg ‘𝐸)‘𝐺))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (♯‘𝑏))
191	84, 190	n0limd 32559	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (♯‘𝑏))
192	191, 145	breqtrrd 5100	. 2 ⊢ ((𝜑 ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))
193	39, 192	n0limd 32559	1 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∪ cun 3881 ⊆ wss 3883 ∅c0 4261 class class class wbr 5072 ‘cfv 6485 (class class class)co 7356 Fincfn 8883 ≤ cle 11171 ℕ₀cn0 12428 ♯chash 14283 Basecbs 17170 ↾_s cress 17191 Scalarcsca 17214 SubRingcsubrg 20541 RingSpancrgspn 20582 IDomncidom 20665 DivRingcdr 20701 Fieldcfield 20702 SubDRingcsdrg 20758 LModclmod 20850 LSubSpclss 20921 LSpanclspn 20961 LBasisclbs 21064 LVecclvec 21092 subringAlg csra 21161 dimcldim 33783 /_FldExtcfldext 33822 [:]cextdg 33824

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-reg 9497 ax-inf2 9553 ax-ac2 10376 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107 ax-addf 11108

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-iin 4924 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-isom 6494 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-rpss 7666 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-tpos 8166 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-er 8633 df-map 8765 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9265 df-sup 9345 df-inf 9346 df-oi 9415 df-r1 9679 df-rank 9680 df-dju 9816 df-card 9854 df-acn 9857 df-ac 10029 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-ind 12151 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-xnn0 12502 df-z 12516 df-dec 12636 df-uz 12780 df-rp 12934 df-fz 13453 df-fzo 13600 df-seq 13955 df-exp 14015 df-hash 14284 df-word 14467 df-lsw 14516 df-concat 14524 df-s1 14550 df-substr 14595 df-pfx 14625 df-s2 14801 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-clim 15441 df-sum 15640 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-starv 17226 df-sca 17227 df-vsca 17228 df-ip 17229 df-tset 17230 df-ple 17231 df-ocomp 17232 df-ds 17233 df-unif 17234 df-hom 17235 df-cco 17236 df-0g 17395 df-gsum 17396 df-prds 17401 df-pws 17403 df-mre 17539 df-mrc 17540 df-mri 17541 df-acs 17542 df-proset 18251 df-drs 18252 df-poset 18270 df-ipo 18485 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-mhm 18742 df-submnd 18743 df-grp 18903 df-minusg 18904 df-sbg 18905 df-mulg 19035 df-subg 19090 df-ghm 19179 df-cntz 19283 df-cmn 19748 df-abl 19749 df-mgp 20113 df-rng 20125 df-ur 20154 df-ring 20207 df-cring 20208 df-oppr 20308 df-dvdsr 20328 df-unit 20329 df-invr 20359 df-nzr 20485 df-subrng 20518 df-subrg 20542 df-rgspn 20583 df-rlreg 20666 df-domn 20667 df-idom 20668 df-drng 20703 df-field 20704 df-sdrg 20759 df-lmod 20852 df-lss 20922 df-lsp 20962 df-lmhm 21012 df-lbs 21065 df-lvec 21093 df-sra 21163 df-rgmod 21164 df-cnfld 21348 df-zring 21422 df-dsmm 21707 df-frlm 21722 df-uvc 21758 df-dim 33784 df-fldext 33825 df-extdg 33826

This theorem is referenced by: fldextrspunfld 33860 fldextrspundgle 33862

W3C validator