Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lindslinindsimp2 Structured version   Visualization version   GIF version

Theorem lindslinindsimp2 42777
Description: Implication 2 for lindslininds 42778. (Contributed by AV, 26-Apr-2019.) (Revised by AV, 30-Jul-2019.)
Hypotheses
Ref Expression
lindslinind.r 𝑅 = (Scalar‘𝑀)
lindslinind.b 𝐵 = (Base‘𝑅)
lindslinind.0 0 = (0g𝑅)
lindslinind.z 𝑍 = (0g𝑀)
Assertion
Ref Expression
lindslinindsimp2 ((𝑆𝑉𝑀 ∈ LMod) → ((𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) → (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 ))))
Distinct variable groups:   𝐵,𝑓,𝑠,𝑦   𝑓,𝑀,𝑠,𝑦   𝑅,𝑓,𝑥   𝑆,𝑓,𝑠,𝑥,𝑦   𝑉,𝑠,𝑦   𝑓,𝑍,𝑠,𝑦   0 ,𝑓,𝑠,𝑥,𝑦   𝑦,𝑅   𝑥,𝐵   𝑥,𝑀   𝑅,𝑠   𝑓,𝑉,𝑥   𝑥,𝑍

Proof of Theorem lindslinindsimp2
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 simprl 754 . . . 4 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) → 𝑆 ⊆ (Base‘𝑀))
2 elpwg 4306 . . . . 5 (𝑆𝑉 → (𝑆 ∈ 𝒫 (Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀)))
32ad2antrr 705 . . . 4 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) → (𝑆 ∈ 𝒫 (Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀)))
41, 3mpbird 247 . . 3 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) → 𝑆 ∈ 𝒫 (Base‘𝑀))
5 simplr 752 . . . . . . . . 9 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → 𝑀 ∈ LMod)
6 ssdifss 3892 . . . . . . . . . . 11 (𝑆 ⊆ (Base‘𝑀) → (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀))
76adantl 467 . . . . . . . . . 10 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀))
8 difexg 4943 . . . . . . . . . . . 12 (𝑆𝑉 → (𝑆 ∖ {𝑠}) ∈ V)
98ad2antrr 705 . . . . . . . . . . 11 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑆 ∖ {𝑠}) ∈ V)
10 elpwg 4306 . . . . . . . . . . 11 ((𝑆 ∖ {𝑠}) ∈ V → ((𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀)))
119, 10syl 17 . . . . . . . . . 10 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ((𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀)))
127, 11mpbird 247 . . . . . . . . 9 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀))
13 eqid 2771 . . . . . . . . . . . 12 (Base‘𝑀) = (Base‘𝑀)
1413lspeqlco 42753 . . . . . . . . . . 11 ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → (𝑀 LinCo (𝑆 ∖ {𝑠})) = ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))
1514eleq2d 2836 . . . . . . . . . 10 ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))))
1615bicomd 213 . . . . . . . . 9 ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠}))))
175, 12, 16syl2anc 573 . . . . . . . 8 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠}))))
1817notbid 307 . . . . . . 7 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠}))))
19 lindslinind.r . . . . . . . . . . . 12 𝑅 = (Scalar‘𝑀)
20 lindslinind.b . . . . . . . . . . . 12 𝐵 = (Base‘𝑅)
2113, 19, 20lcoval 42726 . . . . . . . . . . 11 ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g𝑅) ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
22 lindslinind.0 . . . . . . . . . . . . . . . 16 0 = (0g𝑅)
2322eqcomi 2780 . . . . . . . . . . . . . . 15 (0g𝑅) = 0
2423breq2i 4795 . . . . . . . . . . . . . 14 (𝑔 finSupp (0g𝑅) ↔ 𝑔 finSupp 0 )
2524anbi1i 610 . . . . . . . . . . . . 13 ((𝑔 finSupp (0g𝑅) ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
2625rexbii 3189 . . . . . . . . . . . 12 (∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g𝑅) ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
2726anbi2i 609 . . . . . . . . . . 11 (((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g𝑅) ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
2821, 27syl6bb 276 . . . . . . . . . 10 ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
295, 12, 28syl2anc 573 . . . . . . . . 9 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
3029notbid 307 . . . . . . . 8 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ¬ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
31 ianor 966 . . . . . . . . 9 (¬ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ¬ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
32 ralnex 3141 . . . . . . . . . . 11 (∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠})) ¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ¬ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
33 ianor 966 . . . . . . . . . . . 12 (¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
3433ralbii 3129 . . . . . . . . . . 11 (∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠})) ¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
3532, 34bitr3i 266 . . . . . . . . . 10 (¬ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
3635orbi2i 898 . . . . . . . . 9 ((¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ¬ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
3731, 36bitri 264 . . . . . . . 8 (¬ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
3830, 37syl6bb 276 . . . . . . 7 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
3918, 38bitrd 268 . . . . . 6 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
40392ralbidv 3138 . . . . 5 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
41 simpllr 760 . . . . . . . . . . 11 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑀 ∈ LMod)
42 eldifi 3883 . . . . . . . . . . . . 13 (𝑦 ∈ (𝐵 ∖ { 0 }) → 𝑦𝐵)
4342adantl 467 . . . . . . . . . . . 12 ((𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })) → 𝑦𝐵)
4443adantl 467 . . . . . . . . . . 11 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑦𝐵)
45 ssel2 3747 . . . . . . . . . . . 12 ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑠𝑆) → 𝑠 ∈ (Base‘𝑀))
4645ad2ant2lr 742 . . . . . . . . . . 11 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑠 ∈ (Base‘𝑀))
47 eqid 2771 . . . . . . . . . . . 12 ( ·𝑠𝑀) = ( ·𝑠𝑀)
4813, 19, 47, 20lmodvscl 19089 . . . . . . . . . . 11 ((𝑀 ∈ LMod ∧ 𝑦𝐵𝑠 ∈ (Base‘𝑀)) → (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀))
4941, 44, 46, 48syl3anc 1476 . . . . . . . . . 10 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀))
5049notnotd 140 . . . . . . . . 9 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → ¬ ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀))
51 nbfal 1643 . . . . . . . . 9 (¬ ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ↔ ⊥))
5250, 51sylib 208 . . . . . . . 8 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ↔ ⊥))
5352orbi1d 902 . . . . . . 7 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → ((¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
54532ralbidva 3137 . . . . . 6 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
55 r19.32v 3231 . . . . . . . . 9 (∀𝑦 ∈ (𝐵 ∖ { 0 })(⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (⊥ ∨ ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
5655ralbii 3129 . . . . . . . 8 (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ ∀𝑠𝑆 (⊥ ∨ ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
57 r19.32v 3231 . . . . . . . 8 (∀𝑠𝑆 (⊥ ∨ ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (⊥ ∨ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
5856, 57bitri 264 . . . . . . 7 (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (⊥ ∨ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
59 falim 1646 . . . . . . . . 9 (⊥ → (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
60 sneq 4327 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = 𝑥 → {𝑠} = {𝑥})
6160difeq2d 3879 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = 𝑥 → (𝑆 ∖ {𝑠}) = (𝑆 ∖ {𝑥}))
6261oveq2d 6811 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑥 → (𝐵𝑚 (𝑆 ∖ {𝑠})) = (𝐵𝑚 (𝑆 ∖ {𝑥})))
63 oveq2 6803 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = 𝑥 → (𝑦( ·𝑠𝑀)𝑠) = (𝑦( ·𝑠𝑀)𝑥))
6461oveq2d 6811 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = 𝑥 → (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))
6563, 64eqeq12d 2786 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = 𝑥 → ((𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))))
6665notbid 307 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = 𝑥 → (¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})) ↔ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))))
6766orbi2d 901 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑥 → ((¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))))
6862, 67raleqbidv 3301 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑥 → (∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))))
6968ralbidv 3135 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑥 → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))))
7069rspcva 3458 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑆 ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))))
71 lindslinind.z . . . . . . . . . . . . . . . . . . . . 21 𝑍 = (0g𝑀)
7219, 20, 22, 71lindslinindsimp2lem5 42776 . . . . . . . . . . . . . . . . . . . 20 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥𝑆)) → ((𝑓 ∈ (𝐵𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓𝑥) = 0 )))
7372expr 444 . . . . . . . . . . . . . . . . . . 19 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑥𝑆 → ((𝑓 ∈ (𝐵𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓𝑥) = 0 ))))
7473com14 96 . . . . . . . . . . . . . . . . . 18 (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑥𝑆 → ((𝑓 ∈ (𝐵𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑓𝑥) = 0 ))))
7570, 74syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥𝑆 ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → (𝑥𝑆 → ((𝑓 ∈ (𝐵𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑓𝑥) = 0 ))))
7675ex 397 . . . . . . . . . . . . . . . 16 (𝑥𝑆 → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) → (𝑥𝑆 → ((𝑓 ∈ (𝐵𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑓𝑥) = 0 )))))
7776pm2.43a 54 . . . . . . . . . . . . . . 15 (𝑥𝑆 → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) → ((𝑓 ∈ (𝐵𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑓𝑥) = 0 ))))
7877com14 96 . . . . . . . . . . . . . 14 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) → ((𝑓 ∈ (𝐵𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (𝑥𝑆 → (𝑓𝑥) = 0 ))))
7978imp 393 . . . . . . . . . . . . 13 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ((𝑓 ∈ (𝐵𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (𝑥𝑆 → (𝑓𝑥) = 0 )))
8079expdimp 440 . . . . . . . . . . . 12 (((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ∧ 𝑓 ∈ (𝐵𝑚 𝑆)) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → (𝑥𝑆 → (𝑓𝑥) = 0 )))
8180ralrimdv 3117 . . . . . . . . . . 11 (((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ∧ 𝑓 ∈ (𝐵𝑚 𝑆)) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 ))
8281ralrimiva 3115 . . . . . . . . . 10 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 ))
8382expcom 398 . . . . . . . . 9 (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) → (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
8459, 83jaoi 846 . . . . . . . 8 ((⊥ ∨ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
8584com12 32 . . . . . . 7 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ((⊥ ∨ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
8658, 85syl5bi 232 . . . . . 6 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
8754, 86sylbid 230 . . . . 5 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
8840, 87sylbid 230 . . . 4 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
8988impr 442 . . 3 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 ))
904, 89jca 501 . 2 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) → (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
9190ex 397 1 ((𝑆𝑉𝑀 ∈ LMod) → ((𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) → (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 ))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 836   = wceq 1631  wfal 1636  wcel 2145  wral 3061  wrex 3062  Vcvv 3351  cdif 3720  wss 3723  𝒫 cpw 4298  {csn 4317   class class class wbr 4787  cfv 6030  (class class class)co 6795  𝑚 cmap 8012   finSupp cfsupp 8434  Basecbs 16063  Scalarcsca 16151   ·𝑠 cvsca 16152  0gc0g 16307  LModclmod 19072  LSpanclspn 19183   linC clinc 42718   LinCo clinco 42719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099  ax-inf2 8705  ax-cnex 10197  ax-resscn 10198  ax-1cn 10199  ax-icn 10200  ax-addcl 10201  ax-addrcl 10202  ax-mulcl 10203  ax-mulrcl 10204  ax-mulcom 10205  ax-addass 10206  ax-mulass 10207  ax-distr 10208  ax-i2m1 10209  ax-1ne0 10210  ax-1rid 10211  ax-rnegex 10212  ax-rrecex 10213  ax-cnre 10214  ax-pre-lttri 10215  ax-pre-lttrn 10216  ax-pre-ltadd 10217  ax-pre-mulgt0 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-isom 6039  df-riota 6756  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-of 7047  df-om 7216  df-1st 7318  df-2nd 7319  df-supp 7450  df-wrecs 7562  df-recs 7624  df-rdg 7662  df-1o 7716  df-oadd 7720  df-er 7899  df-map 8014  df-en 8113  df-dom 8114  df-sdom 8115  df-fin 8116  df-fsupp 8435  df-oi 8574  df-card 8968  df-pnf 10281  df-mnf 10282  df-xr 10283  df-ltxr 10284  df-le 10285  df-sub 10473  df-neg 10474  df-nn 11226  df-2 11284  df-n0 11499  df-z 11584  df-uz 11893  df-fz 12533  df-fzo 12673  df-seq 13008  df-hash 13321  df-ndx 16066  df-slot 16067  df-base 16069  df-sets 16070  df-ress 16071  df-plusg 16161  df-0g 16309  df-gsum 16310  df-mre 16453  df-mrc 16454  df-acs 16456  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-mhm 17542  df-submnd 17543  df-grp 17632  df-minusg 17633  df-sbg 17634  df-mulg 17748  df-subg 17798  df-ghm 17865  df-cntz 17956  df-cmn 18401  df-abl 18402  df-mgp 18697  df-ur 18709  df-ring 18756  df-lmod 19074  df-lss 19142  df-lsp 19184  df-linc 42720  df-lco 42721
This theorem is referenced by:  lindslininds  42778
  Copyright terms: Public domain W3C validator