Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lindslinindsimp1 Structured version   Visualization version   GIF version
Theorem lindslinindsimp1 47637
Description: Implication 1 for lindslininds 47644. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) (Proof shortened by II, 16-Feb-2023.)
Hypotheses
Ref Expression
lindslinind.r 𝑅 = (Scalarβ€˜π‘€)
lindslinind.b 𝐡 = (Baseβ€˜π‘…)
lindslinind.0 0 = (0gβ€˜π‘…)
lindslinind.z 𝑍 = (0gβ€˜π‘€)
Assertion
Ref Expression
lindslinindsimp1 ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) β†’ ((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 )) β†’ (𝑆 βŠ† (Baseβ€˜π‘€) ∧ βˆ€π‘  ∈ 𝑆 βˆ€π‘¦ ∈ (𝐡 βˆ– { 0 }) Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ ((LSpanβ€˜π‘€)β€˜(𝑆 βˆ– {𝑠})))))
Distinct variable groups:   𝐡,𝑓,𝑠,𝑦   𝑓,𝑀,𝑠,𝑦   𝑅,𝑓,π‘₯   𝑆,𝑓,𝑠,π‘₯,𝑦   𝑉,𝑠,𝑦   𝑓,𝑍,𝑠,𝑦   0 ,𝑓,𝑠,π‘₯,𝑦
Allowed substitution hints:   𝐡(π‘₯)   𝑅(𝑦,𝑠)   𝑀(π‘₯)   𝑉(π‘₯,𝑓)   𝑍(π‘₯)
Proof of Theorem lindslinindsimp1
Dummy variables 𝑔 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elpwi 4610 . . . 4 (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ 𝑆 βŠ† (Baseβ€˜π‘€))
21ad2antrl 726 . . 3 (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) β†’ 𝑆 βŠ† (Baseβ€˜π‘€))
3 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) β†’ 𝑀 ∈ LMod)
43anim2i 615 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ 𝑀 ∈ LMod))
54ancomd 460 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) β†’ (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Baseβ€˜π‘€)))
65ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Baseβ€˜π‘€)))
7 eldifi 4124 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝐡 βˆ– { 0 }) β†’ 𝑦 ∈ 𝐡)
87adantl 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 })) β†’ 𝑦 ∈ 𝐡)
98adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ 𝑦 ∈ 𝐡)
109adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ 𝑦 ∈ 𝐡)
11 simprl 769 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ 𝑠 ∈ 𝑆)
1211adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ 𝑠 ∈ 𝑆)
13 simprl 769 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})))
1410, 12, 133jca 1125 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (𝑦 ∈ 𝐡 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))))
15 simprrl 779 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ 𝑔 finSupp 0 )
16 eqid 2725 . . . . . . . . . . . . . . . . . . . . . 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 2725 . . . . . . . . . . . . . . . . . . . . . 22 (invgβ€˜π‘…) = (invgβ€˜π‘…)
22 eqid 2725 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))
2316, 17, 18, 19, 20, 21, 22lincext2 47635 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Baseβ€˜π‘€)) ∧ (𝑦 ∈ 𝐡 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))) ∧ 𝑔 finSupp 0 ) β†’ (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) finSupp 0 )
246, 14, 15, 23syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) finSupp 0 )
254adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ 𝑀 ∈ LMod))
2625ancomd 460 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Baseβ€˜π‘€)))
2726adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Baseβ€˜π‘€)))
2816, 17, 18, 19, 20, 21, 22lincext1 47634 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Baseβ€˜π‘€)) ∧ (𝑦 ∈ 𝐡 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})))) β†’ (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) ∈ (𝐡 ↑m 𝑆))
2927, 14, 28syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) ∈ (𝐡 ↑m 𝑆))
30 breq1 5151 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) β†’ (𝑓 finSupp 0 ↔ (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) finSupp 0 ))
31 oveq1 7424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) β†’ (𝑓( linC β€˜π‘€)𝑆) = ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆))
3231eqeq1d 2727 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) β†’ ((𝑓( linC β€˜π‘€)𝑆) = 𝑍 ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆) = 𝑍))
3330, 32anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) β†’ ((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆) = 𝑍)))
34 fveq1 6893 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) β†’ (π‘“β€˜π‘₯) = ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯))
3534eqeq1d 2727 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) β†’ ((π‘“β€˜π‘₯) = 0 ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 ))
3635ralbidv 3168 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) β†’ (βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ↔ βˆ€π‘₯ ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 ))
3733, 36imbi12d 343 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) β†’ (((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ) ↔ (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 )))
3837rspcv 3603 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) ∈ (𝐡 ↑m 𝑆) β†’ (βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ) β†’ (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 )))
3929, 38syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ) β†’ (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 )))
4039exp4a 430 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ) β†’ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) finSupp 0 β†’ (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆) = 𝑍 β†’ βˆ€π‘₯ ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 ))))
4124, 40mpid 44 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ) β†’ (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆) = 𝑍 β†’ βˆ€π‘₯ ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 )))
42 simprr 771 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
4316, 17, 18, 19, 20, 21, 22lincext3 47636 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Baseβ€˜π‘€)) ∧ (𝑦 ∈ 𝐡 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))) β†’ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆) = 𝑍)
446, 14, 42, 43syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆) = 𝑍)
45 fveqeq2 6903 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 𝑠 β†’ (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘ ) = 0 ))
4645rspcv 3603 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ 𝑆 β†’ (βˆ€π‘₯ ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 β†’ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘ ) = 0 ))
4712, 46syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (βˆ€π‘₯ ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 β†’ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘ ) = 0 ))
48 eqidd 2726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))) = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§))))
49 iftrue 4535 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑠 β†’ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)) = ((invgβ€˜π‘…)β€˜π‘¦))
5049adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ 𝑧 = 𝑠) β†’ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)) = ((invgβ€˜π‘…)β€˜π‘¦))
51 fvexd 6909 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ ((invgβ€˜π‘…)β€˜π‘¦) ∈ V)
5248, 50, 11, 51fvmptd 7009 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘ ) = ((invgβ€˜π‘…)β€˜π‘¦))
5352adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘ ) = ((invgβ€˜π‘…)β€˜π‘¦))
5453eqeq1d 2727 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘ ) = 0 ↔ ((invgβ€˜π‘…)β€˜π‘¦) = 0 ))
5517lmodfgrp 20756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 ∈ LMod β†’ 𝑅 ∈ Grp)
5618, 19, 21grpinvnzcl 18971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑅 ∈ Grp ∧ 𝑦 ∈ (𝐡 βˆ– { 0 })) β†’ ((invgβ€˜π‘…)β€˜π‘¦) ∈ (𝐡 βˆ– { 0 }))
57 eldif 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((invgβ€˜π‘…)β€˜π‘¦) ∈ (𝐡 βˆ– { 0 }) ↔ (((invgβ€˜π‘…)β€˜π‘¦) ∈ 𝐡 ∧ Β¬ ((invgβ€˜π‘…)β€˜π‘¦) ∈ { 0 }))
58 fvex 6907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((invgβ€˜π‘…)β€˜π‘¦) ∈ V
5958elsn 4644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((invgβ€˜π‘…)β€˜π‘¦) ∈ { 0 } ↔ ((invgβ€˜π‘…)β€˜π‘¦) = 0 )
60 pm2.21 123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (Β¬ ((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ (𝑆 ∈ 𝑉 β†’ (𝑠 ∈ 𝑆 β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))))
6160com25 99 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (Β¬ ((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑆 ∈ 𝑉 β†’ (𝑠 ∈ 𝑆 β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))))
6259, 61sylnbi 329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (Β¬ ((invgβ€˜π‘…)β€˜π‘¦) ∈ { 0 } β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑆 ∈ 𝑉 β†’ (𝑠 ∈ 𝑆 β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))))
6357, 62simplbiim 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((invgβ€˜π‘…)β€˜π‘¦) ∈ (𝐡 βˆ– { 0 }) β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑆 ∈ 𝑉 β†’ (𝑠 ∈ 𝑆 β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))))
6456, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ Grp ∧ 𝑦 ∈ (𝐡 βˆ– { 0 })) β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑆 ∈ 𝑉 β†’ (𝑠 ∈ 𝑆 β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))))
6564ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑅 ∈ Grp β†’ (𝑦 ∈ (𝐡 βˆ– { 0 }) β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑆 ∈ 𝑉 β†’ (𝑠 ∈ 𝑆 β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))))))
6655, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 ∈ LMod β†’ (𝑦 ∈ (𝐡 βˆ– { 0 }) β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑆 ∈ 𝑉 β†’ (𝑠 ∈ 𝑆 β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))))))
6766com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 ∈ LMod β†’ (𝑆 ∈ 𝑉 β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑦 ∈ (𝐡 βˆ– { 0 }) β†’ (𝑠 ∈ 𝑆 β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))))))
6867impcom 406 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑦 ∈ (𝐡 βˆ– { 0 }) β†’ (𝑠 ∈ 𝑆 β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))))
6968impcom 406 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) β†’ (𝑦 ∈ (𝐡 βˆ– { 0 }) β†’ (𝑠 ∈ 𝑆 β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))))
7069com13 88 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ 𝑆 β†’ (𝑦 ∈ (𝐡 βˆ– { 0 }) β†’ ((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))))
7170imp 405 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 })) β†’ ((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))
7271impcom 406 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
7372adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (((invgβ€˜π‘…)β€˜π‘¦) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
7454, 73sylbid 239 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘ ) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
7547, 74syld 47 . . . . . . . . . . . . . . . . . . . 20 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ (βˆ€π‘₯ ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
7644, 75embantd 59 . . . . . . . . . . . . . . . . . . 19 ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ ((((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))( linC β€˜π‘€)𝑆) = 𝑍 β†’ βˆ€π‘₯ ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invgβ€˜π‘…)β€˜π‘¦), (π‘”β€˜π‘§)))β€˜π‘₯) = 0 ) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
7741, 76syldc 48 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ) β†’ ((((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ (𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
7877exp5j 444 . . . . . . . . . . . . . . . . 17 (βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ) β†’ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) β†’ ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 })) β†’ ((𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))))
7978impcom 406 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 )) β†’ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) β†’ ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 })) β†’ ((𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))))
8079impcom 406 . . . . . . . . . . . . . . 15 (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) β†’ ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 })) β†’ ((𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))
8180imp 405 . . . . . . . . . . . . . 14 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ ((𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
8281expdimp 451 . . . . . . . . . . . . 13 (((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))) β†’ ((𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
8382expd 414 . . . . . . . . . . . 12 (((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))) β†’ (𝑔 finSupp 0 β†’ ((𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))
8483impcom 406 . . . . . . . . . . 11 ((𝑔 finSupp 0 ∧ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})))) β†’ ((𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
8584pm2.01d 189 . . . . . . . . . 10 ((𝑔 finSupp 0 ∧ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})))) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))
8685olcd 872 . . . . . . . . 9 ((𝑔 finSupp 0 ∧ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})))) β†’ (Β¬ 𝑔 finSupp 0 ∨ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
87 animorl 975 . . . . . . . . 9 ((Β¬ 𝑔 finSupp 0 ∧ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})))) β†’ (Β¬ 𝑔 finSupp 0 ∨ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
8886, 87pm2.61ian 810 . . . . . . . 8 (((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) ∧ 𝑔 ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))) β†’ (Β¬ 𝑔 finSupp 0 ∨ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
8988ralrimiva 3136 . . . . . . 7 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ βˆ€π‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(Β¬ 𝑔 finSupp 0 ∨ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
90 ralnex 3062 . . . . . . . 8 (βˆ€π‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) Β¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))) ↔ Β¬ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
91 ianor 979 . . . . . . . . 9 (Β¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))) ↔ (Β¬ 𝑔 finSupp 0 ∨ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
9291ralbii 3083 . . . . . . . 8 (βˆ€π‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠})) Β¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))) ↔ βˆ€π‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(Β¬ 𝑔 finSupp 0 ∨ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
9390, 92bitr3i 276 . . . . . . 7 (Β¬ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))) ↔ βˆ€π‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(Β¬ 𝑔 finSupp 0 ∨ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
9489, 93sylibr 233 . . . . . 6 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ Β¬ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
9594intnand 487 . . . . 5 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ Β¬ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (Baseβ€˜π‘€) ∧ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))
963ad2antrr 724 . . . . . . 7 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ 𝑀 ∈ LMod)
97 difexg 5329 . . . . . . . . . 10 (𝑆 ∈ 𝑉 β†’ (𝑆 βˆ– {𝑠}) ∈ V)
9897ad2antrr 724 . . . . . . . . 9 (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) β†’ (𝑆 βˆ– {𝑠}) ∈ V)
991ssdifssd 4140 . . . . . . . . . 10 (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑆 βˆ– {𝑠}) βŠ† (Baseβ€˜π‘€))
10099ad2antrl 726 . . . . . . . . 9 (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) β†’ (𝑆 βˆ– {𝑠}) βŠ† (Baseβ€˜π‘€))
10198, 100elpwd 4609 . . . . . . . 8 (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) β†’ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€))
102101adantr 479 . . . . . . 7 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€))
10316lspeqlco 47619 . . . . . . . . 9 ((𝑀 ∈ LMod ∧ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€)) β†’ (𝑀 LinCo (𝑆 βˆ– {𝑠})) = ((LSpanβ€˜π‘€)β€˜(𝑆 βˆ– {𝑠})))
104103eleq2d 2811 . . . . . . . 8 ((𝑀 ∈ LMod ∧ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€)) β†’ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (𝑀 LinCo (𝑆 βˆ– {𝑠})) ↔ (𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ ((LSpanβ€˜π‘€)β€˜(𝑆 βˆ– {𝑠}))))
105104bicomd 222 . . . . . . 7 ((𝑀 ∈ LMod ∧ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€)) β†’ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ ((LSpanβ€˜π‘€)β€˜(𝑆 βˆ– {𝑠})) ↔ (𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (𝑀 LinCo (𝑆 βˆ– {𝑠}))))
10696, 102, 105syl2anc 582 . . . . . 6 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ ((LSpanβ€˜π‘€)β€˜(𝑆 βˆ– {𝑠})) ↔ (𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (𝑀 LinCo (𝑆 βˆ– {𝑠}))))
1073adantr 479 . . . . . . . . 9 (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) β†’ 𝑀 ∈ LMod)
108 difexg 5329 . . . . . . . . . . 11 (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑆 βˆ– {𝑠}) ∈ V)
109108, 99elpwd 4609 . . . . . . . . . 10 (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) β†’ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€))
110109ad2antrl 726 . . . . . . . . 9 (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) β†’ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€))
111107, 110jca 510 . . . . . . . 8 (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) β†’ (𝑀 ∈ LMod ∧ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€)))
112111adantr 479 . . . . . . 7 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ (𝑀 ∈ LMod ∧ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€)))
11316, 17, 18lcoval 47592 . . . . . . . 8 ((𝑀 ∈ LMod ∧ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€)) β†’ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (𝑀 LinCo (𝑆 βˆ– {𝑠})) ↔ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (Baseβ€˜π‘€) ∧ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp (0gβ€˜π‘…) ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))))
11419eqcomi 2734 . . . . . . . . . . . 12 (0gβ€˜π‘…) = 0
115114breq2i 5156 . . . . . . . . . . 11 (𝑔 finSupp (0gβ€˜π‘…) ↔ 𝑔 finSupp 0 )
116115anbi1i 622 . . . . . . . . . 10 ((𝑔 finSupp (0gβ€˜π‘…) ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))) ↔ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
117116rexbii 3084 . . . . . . . . 9 (βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp (0gβ€˜π‘…) ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))) ↔ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))
118117anbi2i 621 . . . . . . . 8 (((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (Baseβ€˜π‘€) ∧ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp (0gβ€˜π‘…) ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))) ↔ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (Baseβ€˜π‘€) ∧ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠})))))
119113, 118bitrdi 286 . . . . . . 7 ((𝑀 ∈ LMod ∧ (𝑆 βˆ– {𝑠}) ∈ 𝒫 (Baseβ€˜π‘€)) β†’ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (𝑀 LinCo (𝑆 βˆ– {𝑠})) ↔ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (Baseβ€˜π‘€) ∧ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))))
120112, 119syl 17 . . . . . 6 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (𝑀 LinCo (𝑆 βˆ– {𝑠})) ↔ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (Baseβ€˜π‘€) ∧ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))))
121106, 120bitrd 278 . . . . 5 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ ((LSpanβ€˜π‘€)β€˜(𝑆 βˆ– {𝑠})) ↔ ((𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ (Baseβ€˜π‘€) ∧ βˆƒπ‘” ∈ (𝐡 ↑m (𝑆 βˆ– {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠 β€˜π‘€)𝑠) = (𝑔( linC β€˜π‘€)(𝑆 βˆ– {𝑠}))))))
12295, 121mtbird 324 . . . 4 ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐡 βˆ– { 0 }))) β†’ Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ ((LSpanβ€˜π‘€)β€˜(𝑆 βˆ– {𝑠})))
123122ralrimivva 3191 . . 3 (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) β†’ βˆ€π‘  ∈ 𝑆 βˆ€π‘¦ ∈ (𝐡 βˆ– { 0 }) Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ ((LSpanβ€˜π‘€)β€˜(𝑆 βˆ– {𝑠})))
1242, 123jca 510 . 2 (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 ))) β†’ (𝑆 βŠ† (Baseβ€˜π‘€) ∧ βˆ€π‘  ∈ 𝑆 βˆ€π‘¦ ∈ (𝐡 βˆ– { 0 }) Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ ((LSpanβ€˜π‘€)β€˜(𝑆 βˆ– {𝑠}))))
125124ex 411 1 ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) β†’ ((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ βˆ€π‘“ ∈ (𝐡 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC β€˜π‘€)𝑆) = 𝑍) β†’ βˆ€π‘₯ ∈ 𝑆 (π‘“β€˜π‘₯) = 0 )) β†’ (𝑆 βŠ† (Baseβ€˜π‘€) ∧ βˆ€π‘  ∈ 𝑆 βˆ€π‘¦ ∈ (𝐡 βˆ– { 0 }) Β¬ (𝑦( ·𝑠 β€˜π‘€)𝑠) ∈ ((LSpanβ€˜π‘€)β€˜(𝑆 βˆ– {𝑠})))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3051  βˆƒwrex 3060  Vcvv 3463   βˆ– cdif 3942   βŠ† wss 3945  ifcif 4529  π’« cpw 4603  {csn 4629   class class class wbr 5148   ↦ cmpt 5231  β€˜cfv 6547  (class class class)co 7417   ↑m cmap 8843   finSupp cfsupp 9385  Basecbs 17179  Scalarcsca 17235   ·𝑠 cvsca 17236  0gc0g 17420  Grpcgrp 18894  invgcminusg 18895  LModclmod 20747  LSpanclspn 20859   linC clinc 47584   LinCo clinco 47585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-isom 6556  df-riota 7373  df-ov 7420  df-oprab 7421  df-mpo 7422  df-of 7683  df-om 7870  df-1st 7992  df-2nd 7993  df-supp 8164  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8723  df-map 8845  df-en 8963  df-dom 8964  df-sdom 8965  df-fin 8966  df-fsupp 9386  df-oi 9533  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-nn 12243  df-2 12305  df-n0 12503  df-z 12589  df-uz 12853  df-fz 13517  df-fzo 13660  df-seq 13999  df-hash 14322  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17180  df-ress 17209  df-plusg 17245  df-0g 17422  df-gsum 17423  df-mre 17565  df-mrc 17566  df-acs 17568  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-mhm 18739  df-submnd 18740  df-grp 18897  df-minusg 18898  df-sbg 18899  df-mulg 19028  df-subg 19082  df-ghm 19172  df-cntz 19272  df-cmn 19741  df-abl 19742  df-mgp 20079  df-rng 20097  df-ur 20126  df-ring 20179  df-lmod 20749  df-lss 20820  df-lsp 20860  df-linc 47586  df-lco 47587
This theorem is referenced by:  lindslininds  47644
  Copyright terms: Public domain W3C validator