This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fldextrspunlem1

Description: Lemma for fldextrspunfld . Part of the proof of Proposition 5, Chapter 5, of BourbakiAlg2 p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses fldextrspunfld.k 
|- K = ( L |`s F )
fldextrspunfld.i 
|- I = ( L |`s G )
fldextrspunfld.j 
|- J = ( L |`s H )
fldextrspunfld.2 
|- ( ph -> L e. Field )
fldextrspunfld.3 
|- ( ph -> F e. ( SubDRing ` I ) )
fldextrspunfld.4 
|- ( ph -> F e. ( SubDRing ` J ) )
fldextrspunfld.5 
|- ( ph -> G e. ( SubDRing ` L ) )
fldextrspunfld.6 
|- ( ph -> H e. ( SubDRing ` L ) )
fldextrspunfld.7 
|- ( ph -> ( J [:] K ) e. NN0 )
fldextrspunfld.n 
|- N = ( RingSpan ` L )
fldextrspunfld.c 
|- C = ( N ` ( G u. H ) )
fldextrspunfld.e 
|- E = ( L |`s C )
Assertion fldextrspunlem1 
|- ( ph -> ( dim ` ( ( subringAlg ` E ) ` G ) ) <_ ( J [:] K ) )

Proof

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