fldextrspunlem1

	Ref	Expression
Hypotheses	fldextrspunfld.k	$⊢ K = L ↾_{𝑠} F$
	fldextrspunfld.i	$⊢ I = L ↾_{𝑠} G$
	fldextrspunfld.j	$⊢ J = L ↾_{𝑠} H$
	fldextrspunfld.2	$⊢ φ \to L \in Field$
	fldextrspunfld.3	$⊢ φ \to F \in SubDRing (I)$
	fldextrspunfld.4	$⊢ φ \to F \in SubDRing (J)$
	fldextrspunfld.5	$⊢ φ \to G \in SubDRing (L)$
	fldextrspunfld.6	$⊢ φ \to H \in SubDRing (L)$
	fldextrspunfld.7	$⊢ φ \to J [. : .] K \in ℕ_{0}$
	fldextrspunfld.n	$⊢ N = RingSpan (L)$
	fldextrspunfld.c	$⊢ C = N (G \cup H)$
	fldextrspunfld.e	$⊢ E = L ↾_{𝑠} C$
Assertion	fldextrspunlem1	$⊢ φ \to \dim (subringAlg (E) (G)) \leq J [. : .] K$

Proof

Step	Hyp	Ref	Expression
1		fldextrspunfld.k	$⊢ K = L ↾_{𝑠} F$
2		fldextrspunfld.i	$⊢ I = L ↾_{𝑠} G$
3		fldextrspunfld.j	$⊢ J = L ↾_{𝑠} H$
4		fldextrspunfld.2	$⊢ φ \to L \in Field$
5		fldextrspunfld.3	$⊢ φ \to F \in SubDRing (I)$
6		fldextrspunfld.4	$⊢ φ \to F \in SubDRing (J)$
7		fldextrspunfld.5	$⊢ φ \to G \in SubDRing (L)$
8		fldextrspunfld.6	$⊢ φ \to H \in SubDRing (L)$
9		fldextrspunfld.7	$⊢ φ \to J [. : .] K \in ℕ_{0}$
10		fldextrspunfld.n	$⊢ N = RingSpan (L)$
11		fldextrspunfld.c	$⊢ C = N (G \cup H)$
12		fldextrspunfld.e	$⊢ E = L ↾_{𝑠} C$
13	3	sdrgdrng	$⊢ H \in SubDRing (L) \to J \in DivRing$
14	8 13	syl	$⊢ φ \to J \in DivRing$
15		eqid	$⊢ J ↾_{𝑠} F = J ↾_{𝑠} F$
16	15	sdrgdrng	$⊢ F \in SubDRing (J) \to J ↾_{𝑠} F \in DivRing$
17	6 16	syl	$⊢ φ \to J ↾_{𝑠} F \in DivRing$
18		sdrgsubrg	$⊢ H \in SubDRing (L) \to H \in SubRing (L)$
19	8 18	syl	$⊢ φ \to H \in SubRing (L)$
20		sdrgsubrg	$⊢ G \in SubDRing (L) \to G \in SubRing (L)$
21	7 20	syl	$⊢ φ \to G \in SubRing (L)$
22		sdrgsubrg	$⊢ F \in SubDRing (I) \to F \in SubRing (I)$
23	5 22	syl	$⊢ φ \to F \in SubRing (I)$
24	2	subsubrg	$⊢ G \in SubRing (L) \to (F \in SubRing (I) \leftrightarrow (F \in SubRing (L) \land F \subseteq G))$
25	24	biimpa	$⊢ (G \in SubRing (L) \land F \in SubRing (I)) \to (F \in SubRing (L) \land F \subseteq G)$
26	21 23 25	syl2anc	$⊢ φ \to (F \in SubRing (L) \land F \subseteq G)$
27	26	simpld	$⊢ φ \to F \in SubRing (L)$
28		eqid	$⊢ {Base}_{J} = {Base}_{J}$
29	28	sdrgss	$⊢ F \in SubDRing (J) \to F \subseteq {Base}_{J}$
30	6 29	syl	$⊢ φ \to F \subseteq {Base}_{J}$
31		eqid	$⊢ {Base}_{L} = {Base}_{L}$
32	31	sdrgss	$⊢ H \in SubDRing (L) \to H \subseteq {Base}_{L}$
33	8 32	syl	$⊢ φ \to H \subseteq {Base}_{L}$
34	3 31	ressbas2	$⊢ H \subseteq {Base}_{L} \to H = {Base}_{J}$
35	33 34	syl	$⊢ φ \to H = {Base}_{J}$
36	30 35	sseqtrrd	$⊢ φ \to F \subseteq H$
37	3	subsubrg	$⊢ H \in SubRing (L) \to (F \in SubRing (J) \leftrightarrow (F \in SubRing (L) \land F \subseteq H))$
38	37	biimpar	$⊢ (H \in SubRing (L) \land (F \in SubRing (L) \land F \subseteq H)) \to F \in SubRing (J)$
39	19 27 36 38	syl12anc	$⊢ φ \to F \in SubRing (J)$
40		eqid	$⊢ subringAlg (J) (F) = subringAlg (J) (F)$
41	40 15	sralvec	$⊢ (J \in DivRing \land J ↾_{𝑠} F \in DivRing \land F \in SubRing (J)) \to subringAlg (J) (F) \in LVec$
42	14 17 39 41	syl3anc	$⊢ φ \to subringAlg (J) (F) \in LVec$
43		eqid	$⊢ LBasis (subringAlg (J) (F)) = LBasis (subringAlg (J) (F))$
44	43	lbsex	$⊢ subringAlg (J) (F) \in LVec \to LBasis (subringAlg (J) (F)) \neq \emptyset$
45	42 44	syl	$⊢ φ \to LBasis (subringAlg (J) (F)) \neq \emptyset$
46		fldidom	$⊢ L \in Field \to L \in IDomn$
47	4 46	syl	$⊢ φ \to L \in IDomn$
48	47	idomringd	$⊢ φ \to L \in Ring$
49		eqidd	$⊢ φ \to {Base}_{L} = {Base}_{L}$
50	31	sdrgss	$⊢ G \in SubDRing (L) \to G \subseteq {Base}_{L}$
51	7 50	syl	$⊢ φ \to G \subseteq {Base}_{L}$
52	51 33	unssd	$⊢ φ \to G \cup H \subseteq {Base}_{L}$
53	10	a1i	$⊢ φ \to N = RingSpan (L)$
54	11	a1i	$⊢ φ \to C = N (G \cup H)$
55	48 49 52 53 54	rgspncl	$⊢ φ \to C \in SubRing (L)$
56	48 49 52 53 54	rgspnssid	$⊢ φ \to G \cup H \subseteq C$
57	56	unssad	$⊢ φ \to G \subseteq C$
58	12	subsubrg	$⊢ C \in SubRing (L) \to (G \in SubRing (E) \leftrightarrow (G \in SubRing (L) \land G \subseteq C))$
59	58	biimpar	$⊢ (C \in SubRing (L) \land (G \in SubRing (L) \land G \subseteq C)) \to G \in SubRing (E)$
60	55 21 57 59	syl12anc	$⊢ φ \to G \in SubRing (E)$
61		eqid	$⊢ subringAlg (E) (G) = subringAlg (E) (G)$
62	61	sralmod	$⊢ G \in SubRing (E) \to subringAlg (E) (G) \in LMod$
63	60 62	syl	$⊢ φ \to subringAlg (E) (G) \in LMod$
64		ressabs	$⊢ (C \in SubRing (L) \land G \subseteq C) \to (L ↾_{𝑠} C) ↾_{𝑠} G = L ↾_{𝑠} G$
65	55 57 64	syl2anc	$⊢ φ \to (L ↾_{𝑠} C) ↾_{𝑠} G = L ↾_{𝑠} G$
66	12	oveq1i	$⊢ E ↾_{𝑠} G = (L ↾_{𝑠} C) ↾_{𝑠} G$
67	65 66 2	3eqtr4g	$⊢ φ \to E ↾_{𝑠} G = I$
68		eqidd	$⊢ φ \to subringAlg (E) (G) = subringAlg (E) (G)$
69	31	subrgss	$⊢ C \in SubRing (L) \to C \subseteq {Base}_{L}$
70	55 69	syl	$⊢ φ \to C \subseteq {Base}_{L}$
71	12 31	ressbas2	$⊢ C \subseteq {Base}_{L} \to C = {Base}_{E}$
72	70 71	syl	$⊢ φ \to C = {Base}_{E}$
73	56 72	sseqtrd	$⊢ φ \to G \cup H \subseteq {Base}_{E}$
74	73	unssad	$⊢ φ \to G \subseteq {Base}_{E}$
75	68 74	srasca	$⊢ φ \to E ↾_{𝑠} G = Scalar (subringAlg (E) (G))$
76	67 75	eqtr3d	$⊢ φ \to I = Scalar (subringAlg (E) (G))$
77	2	sdrgdrng	$⊢ G \in SubDRing (L) \to I \in DivRing$
78	7 77	syl	$⊢ φ \to I \in DivRing$
79	76 78	eqeltrrd	$⊢ φ \to Scalar (subringAlg (E) (G)) \in DivRing$
80		eqid	$⊢ Scalar (subringAlg (E) (G)) = Scalar (subringAlg (E) (G))$
81	80	islvec	$⊢ subringAlg (E) (G) \in LVec \leftrightarrow (subringAlg (E) (G) \in LMod \land Scalar (subringAlg (E) (G)) \in DivRing)$
82	63 79 81	sylanbrc	$⊢ φ \to subringAlg (E) (G) \in LVec$
83		eqid	$⊢ LBasis (subringAlg (E) (G)) = LBasis (subringAlg (E) (G))$
84	83	lbsex	$⊢ subringAlg (E) (G) \in LVec \to LBasis (subringAlg (E) (G)) \neq \emptyset$
85	82 84	syl	$⊢ φ \to LBasis (subringAlg (E) (G)) \neq \emptyset$
86	85	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to LBasis (subringAlg (E) (G)) \neq \emptyset$
87	82	ad2antrr	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to subringAlg (E) (G) \in LVec$
88		simpr	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to c \in LBasis (subringAlg (E) (G))$
89	83	dimval	$⊢ (subringAlg (E) (G) \in LVec \land c \in LBasis (subringAlg (E) (G))) \to \dim (subringAlg (E) (G)) = \|c\|$
90	87 88 89	syl2anc	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to \dim (subringAlg (E) (G)) = \|c\|$
91		eqid	$⊢ {Base}_{subringAlg (E) (G)} = {Base}_{subringAlg (E) (G)}$
92		eqid	$⊢ LSpan (subringAlg (E) (G)) = LSpan (subringAlg (E) (G))$
93		eqid	$⊢ {Base}_{subringAlg (J) (F)} = {Base}_{subringAlg (J) (F)}$
94	93 43	lbsss	$⊢ b \in LBasis (subringAlg (J) (F)) \to b \subseteq {Base}_{subringAlg (J) (F)}$
95	94	ad2antlr	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to b \subseteq {Base}_{subringAlg (J) (F)}$
96		eqidd	$⊢ φ \to subringAlg (J) (F) = subringAlg (J) (F)$
97	96 30	srabase	$⊢ φ \to {Base}_{J} = {Base}_{subringAlg (J) (F)}$
98	35 97	eqtrd	$⊢ φ \to H = {Base}_{subringAlg (J) (F)}$
99	98	ad2antrr	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to H = {Base}_{subringAlg (J) (F)}$
100	95 99	sseqtrrd	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to b \subseteq H$
101	56	unssbd	$⊢ φ \to H \subseteq C$
102	101	ad2antrr	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to H \subseteq C$
103	100 102	sstrd	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to b \subseteq C$
104	72	ad2antrr	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to C = {Base}_{E}$
105	103 104	sseqtrd	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to b \subseteq {Base}_{E}$
106		eqidd	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to subringAlg (E) (G) = subringAlg (E) (G)$
107	74	ad2antrr	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to G \subseteq {Base}_{E}$
108	106 107	srabase	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to {Base}_{E} = {Base}_{subringAlg (E) (G)}$
109	105 108	sseqtrd	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to b \subseteq {Base}_{subringAlg (E) (G)}$
110	63	ad2antrr	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to subringAlg (E) (G) \in LMod$
111	91 92	lspssv	$⊢ (subringAlg (E) (G) \in LMod \land b \subseteq {Base}_{subringAlg (E) (G)}) \to LSpan (subringAlg (E) (G)) (b) \subseteq {Base}_{subringAlg (E) (G)}$
112	110 109 111	syl2anc	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to LSpan (subringAlg (E) (G)) (b) \subseteq {Base}_{subringAlg (E) (G)}$
113	4	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to L \in Field$
114	5	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to F \in SubDRing (I)$
115	6	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to F \in SubDRing (J)$
116	7	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to G \in SubDRing (L)$
117	8	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to H \in SubDRing (L)$
118		simpr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to b \in LBasis (subringAlg (J) (F))$
119		fldsdrgfld	$⊢ (L \in Field \land H \in SubDRing (L)) \to L ↾_{𝑠} H \in Field$
120	4 8 119	syl2anc	$⊢ φ \to L ↾_{𝑠} H \in Field$
121	3 120	eqeltrid	$⊢ φ \to J \in Field$
122		ressabs	$⊢ (H \in SubDRing (L) \land F \subseteq H) \to (L ↾_{𝑠} H) ↾_{𝑠} F = L ↾_{𝑠} F$
123	8 36 122	syl2anc	$⊢ φ \to (L ↾_{𝑠} H) ↾_{𝑠} F = L ↾_{𝑠} F$
124	3	oveq1i	$⊢ J ↾_{𝑠} F = (L ↾_{𝑠} H) ↾_{𝑠} F$
125	123 124 1	3eqtr4g	$⊢ φ \to J ↾_{𝑠} F = K$
126		fldsdrgfld	$⊢ (J \in Field \land F \in SubDRing (J)) \to J ↾_{𝑠} F \in Field$
127	121 6 126	syl2anc	$⊢ φ \to J ↾_{𝑠} F \in Field$
128	125 127	eqeltrrd	$⊢ φ \to K \in Field$
129	36 33	sstrd	$⊢ φ \to F \subseteq {Base}_{L}$
130	1 31	ressbas2	$⊢ F \subseteq {Base}_{L} \to F = {Base}_{K}$
131	129 130	syl	$⊢ φ \to F = {Base}_{K}$
132	131	oveq2d	$⊢ φ \to J ↾_{𝑠} F = J ↾_{𝑠} {Base}_{K}$
133	125 132	eqtr3d	$⊢ φ \to K = J ↾_{𝑠} {Base}_{K}$
134	131 39	eqeltrrd	$⊢ φ \to {Base}_{K} \in SubRing (J)$
135		brfldext	$⊢ (J \in Field \land K \in Field) \to (J /_{FldExt} K \leftrightarrow (K = J ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (J)))$
136	135	biimpar	$⊢ ((J \in Field \land K \in Field) \land (K = J ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (J))) \to J /_{FldExt} K$
137	121 128 133 134 136	syl22anc	$⊢ φ \to J /_{FldExt} K$
138	137	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to J /_{FldExt} K$
139		extdgval	$⊢ J /_{FldExt} K \to J [. : .] K = \dim (subringAlg (J) ({Base}_{K}))$
140	138 139	syl	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to J [. : .] K = \dim (subringAlg (J) ({Base}_{K}))$
141	131	fveq2d	$⊢ φ \to subringAlg (J) (F) = subringAlg (J) ({Base}_{K})$
142	141	fveq2d	$⊢ φ \to \dim (subringAlg (J) (F)) = \dim (subringAlg (J) ({Base}_{K}))$
143	142	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to \dim (subringAlg (J) (F)) = \dim (subringAlg (J) ({Base}_{K}))$
144	43	dimval	$⊢ (subringAlg (J) (F) \in LVec \land b \in LBasis (subringAlg (J) (F))) \to \dim (subringAlg (J) (F)) = \|b\|$
145	42 144	sylan	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to \dim (subringAlg (J) (F)) = \|b\|$
146	140 143 145	3eqtr2d	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to J [. : .] K = \|b\|$
147	9	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to J [. : .] K \in ℕ_{0}$
148	146 147	eqeltrrd	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to \|b\| \in ℕ_{0}$
149		hashclb	$⊢ b \in LBasis (subringAlg (J) (F)) \to (b \in Fin \leftrightarrow \|b\| \in ℕ_{0})$
150	149	biimpar	$⊢ (b \in LBasis (subringAlg (J) (F)) \land \|b\| \in ℕ_{0}) \to b \in Fin$
151	118 148 150	syl2anc	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to b \in Fin$
152	1 2 3 113 114 115 116 117 10 11 12 118 151	fldextrspunlsp	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to C = LSpan (subringAlg (L) (G)) (b)$
153	152	eqimssd	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to C \subseteq LSpan (subringAlg (L) (G)) (b)$
154	31 12 70 57 4	resssra	$⊢ φ \to subringAlg (E) (G) = subringAlg (L) (G) ↾_{𝑠} C$
155	154	fveq2d	$⊢ φ \to LSpan (subringAlg (E) (G)) = LSpan (subringAlg (L) (G) ↾_{𝑠} C)$
156	155	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to LSpan (subringAlg (E) (G)) = LSpan (subringAlg (L) (G) ↾_{𝑠} C)$
157	156	fveq1d	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to LSpan (subringAlg (E) (G)) (b) = LSpan (subringAlg (L) (G) ↾_{𝑠} C) (b)$
158	116 20	syl	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to G \in SubRing (L)$
159		eqid	$⊢ subringAlg (L) (G) = subringAlg (L) (G)$
160	159	sralmod	$⊢ G \in SubRing (L) \to subringAlg (L) (G) \in LMod$
161	158 160	syl	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to subringAlg (L) (G) \in LMod$
162	118 94	syl	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to b \subseteq {Base}_{subringAlg (J) (F)}$
163	98	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to H = {Base}_{subringAlg (J) (F)}$
164	162 163	sseqtrrd	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to b \subseteq H$
165	117 32	syl	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to H \subseteq {Base}_{L}$
166	164 165	sstrd	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to b \subseteq {Base}_{L}$
167		eqidd	$⊢ φ \to subringAlg (L) (G) = subringAlg (L) (G)$
168	167 51	srabase	$⊢ φ \to {Base}_{L} = {Base}_{subringAlg (L) (G)}$
169	168	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to {Base}_{L} = {Base}_{subringAlg (L) (G)}$
170	166 169	sseqtrd	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to b \subseteq {Base}_{subringAlg (L) (G)}$
171		eqid	$⊢ {Base}_{subringAlg (L) (G)} = {Base}_{subringAlg (L) (G)}$
172		eqid	$⊢ LSubSp (subringAlg (L) (G)) = LSubSp (subringAlg (L) (G))$
173		eqid	$⊢ LSpan (subringAlg (L) (G)) = LSpan (subringAlg (L) (G))$
174	171 172 173	lspcl	$⊢ (subringAlg (L) (G) \in LMod \land b \subseteq {Base}_{subringAlg (L) (G)}) \to LSpan (subringAlg (L) (G)) (b) \in LSubSp (subringAlg (L) (G))$
175	161 170 174	syl2anc	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to LSpan (subringAlg (L) (G)) (b) \in LSubSp (subringAlg (L) (G))$
176	152 175	eqeltrd	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to C \in LSubSp (subringAlg (L) (G))$
177	101	adantr	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to H \subseteq C$
178	164 177	sstrd	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to b \subseteq C$
179		eqid	$⊢ subringAlg (L) (G) ↾_{𝑠} C = subringAlg (L) (G) ↾_{𝑠} C$
180		eqid	$⊢ LSpan (subringAlg (L) (G) ↾_{𝑠} C) = LSpan (subringAlg (L) (G) ↾_{𝑠} C)$
181	179 173 180 172	lsslsp	$⊢ (subringAlg (L) (G) \in LMod \land C \in LSubSp (subringAlg (L) (G)) \land b \subseteq C) \to LSpan (subringAlg (L) (G) ↾_{𝑠} C) (b) = LSpan (subringAlg (L) (G)) (b)$
182	161 176 178 181	syl3anc	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to LSpan (subringAlg (L) (G) ↾_{𝑠} C) (b) = LSpan (subringAlg (L) (G)) (b)$
183	157 182	eqtr2d	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to LSpan (subringAlg (L) (G)) (b) = LSpan (subringAlg (E) (G)) (b)$
184	153 183	sseqtrd	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to C \subseteq LSpan (subringAlg (E) (G)) (b)$
185	184	adantr	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to C \subseteq LSpan (subringAlg (E) (G)) (b)$
186	104 185	eqsstrrd	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to {Base}_{E} \subseteq LSpan (subringAlg (E) (G)) (b)$
187	108 186	eqsstrrd	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to {Base}_{subringAlg (E) (G)} \subseteq LSpan (subringAlg (E) (G)) (b)$
188	112 187	eqssd	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to LSpan (subringAlg (E) (G)) (b) = {Base}_{subringAlg (E) (G)}$
189	91 83 92 87 88 109 188	lbslelsp	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to \|c\| \leq \|b\|$
190	90 189	eqbrtrd	$⊢ ((φ \land b \in LBasis (subringAlg (J) (F))) \land c \in LBasis (subringAlg (E) (G))) \to \dim (subringAlg (E) (G)) \leq \|b\|$
191	86 190	n0limd	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to \dim (subringAlg (E) (G)) \leq \|b\|$
192	191 146	breqtrrd	$⊢ (φ \land b \in LBasis (subringAlg (J) (F))) \to \dim (subringAlg (E) (G)) \leq J [. : .] K$
193	45 192	n0limd	$⊢ φ \to \dim (subringAlg (E) (G)) \leq J [. : .] K$

Metamath Proof Explorer

Theorem fldextrspunlem1

Proof