| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elpwi 4607 | . . . 4
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) → 𝑆 ⊆ (Base‘𝑀)) | 
| 2 | 1 | ad2antrl 728 | . . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → 𝑆 ⊆ (Base‘𝑀)) | 
| 3 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → 𝑀 ∈ LMod) | 
| 4 | 3 | anim2i 617 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) → (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) | 
| 5 | 4 | ancomd 461 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀))) | 
| 6 | 5 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀))) | 
| 7 |  | eldifi 4131 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) → 𝑦 ∈ 𝐵) | 
| 8 | 7 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → 𝑦 ∈ 𝐵) | 
| 9 | 8 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑦 ∈ 𝐵) | 
| 10 | 9 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → 𝑦 ∈ 𝐵) | 
| 11 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑠 ∈ 𝑆) | 
| 12 | 11 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → 𝑠 ∈ 𝑆) | 
| 13 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))) | 
| 14 | 10, 12, 13 | 3jca 1129 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})))) | 
| 15 |  | simprrl 781 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → 𝑔 finSupp 0 ) | 
| 16 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝑀) =
(Base‘𝑀) | 
| 17 |  | lindslinind.r | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑅 = (Scalar‘𝑀) | 
| 18 |  | lindslinind.b | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐵 = (Base‘𝑅) | 
| 19 |  | lindslinind.0 | . . . . . . . . . . . . . . . . . . . . . 22
⊢  0 =
(0g‘𝑅) | 
| 20 |  | lindslinind.z | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑍 = (0g‘𝑀) | 
| 21 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(invg‘𝑅) = (invg‘𝑅) | 
| 22 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) | 
| 23 | 16, 17, 18, 19, 20, 21, 22 | lincext2 48372 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀)) ∧
(𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))) ∧ 𝑔 finSupp 0 ) → (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ) | 
| 24 | 6, 14, 15, 23 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ) | 
| 25 | 4 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑆 ∈ 𝒫
(Base‘𝑀) ∧ 𝑀 ∈ LMod)) | 
| 26 | 25 | ancomd 461 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀))) | 
| 27 | 26 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀))) | 
| 28 | 16, 17, 18, 19, 20, 21, 22 | lincext1 48371 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀)) ∧
(𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})))) → (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) ∈ (𝐵 ↑m 𝑆)) | 
| 29 | 27, 14, 28 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) ∈ (𝐵 ↑m 𝑆)) | 
| 30 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → (𝑓 finSupp 0 ↔ (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 )) | 
| 31 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → (𝑓( linC ‘𝑀)𝑆) = ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆)) | 
| 32 | 31 | eqeq1d 2739 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍)) | 
| 33 | 30, 32 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍))) | 
| 34 |  | fveq1 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → (𝑓‘𝑥) = ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥)) | 
| 35 | 34 | eqeq1d 2739 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → ((𝑓‘𝑥) = 0 ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 )) | 
| 36 | 35 | ralbidv 3178 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → (∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 )) | 
| 37 | 33, 36 | imbi12d 344 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) ↔ (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ))) | 
| 38 | 37 | rspcv 3618 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) ∈ (𝐵 ↑m 𝑆) → (∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ))) | 
| 39 | 29, 38 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ))) | 
| 40 | 39 | exp4a 431 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍 → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 )))) | 
| 41 | 24, 40 | mpid 44 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍 → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ))) | 
| 42 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 43 | 16, 17, 18, 19, 20, 21, 22 | lincext3 48373 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀)) ∧
(𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍) | 
| 44 | 6, 14, 42, 43 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍) | 
| 45 |  | fveqeq2 6915 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑠 → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = 0 )) | 
| 46 | 45 | rspcv 3618 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = 0 )) | 
| 47 | 12, 46 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = 0 )) | 
| 48 |  | eqidd 2738 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))) | 
| 49 |  | iftrue 4531 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑠 → if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)) = ((invg‘𝑅)‘𝑦)) | 
| 50 | 49 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑧 = 𝑠) → if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)) = ((invg‘𝑅)‘𝑦)) | 
| 51 |  | fvexd 6921 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) →
((invg‘𝑅)‘𝑦) ∈ V) | 
| 52 | 48, 50, 11, 51 | fvmptd 7023 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = ((invg‘𝑅)‘𝑦)) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = ((invg‘𝑅)‘𝑦)) | 
| 54 | 53 | eqeq1d 2739 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = 0 ↔
((invg‘𝑅)‘𝑦) = 0 )) | 
| 55 | 17 | lmodfgrp 20867 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑀 ∈ LMod → 𝑅 ∈ Grp) | 
| 56 | 18, 19, 21 | grpinvnzcl 19029 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) →
((invg‘𝑅)‘𝑦) ∈ (𝐵 ∖ { 0 })) | 
| 57 |  | eldif 3961 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((invg‘𝑅)‘𝑦) ∈ (𝐵 ∖ { 0 }) ↔
(((invg‘𝑅)‘𝑦) ∈ 𝐵 ∧ ¬ ((invg‘𝑅)‘𝑦) ∈ { 0 })) | 
| 58 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((invg‘𝑅)‘𝑦) ∈ V | 
| 59 | 58 | elsn 4641 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((invg‘𝑅)‘𝑦) ∈ { 0 } ↔
((invg‘𝑅)‘𝑦) = 0 ) | 
| 60 |  | pm2.21 123 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (¬
((invg‘𝑅)‘𝑦) = 0 →
(((invg‘𝑅)‘𝑦) = 0 → (𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (𝑆 ∈ 𝒫 (Base‘𝑀) → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) | 
| 61 | 60 | com25 99 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (¬
((invg‘𝑅)‘𝑦) = 0 → (𝑆 ∈ 𝒫 (Base‘𝑀) → (𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) | 
| 62 | 59, 61 | sylnbi 330 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (¬
((invg‘𝑅)‘𝑦) ∈ { 0 } → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) | 
| 63 | 57, 62 | simplbiim 504 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((invg‘𝑅)‘𝑦) ∈ (𝐵 ∖ { 0 }) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) | 
| 64 | 56, 63 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) | 
| 65 | 64 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑅 ∈ Grp → (𝑦 ∈ (𝐵 ∖ { 0 }) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))))) | 
| 66 | 55, 65 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑀 ∈ LMod → (𝑦 ∈ (𝐵 ∖ { 0 }) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))))) | 
| 67 | 66 | com24 95 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑀 ∈ LMod → (𝑆 ∈ 𝑉 → (𝑆 ∈ 𝒫 (Base‘𝑀) → (𝑦 ∈ (𝐵 ∖ { 0 }) → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))))) | 
| 68 | 67 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → (𝑆 ∈ 𝒫 (Base‘𝑀) → (𝑦 ∈ (𝐵 ∖ { 0 }) → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) | 
| 69 | 68 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) → (𝑦 ∈ (𝐵 ∖ { 0 }) → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) | 
| 70 | 69 | com13 88 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑠 ∈ 𝑆 → (𝑦 ∈ (𝐵 ∖ { 0 }) → ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) →
(((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) | 
| 71 | 70 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) →
(((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) | 
| 72 | 71 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) →
(((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 73 | 72 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 74 | 54, 73 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 75 | 47, 74 | syld 47 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 76 | 44, 75 | embantd 59 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → ((((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍 → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ) → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 77 | 41, 76 | syldc 48 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑓 ∈
(𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 78 | 77 | exp5j 445 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑓 ∈
(𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → ((𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) | 
| 79 | 78 | impcom 407 | . . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧
∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )) → ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → ((𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) | 
| 80 | 79 | impcom 407 | . . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → ((𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) | 
| 81 | 80 | imp 406 | . . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 82 | 81 | expdimp 452 | . . . . . . . . . . . . 13
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))) → ((𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 83 | 82 | expd 415 | . . . . . . . . . . . 12
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))) → (𝑔 finSupp 0 → ((𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) | 
| 84 | 83 | impcom 407 | . . . . . . . . . . 11
⊢ ((𝑔 finSupp 0 ∧ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})))) → ((𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 85 | 84 | pm2.01d 190 | . . . . . . . . . 10
⊢ ((𝑔 finSupp 0 ∧ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) | 
| 86 | 85 | olcd 875 | . . . . . . . . 9
⊢ ((𝑔 finSupp 0 ∧ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})))) → (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 87 |  | animorl 980 | . . . . . . . . 9
⊢ ((¬
𝑔 finSupp 0 ∧
((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠})))) → (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 88 | 86, 87 | pm2.61ian 812 | . . . . . . . 8
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))) → (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 89 | 88 | ralrimiva 3146 | . . . . . . 7
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ∀𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 90 |  | ralnex 3072 | . . . . . . . 8
⊢
(∀𝑔 ∈
(𝐵 ↑m
(𝑆 ∖ {𝑠})) ¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ¬ ∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 91 |  | ianor 984 | . . . . . . . . 9
⊢ (¬
(𝑔 finSupp 0 ∧ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 92 | 91 | ralbii 3093 | . . . . . . . 8
⊢
(∀𝑔 ∈
(𝐵 ↑m
(𝑆 ∖ {𝑠})) ¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 93 | 90, 92 | bitr3i 277 | . . . . . . 7
⊢ (¬
∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 94 | 89, 93 | sylibr 234 | . . . . . 6
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ¬
∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 95 | 94 | intnand 488 | . . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ¬ ((𝑦(
·𝑠 ‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) | 
| 96 | 3 | ad2antrr 726 | . . . . . . 7
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑀 ∈ LMod) | 
| 97 |  | difexg 5329 | . . . . . . . . . 10
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∖ {𝑠}) ∈ V) | 
| 98 | 97 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑆 ∖ {𝑠}) ∈ V) | 
| 99 | 1 | ssdifssd 4147 | . . . . . . . . . 10
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀)) | 
| 100 | 99 | ad2antrl 728 | . . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀)) | 
| 101 | 98, 100 | elpwd 4606 | . . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) | 
| 102 | 101 | adantr 480 | . . . . . . 7
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) | 
| 103 | 16 | lspeqlco 48356 | . . . . . . . . 9
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → (𝑀 LinCo (𝑆 ∖ {𝑠})) = ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) | 
| 104 | 103 | eleq2d 2827 | . . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠
‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) | 
| 105 | 104 | bicomd 223 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠
‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})))) | 
| 106 | 96, 102, 105 | syl2anc 584 | . . . . . 6
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠
‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})))) | 
| 107 | 3 | adantr 480 | . . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → 𝑀 ∈ LMod) | 
| 108 |  | difexg 5329 | . . . . . . . . . . 11
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∖ {𝑠}) ∈ V) | 
| 109 | 108, 99 | elpwd 4606 | . . . . . . . . . 10
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∖ {𝑠}) ∈ 𝒫
(Base‘𝑀)) | 
| 110 | 109 | ad2antrl 728 | . . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) | 
| 111 | 107, 110 | jca 511 | . . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀))) | 
| 112 | 111 | adantr 480 | . . . . . . 7
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀))) | 
| 113 | 16, 17, 18 | lcoval 48329 | . . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g‘𝑅) ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) | 
| 114 | 19 | eqcomi 2746 | . . . . . . . . . . . 12
⊢
(0g‘𝑅) = 0 | 
| 115 | 114 | breq2i 5151 | . . . . . . . . . . 11
⊢ (𝑔 finSupp
(0g‘𝑅)
↔ 𝑔 finSupp 0
) | 
| 116 | 115 | anbi1i 624 | . . . . . . . . . 10
⊢ ((𝑔 finSupp
(0g‘𝑅)
∧ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 117 | 116 | rexbii 3094 | . . . . . . . . 9
⊢
(∃𝑔 ∈
(𝐵 ↑m
(𝑆 ∖ {𝑠}))(𝑔 finSupp (0g‘𝑅) ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) | 
| 118 | 117 | anbi2i 623 | . . . . . . . 8
⊢ (((𝑦(
·𝑠 ‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g‘𝑅) ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) | 
| 119 | 113, 118 | bitrdi 287 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) | 
| 120 | 112, 119 | syl 17 | . . . . . 6
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑦(
·𝑠 ‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) | 
| 121 | 106, 120 | bitrd 279 | . . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑m (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) | 
| 122 | 95, 121 | mtbird 325 | . . . 4
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) | 
| 123 | 122 | ralrimivva 3202 | . . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → ∀𝑠 ∈ 𝑆 ∀𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) | 
| 124 | 2, 123 | jca 511 | . 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠 ∈ 𝑆 ∀𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) | 
| 125 | 124 | ex 412 | 1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → ((𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )) → (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠 ∈ 𝑆 ∀𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))))) |