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 ⊢ 𝐾 = ( 𝐿 ↾s 𝐹 )
fldextrspunfld.i ⊢ 𝐼 = ( 𝐿 ↾s 𝐺 )
fldextrspunfld.j ⊢ 𝐽 = ( 𝐿 ↾s 𝐻 )
fldextrspunfld.2 ⊢ ( 𝜑 → 𝐿 ∈ Field )
fldextrspunfld.3 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐼 ) )
fldextrspunfld.4 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐽 ) )
fldextrspunfld.5 ⊢ ( 𝜑 → 𝐺 ∈ ( SubDRing ‘ 𝐿 ) )
fldextrspunfld.6 ⊢ ( 𝜑 → 𝐻 ∈ ( SubDRing ‘ 𝐿 ) )
fldextrspunfld.7 ⊢ ( 𝜑 → ( 𝐽 [:] 𝐾 ) ∈ ℕ0 )
fldextrspunfld.n ⊢ 𝑁 = ( RingSpan ‘ 𝐿 )
fldextrspunfld.c ⊢ 𝐶 = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) )
fldextrspunfld.e ⊢ 𝐸 = ( 𝐿 ↾s 𝐶 )
Assertion fldextrspunlem1 ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐺 ) ) ≤ ( 𝐽 [:] 𝐾 ) )

Proof

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