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

Metamath Proof Explorer

Theorem extdgfialglem1

Description: Lemma for extdgfialg . (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses extdgfialg.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
extdgfialg.d ⊢ 𝐷 = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) )
extdgfialg.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
extdgfialg.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
extdgfialg.1 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
extdgfialglem1.2 ⊢ 𝑍 = ( 0g ‘ 𝐸 )
extdgfialglem1.3 ⊢ · = ( .r ‘ 𝐸 )
extdgfialglem1.r ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑋 ) )
extdgfialglem1.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion extdgfialglem1 ( 𝜑 → ∃ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ( 𝑎 finSupp 𝑍 ∧ ( ( 𝐸 Σg ( 𝑎 ∘f · 𝐺 ) ) = 𝑍 ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { 𝑍 } ) ) ) )

Proof

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 ... 𝐷 ) × { 𝑍 } ) ) ) )