| Step |
Hyp |
Ref |
Expression |
| 1 |
|
extdgfialg.b |
⊢ 𝐵 = ( Base ‘ 𝐸 ) |
| 2 |
|
extdgfialg.d |
⊢ 𝐷 = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) |
| 3 |
|
extdgfialg.e |
⊢ ( 𝜑 → 𝐸 ∈ Field ) |
| 4 |
|
extdgfialg.f |
⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ) |
| 5 |
|
extdgfialg.1 |
⊢ ( 𝜑 → 𝐷 ∈ ℕ0 ) |
| 6 |
|
extdgfialglem1.2 |
⊢ 𝑍 = ( 0g ‘ 𝐸 ) |
| 7 |
|
extdgfialglem1.3 |
⊢ · = ( .r ‘ 𝐸 ) |
| 8 |
|
extdgfialglem1.r |
⊢ 𝐺 = ( 𝑛 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) ) |
| 9 |
|
extdgfialglem1.4 |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
| 10 |
|
simplr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ran 𝐺 ⊆ 𝑏 ) → 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 11 |
3
|
flddrngd |
⊢ ( 𝜑 → 𝐸 ∈ DivRing ) |
| 12 |
|
eqid |
⊢ ( 𝐸 ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 ) |
| 13 |
12
|
sdrgdrng |
⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) |
| 14 |
4 13
|
syl |
⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) |
| 15 |
|
sdrgsubrg |
⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) ) |
| 16 |
4 15
|
syl |
⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) ) |
| 17 |
|
eqid |
⊢ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) |
| 18 |
17 12
|
sralvec |
⊢ ( ( 𝐸 ∈ DivRing ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ) → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LVec ) |
| 19 |
11 14 16 18
|
syl3anc |
⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LVec ) |
| 20 |
19
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LVec ) |
| 21 |
20
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ran 𝐺 ⊆ 𝑏 ) → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LVec ) |
| 22 |
|
eqid |
⊢ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) |
| 23 |
22
|
dimval |
⊢ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LVec ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = ( ♯ ‘ 𝑏 ) ) |
| 24 |
2 23
|
eqtrid |
⊢ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LVec ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → 𝐷 = ( ♯ ‘ 𝑏 ) ) |
| 25 |
21 10 24
|
syl2anc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ran 𝐺 ⊆ 𝑏 ) → 𝐷 = ( ♯ ‘ 𝑏 ) ) |
| 26 |
5
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ran 𝐺 ⊆ 𝑏 ) → 𝐷 ∈ ℕ0 ) |
| 27 |
25 26
|
eqeltrrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ran 𝐺 ⊆ 𝑏 ) → ( ♯ ‘ 𝑏 ) ∈ ℕ0 ) |
| 28 |
|
hashclb |
⊢ ( 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) → ( 𝑏 ∈ Fin ↔ ( ♯ ‘ 𝑏 ) ∈ ℕ0 ) ) |
| 29 |
28
|
biimpar |
⊢ ( ( 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝑏 ) ∈ ℕ0 ) → 𝑏 ∈ Fin ) |
| 30 |
10 27 29
|
syl2anc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ran 𝐺 ⊆ 𝑏 ) → 𝑏 ∈ Fin ) |
| 31 |
|
hashss |
⊢ ( ( 𝑏 ∈ Fin ∧ ran 𝐺 ⊆ 𝑏 ) → ( ♯ ‘ ran 𝐺 ) ≤ ( ♯ ‘ 𝑏 ) ) |
| 32 |
30 31
|
sylancom |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ran 𝐺 ⊆ 𝑏 ) → ( ♯ ‘ ran 𝐺 ) ≤ ( ♯ ‘ 𝑏 ) ) |
| 33 |
8
|
dmeqi |
⊢ dom 𝐺 = dom ( 𝑛 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) ) |
| 34 |
|
eqid |
⊢ ( 𝑛 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) ) = ( 𝑛 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) ) |
| 35 |
|
ovexd |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ 𝑛 ∈ ( 0 ... 𝐷 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) ∈ V ) |
| 36 |
34 35
|
dmmptd |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → dom ( 𝑛 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) ) = ( 0 ... 𝐷 ) ) |
| 37 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → ( 0 ... 𝐷 ) ∈ V ) |
| 38 |
36 37
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → dom ( 𝑛 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) ) ∈ V ) |
| 39 |
33 38
|
eqeltrid |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → dom 𝐺 ∈ V ) |
| 40 |
|
hashf1rn |
⊢ ( ( dom 𝐺 ∈ V ∧ 𝐺 : dom 𝐺 –1-1→ V ) → ( ♯ ‘ 𝐺 ) = ( ♯ ‘ ran 𝐺 ) ) |
| 41 |
39 40
|
sylancom |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → ( ♯ ‘ 𝐺 ) = ( ♯ ‘ ran 𝐺 ) ) |
| 42 |
41
|
ad3antrrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ran 𝐺 ⊆ 𝑏 ) → ( ♯ ‘ 𝐺 ) = ( ♯ ‘ ran 𝐺 ) ) |
| 43 |
32 42 25
|
3brtr4d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ran 𝐺 ⊆ 𝑏 ) → ( ♯ ‘ 𝐺 ) ≤ 𝐷 ) |
| 44 |
22
|
islinds4 |
⊢ ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LVec → ( ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ↔ ∃ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ran 𝐺 ⊆ 𝑏 ) ) |
| 45 |
44
|
biimpa |
⊢ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LVec ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → ∃ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ran 𝐺 ⊆ 𝑏 ) |
| 46 |
20 45
|
sylancom |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → ∃ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ran 𝐺 ⊆ 𝑏 ) |
| 47 |
43 46
|
r19.29a |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐺 ) ≤ 𝐷 ) |
| 48 |
5
|
nn0red |
⊢ ( 𝜑 → 𝐷 ∈ ℝ ) |
| 49 |
48
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → 𝐷 ∈ ℝ ) |
| 50 |
49
|
ltp1d |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → 𝐷 < ( 𝐷 + 1 ) ) |
| 51 |
|
fzfid |
⊢ ( 𝜑 → ( 0 ... 𝐷 ) ∈ Fin ) |
| 52 |
51
|
mptexd |
⊢ ( 𝜑 → ( 𝑛 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) ) ∈ V ) |
| 53 |
8 52
|
eqeltrid |
⊢ ( 𝜑 → 𝐺 ∈ V ) |
| 54 |
53
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → 𝐺 ∈ V ) |
| 55 |
|
f1f |
⊢ ( 𝐺 : dom 𝐺 –1-1→ V → 𝐺 : dom 𝐺 ⟶ V ) |
| 56 |
55
|
adantl |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → 𝐺 : dom 𝐺 ⟶ V ) |
| 57 |
56
|
ffund |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → Fun 𝐺 ) |
| 58 |
|
hashfundm |
⊢ ( ( 𝐺 ∈ V ∧ Fun 𝐺 ) → ( ♯ ‘ 𝐺 ) = ( ♯ ‘ dom 𝐺 ) ) |
| 59 |
54 57 58
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → ( ♯ ‘ 𝐺 ) = ( ♯ ‘ dom 𝐺 ) ) |
| 60 |
8 35
|
dmmptd |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → dom 𝐺 = ( 0 ... 𝐷 ) ) |
| 61 |
60
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → ( ♯ ‘ dom 𝐺 ) = ( ♯ ‘ ( 0 ... 𝐷 ) ) ) |
| 62 |
|
hashfz0 |
⊢ ( 𝐷 ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝐷 ) ) = ( 𝐷 + 1 ) ) |
| 63 |
5 62
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... 𝐷 ) ) = ( 𝐷 + 1 ) ) |
| 64 |
63
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → ( ♯ ‘ ( 0 ... 𝐷 ) ) = ( 𝐷 + 1 ) ) |
| 65 |
59 61 64
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → ( ♯ ‘ 𝐺 ) = ( 𝐷 + 1 ) ) |
| 66 |
65
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐺 ) = ( 𝐷 + 1 ) ) |
| 67 |
50 66
|
breqtrrd |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → 𝐷 < ( ♯ ‘ 𝐺 ) ) |
| 68 |
49
|
rexrd |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → 𝐷 ∈ ℝ* ) |
| 69 |
54
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → 𝐺 ∈ V ) |
| 70 |
|
hashxrcl |
⊢ ( 𝐺 ∈ V → ( ♯ ‘ 𝐺 ) ∈ ℝ* ) |
| 71 |
69 70
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐺 ) ∈ ℝ* ) |
| 72 |
68 71
|
xrltnled |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → ( 𝐷 < ( ♯ ‘ 𝐺 ) ↔ ¬ ( ♯ ‘ 𝐺 ) ≤ 𝐷 ) ) |
| 73 |
67 72
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → ¬ ( ♯ ‘ 𝐺 ) ≤ 𝐷 ) |
| 74 |
47 73
|
pm2.65da |
⊢ ( ( 𝜑 ∧ 𝐺 : dom 𝐺 –1-1→ V ) → ¬ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 75 |
74
|
ex |
⊢ ( 𝜑 → ( 𝐺 : dom 𝐺 –1-1→ V → ¬ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) |
| 76 |
|
imnan |
⊢ ( ( 𝐺 : dom 𝐺 –1-1→ V → ¬ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↔ ¬ ( 𝐺 : dom 𝐺 –1-1→ V ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) |
| 77 |
75 76
|
sylib |
⊢ ( 𝜑 → ¬ ( 𝐺 : dom 𝐺 –1-1→ V ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) |
| 78 |
19
|
lveclmodd |
⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LMod ) |
| 79 |
|
eqidd |
⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) |
| 80 |
1
|
sdrgss |
⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ⊆ 𝐵 ) |
| 81 |
4 80
|
syl |
⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 ) |
| 82 |
81 1
|
sseqtrdi |
⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐸 ) ) |
| 83 |
79 82
|
srasca |
⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 84 |
|
drngnzr |
⊢ ( ( 𝐸 ↾s 𝐹 ) ∈ DivRing → ( 𝐸 ↾s 𝐹 ) ∈ NzRing ) |
| 85 |
14 84
|
syl |
⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ NzRing ) |
| 86 |
83 85
|
eqeltrrd |
⊢ ( 𝜑 → ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∈ NzRing ) |
| 87 |
|
eqid |
⊢ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) |
| 88 |
87
|
islindf3 |
⊢ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LMod ∧ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∈ NzRing ) → ( 𝐺 LIndF ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↔ ( 𝐺 : dom 𝐺 –1-1→ V ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) ) |
| 89 |
78 86 88
|
syl2anc |
⊢ ( 𝜑 → ( 𝐺 LIndF ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↔ ( 𝐺 : dom 𝐺 –1-1→ V ∧ ran 𝐺 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) ) |
| 90 |
77 89
|
mtbird |
⊢ ( 𝜑 → ¬ 𝐺 LIndF ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) |
| 91 |
|
ovexd |
⊢ ( 𝜑 → ( 0 ... 𝐷 ) ∈ V ) |
| 92 |
|
eqid |
⊢ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) |
| 93 |
|
eqid |
⊢ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) |
| 94 |
92 93
|
mgpbas |
⊢ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = ( Base ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 95 |
|
eqid |
⊢ ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) = ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 96 |
3
|
fldcrngd |
⊢ ( 𝜑 → 𝐸 ∈ CRing ) |
| 97 |
96
|
crngringd |
⊢ ( 𝜑 → 𝐸 ∈ Ring ) |
| 98 |
17 1
|
sraring |
⊢ ( ( 𝐸 ∈ Ring ∧ 𝐹 ⊆ 𝐵 ) → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ Ring ) |
| 99 |
97 81 98
|
syl2anc |
⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ Ring ) |
| 100 |
92
|
ringmgp |
⊢ ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ Ring → ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∈ Mnd ) |
| 101 |
99 100
|
syl |
⊢ ( 𝜑 → ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∈ Mnd ) |
| 102 |
101
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝐷 ) ) → ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∈ Mnd ) |
| 103 |
|
fz0ssnn0 |
⊢ ( 0 ... 𝐷 ) ⊆ ℕ0 |
| 104 |
103
|
a1i |
⊢ ( 𝜑 → ( 0 ... 𝐷 ) ⊆ ℕ0 ) |
| 105 |
104
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝐷 ) ) → 𝑛 ∈ ℕ0 ) |
| 106 |
79 82
|
srabase |
⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 107 |
1 106
|
eqtr2id |
⊢ ( 𝜑 → ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = 𝐵 ) |
| 108 |
9 107
|
eleqtrrd |
⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 109 |
108
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝐷 ) ) → 𝑋 ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 110 |
94 95 102 105 109
|
mulgnn0cld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝐷 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 111 |
110 8
|
fmptd |
⊢ ( 𝜑 → 𝐺 : ( 0 ... 𝐷 ) ⟶ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 112 |
|
eqid |
⊢ ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) |
| 113 |
|
eqid |
⊢ ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) |
| 114 |
|
eqid |
⊢ ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) = ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 115 |
|
eqid |
⊢ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) = ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) |
| 116 |
93 87 112 113 114 115
|
islindf4 |
⊢ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LMod ∧ ( 0 ... 𝐷 ) ∈ V ∧ 𝐺 : ( 0 ... 𝐷 ) ⟶ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → ( 𝐺 LIndF ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↔ ∀ 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) → 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ) |
| 117 |
78 91 111 116
|
syl3anc |
⊢ ( 𝜑 → ( 𝐺 LIndF ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↔ ∀ 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) → 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ) |
| 118 |
90 117
|
mtbid |
⊢ ( 𝜑 → ¬ ∀ 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) → 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) |
| 119 |
|
rexanali |
⊢ ( ∃ 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ ¬ 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ↔ ¬ ∀ 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) → 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) |
| 120 |
118 119
|
sylibr |
⊢ ( 𝜑 → ∃ 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ ¬ 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) |
| 121 |
|
fvex |
⊢ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∈ V |
| 122 |
|
ovex |
⊢ ( 0 ... 𝐷 ) ∈ V |
| 123 |
|
eqid |
⊢ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) = ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) |
| 124 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 125 |
123 124 114 115
|
frlmelbas |
⊢ ( ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∈ V ∧ ( 0 ... 𝐷 ) ∈ V ) → ( 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ↔ ( 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↑m ( 0 ... 𝐷 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) ) ) |
| 126 |
121 122 125
|
mp2an |
⊢ ( 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ↔ ( 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↑m ( 0 ... 𝐷 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) ) |
| 127 |
126
|
anbi1i |
⊢ ( ( 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ↔ ( ( 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↑m ( 0 ... 𝐷 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ) |
| 128 |
|
df-ne |
⊢ ( 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ↔ ¬ 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) |
| 129 |
128
|
anbi2i |
⊢ ( ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ↔ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ ¬ 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) |
| 130 |
129
|
anbi2i |
⊢ ( ( 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ↔ ( 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ ¬ 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ) |
| 131 |
|
anass |
⊢ ( ( ( 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↑m ( 0 ... 𝐷 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ↔ ( 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↑m ( 0 ... 𝐷 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ) ) |
| 132 |
127 130 131
|
3bitr3i |
⊢ ( ( 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ ¬ 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ↔ ( 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↑m ( 0 ... 𝐷 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ) ) |
| 133 |
132
|
rexbii2 |
⊢ ( ∃ 𝑎 ∈ ( Base ‘ ( ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) freeLMod ( 0 ... 𝐷 ) ) ) ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ ¬ 𝑎 = ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ↔ ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↑m ( 0 ... 𝐷 ) ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ) |
| 134 |
120 133
|
sylib |
⊢ ( 𝜑 → ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↑m ( 0 ... 𝐷 ) ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ) |
| 135 |
12 1
|
ressbas2 |
⊢ ( 𝐹 ⊆ 𝐵 → 𝐹 = ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) ) |
| 136 |
81 135
|
syl |
⊢ ( 𝜑 → 𝐹 = ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) ) |
| 137 |
83
|
fveq2d |
⊢ ( 𝜑 → ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) = ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) |
| 138 |
136 137
|
eqtr2d |
⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) = 𝐹 ) |
| 139 |
138
|
oveq1d |
⊢ ( 𝜑 → ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↑m ( 0 ... 𝐷 ) ) = ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) |
| 140 |
96
|
crnggrpd |
⊢ ( 𝜑 → 𝐸 ∈ Grp ) |
| 141 |
140
|
grpmndd |
⊢ ( 𝜑 → 𝐸 ∈ Mnd ) |
| 142 |
|
subrgsubg |
⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → 𝐹 ∈ ( SubGrp ‘ 𝐸 ) ) |
| 143 |
16 142
|
syl |
⊢ ( 𝜑 → 𝐹 ∈ ( SubGrp ‘ 𝐸 ) ) |
| 144 |
|
eqid |
⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 ) |
| 145 |
144
|
subg0cl |
⊢ ( 𝐹 ∈ ( SubGrp ‘ 𝐸 ) → ( 0g ‘ 𝐸 ) ∈ 𝐹 ) |
| 146 |
143 145
|
syl |
⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ 𝐹 ) |
| 147 |
12 1 144
|
ress0g |
⊢ ( ( 𝐸 ∈ Mnd ∧ ( 0g ‘ 𝐸 ) ∈ 𝐹 ∧ 𝐹 ⊆ 𝐵 ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) ) |
| 148 |
141 146 81 147
|
syl3anc |
⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) ) |
| 149 |
83
|
fveq2d |
⊢ ( 𝜑 → ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) = ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ) |
| 150 |
148 149
|
eqtr2d |
⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) = ( 0g ‘ 𝐸 ) ) |
| 151 |
150 6
|
eqtr4di |
⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) = 𝑍 ) |
| 152 |
151
|
breq2d |
⊢ ( 𝜑 → ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↔ 𝑎 finSupp 𝑍 ) ) |
| 153 |
79 82
|
sravsca |
⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 154 |
7 153
|
eqtr2id |
⊢ ( 𝜑 → ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = · ) |
| 155 |
154
|
ofeqd |
⊢ ( 𝜑 → ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = ∘f · ) |
| 156 |
155
|
oveqd |
⊢ ( 𝜑 → ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) = ( 𝑎 ∘f · 𝐺 ) ) |
| 157 |
156
|
oveq2d |
⊢ ( 𝜑 → ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f · 𝐺 ) ) ) |
| 158 |
|
ovexd |
⊢ ( 𝜑 → ( 𝑎 ∘f · 𝐺 ) ∈ V ) |
| 159 |
17 158 3 19 82
|
gsumsra |
⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑎 ∘f · 𝐺 ) ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f · 𝐺 ) ) ) |
| 160 |
157 159
|
eqtr4d |
⊢ ( 𝜑 → ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 𝐸 Σg ( 𝑎 ∘f · 𝐺 ) ) ) |
| 161 |
6
|
a1i |
⊢ ( 𝜑 → 𝑍 = ( 0g ‘ 𝐸 ) ) |
| 162 |
79 161 82
|
sralmod0 |
⊢ ( 𝜑 → 𝑍 = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) |
| 163 |
162
|
eqcomd |
⊢ ( 𝜑 → ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = 𝑍 ) |
| 164 |
160 163
|
eqeq12d |
⊢ ( 𝜑 → ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ↔ ( 𝐸 Σg ( 𝑎 ∘f · 𝐺 ) ) = 𝑍 ) ) |
| 165 |
151
|
sneqd |
⊢ ( 𝜑 → { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } = { 𝑍 } ) |
| 166 |
165
|
xpeq2d |
⊢ ( 𝜑 → ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) = ( ( 0 ... 𝐷 ) × { 𝑍 } ) ) |
| 167 |
166
|
neeq2d |
⊢ ( 𝜑 → ( 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ↔ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { 𝑍 } ) ) ) |
| 168 |
164 167
|
anbi12d |
⊢ ( 𝜑 → ( ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ↔ ( ( 𝐸 Σg ( 𝑎 ∘f · 𝐺 ) ) = 𝑍 ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { 𝑍 } ) ) ) ) |
| 169 |
152 168
|
anbi12d |
⊢ ( 𝜑 → ( ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ↔ ( 𝑎 finSupp 𝑍 ∧ ( ( 𝐸 Σg ( 𝑎 ∘f · 𝐺 ) ) = 𝑍 ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { 𝑍 } ) ) ) ) ) |
| 170 |
139 169
|
rexeqbidv |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ↑m ( 0 ... 𝐷 ) ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) ∧ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) Σg ( 𝑎 ∘f ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) 𝐺 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) } ) ) ) ↔ ∃ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ( 𝑎 finSupp 𝑍 ∧ ( ( 𝐸 Σg ( 𝑎 ∘f · 𝐺 ) ) = 𝑍 ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { 𝑍 } ) ) ) ) ) |
| 171 |
134 170
|
mpbid |
⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ( 𝑎 finSupp 𝑍 ∧ ( ( 𝐸 Σg ( 𝑎 ∘f · 𝐺 ) ) = 𝑍 ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { 𝑍 } ) ) ) ) |