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 43998
Description: Implication 2 for lindslininds 43999. (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 767 . . . 4 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) → 𝑆 ⊆ (Base‘𝑀))
2 elpwg 4461 . . . . 5 (𝑆𝑉 → (𝑆 ∈ 𝒫 (Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀)))
32ad2antrr 722 . . . 4 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) → (𝑆 ∈ 𝒫 (Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀)))
41, 3mpbird 258 . . 3 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) → 𝑆 ∈ 𝒫 (Base‘𝑀))
5 simplr 765 . . . . . . . . 9 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → 𝑀 ∈ LMod)
6 ssdifss 4033 . . . . . . . . . . 11 (𝑆 ⊆ (Base‘𝑀) → (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀))
76adantl 482 . . . . . . . . . 10 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀))
8 difexg 5122 . . . . . . . . . . . 12 (𝑆𝑉 → (𝑆 ∖ {𝑠}) ∈ V)
98ad2antrr 722 . . . . . . . . . . 11 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑆 ∖ {𝑠}) ∈ V)
10 elpwg 4461 . . . . . . . . . . 11 ((𝑆 ∖ {𝑠}) ∈ V → ((𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀)))
119, 10syl 17 . . . . . . . . . 10 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ((𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀)))
127, 11mpbird 258 . . . . . . . . 9 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀))
13 eqid 2795 . . . . . . . . . . . 12 (Base‘𝑀) = (Base‘𝑀)
1413lspeqlco 43974 . . . . . . . . . . 11 ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → (𝑀 LinCo (𝑆 ∖ {𝑠})) = ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))
1514eleq2d 2868 . . . . . . . . . 10 ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))))
1615bicomd 224 . . . . . . . . 9 ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠}))))
175, 12, 16syl2anc 584 . . . . . . . 8 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠}))))
1817notbid 319 . . . . . . 7 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠}))))
19 lindslinind.r . . . . . . . . . . . 12 𝑅 = (Scalar‘𝑀)
20 lindslinind.b . . . . . . . . . . . 12 𝐵 = (Base‘𝑅)
2113, 19, 20lcoval 43947 . . . . . . . . . . 11 ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g𝑅) ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
22 lindslinind.0 . . . . . . . . . . . . . . . 16 0 = (0g𝑅)
2322eqcomi 2804 . . . . . . . . . . . . . . 15 (0g𝑅) = 0
2423breq2i 4970 . . . . . . . . . . . . . 14 (𝑔 finSupp (0g𝑅) ↔ 𝑔 finSupp 0 )
2524anbi1i 623 . . . . . . . . . . . . 13 ((𝑔 finSupp (0g𝑅) ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
2625rexbii 3211 . . . . . . . . . . . 12 (∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g𝑅) ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
2726anbi2i 622 . . . . . . . . . . 11 (((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g𝑅) ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
2821, 27syl6bb 288 . . . . . . . . . 10 ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
295, 12, 28syl2anc 584 . . . . . . . . 9 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ((𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
3029notbid 319 . . . . . . . 8 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ¬ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
31 ianor 976 . . . . . . . . 9 (¬ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ¬ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
32 ralnex 3200 . . . . . . . . . . 11 (∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠})) ¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ¬ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
33 ianor 976 . . . . . . . . . . . 12 (¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
3433ralbii 3132 . . . . . . . . . . 11 (∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠})) ¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
3532, 34bitr3i 278 . . . . . . . . . 10 (¬ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))
3635orbi2i 907 . . . . . . . . 9 ((¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ¬ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
3731, 36bitri 276 . . . . . . . 8 (¬ ((𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
3830, 37syl6bb 288 . . . . . . 7 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
3918, 38bitrd 280 . . . . . 6 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
40392ralbidv 3166 . . . . 5 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
41 simpllr 772 . . . . . . . . . . 11 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑀 ∈ LMod)
42 eldifi 4024 . . . . . . . . . . . . 13 (𝑦 ∈ (𝐵 ∖ { 0 }) → 𝑦𝐵)
4342adantl 482 . . . . . . . . . . . 12 ((𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })) → 𝑦𝐵)
4443adantl 482 . . . . . . . . . . 11 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑦𝐵)
45 ssel2 3884 . . . . . . . . . . . 12 ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑠𝑆) → 𝑠 ∈ (Base‘𝑀))
4645ad2ant2lr 744 . . . . . . . . . . 11 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑠 ∈ (Base‘𝑀))
47 eqid 2795 . . . . . . . . . . . 12 ( ·𝑠𝑀) = ( ·𝑠𝑀)
4813, 19, 47, 20lmodvscl 19341 . . . . . . . . . . 11 ((𝑀 ∈ LMod ∧ 𝑦𝐵𝑠 ∈ (Base‘𝑀)) → (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀))
4941, 44, 46, 48syl3anc 1364 . . . . . . . . . 10 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀))
5049notnotd 146 . . . . . . . . 9 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → ¬ ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀))
51 nbfal 1537 . . . . . . . . 9 (¬ ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ↔ (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ↔ ⊥))
5250, 51sylib 219 . . . . . . . 8 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → (¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ↔ ⊥))
5352orbi1d 911 . . . . . . 7 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ (𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }))) → ((¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
54532ralbidva 3165 . . . . . 6 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))
55 r19.32v 3301 . . . . . . . . 9 (∀𝑦 ∈ (𝐵 ∖ { 0 })(⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (⊥ ∨ ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
5655ralbii 3132 . . . . . . . 8 (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ ∀𝑠𝑆 (⊥ ∨ ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
57 r19.32v 3301 . . . . . . . 8 (∀𝑠𝑆 (⊥ ∨ ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (⊥ ∨ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
5856, 57bitri 276 . . . . . . 7 (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ (⊥ ∨ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))
59 falim 1539 . . . . . . . . 9 (⊥ → (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
60 sneq 4482 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = 𝑥 → {𝑠} = {𝑥})
6160difeq2d 4020 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = 𝑥 → (𝑆 ∖ {𝑠}) = (𝑆 ∖ {𝑥}))
6261oveq2d 7032 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑥 → (𝐵𝑚 (𝑆 ∖ {𝑠})) = (𝐵𝑚 (𝑆 ∖ {𝑥})))
63 oveq2 7024 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = 𝑥 → (𝑦( ·𝑠𝑀)𝑠) = (𝑦( ·𝑠𝑀)𝑥))
6461oveq2d 7032 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = 𝑥 → (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))
6563, 64eqeq12d 2810 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = 𝑥 → ((𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))))
6665notbid 319 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = 𝑥 → (¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})) ↔ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))))
6766orbi2d 910 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑥 → ((¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))))
6862, 67raleqbidv 3361 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑥 → (∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))))
6968ralbidv 3164 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑥 → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))))
7069rspcva 3557 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑆 ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))))
71 lindslinind.z . . . . . . . . . . . . . . . . . . . . 21 𝑍 = (0g𝑀)
7219, 20, 22, 71lindslinindsimp2lem5 43997 . . . . . . . . . . . . . . . . . . . 20 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥𝑆)) → ((𝑓 ∈ (𝐵𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓𝑥) = 0 )))
7372expr 457 . . . . . . . . . . . . . . . . . . 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 413 . . . . . . . . . . . . . . . 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 407 . . . . . . . . . . . . 13 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ((𝑓 ∈ (𝐵𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (𝑥𝑆 → (𝑓𝑥) = 0 )))
8079expdimp 453 . . . . . . . . . . . 12 (((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ∧ 𝑓 ∈ (𝐵𝑚 𝑆)) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → (𝑥𝑆 → (𝑓𝑥) = 0 )))
8180ralrimdv 3155 . . . . . . . . . . 11 (((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ∧ 𝑓 ∈ (𝐵𝑚 𝑆)) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 ))
8281ralrimiva 3149 . . . . . . . . . 10 ((((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 ))
8382expcom 414 . . . . . . . . 9 (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) → (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
8459, 83jaoi 852 . . . . . . . 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 243 . . . . . 6 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(⊥ ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
8754, 86sylbid 241 . . . . 5 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 })(¬ (𝑦( ·𝑠𝑀)𝑠) ∈ (Base‘𝑀) ∨ ∀𝑔 ∈ (𝐵𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦( ·𝑠𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
8840, 87sylbid 241 . . . 4 (((𝑆𝑉𝑀 ∈ LMod) ∧ 𝑆 ⊆ (Base‘𝑀)) → (∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
8988impr 455 . . 3 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) → ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 ))
904, 89jca 512 . 2 (((𝑆𝑉𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) → (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 )))
9190ex 413 1 ((𝑆𝑉𝑀 ∈ LMod) → ((𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠𝑆𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦( ·𝑠𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) → (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥𝑆 (𝑓𝑥) = 0 ))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 842   = wceq 1522  wfal 1534  wcel 2081  wral 3105  wrex 3106  Vcvv 3437  cdif 3856  wss 3859  𝒫 cpw 4453  {csn 4472   class class class wbr 4962  cfv 6225  (class class class)co 7016  𝑚 cmap 8256   finSupp cfsupp 8679  Basecbs 16312  Scalarcsca 16397   ·𝑠 cvsca 16398  0gc0g 16542  LModclmod 19324  LSpanclspn 19433   linC clinc 43939   LinCo clinco 43940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-of 7267  df-om 7437  df-1st 7545  df-2nd 7546  df-supp 7682  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-er 8139  df-map 8258  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-fsupp 8680  df-oi 8820  df-card 9214  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-nn 11487  df-2 11548  df-n0 11746  df-z 11830  df-uz 12094  df-fz 12743  df-fzo 12884  df-seq 13220  df-hash 13541  df-ndx 16315  df-slot 16316  df-base 16318  df-sets 16319  df-ress 16320  df-plusg 16407  df-0g 16544  df-gsum 16545  df-mre 16686  df-mrc 16687  df-acs 16689  df-mgm 17681  df-sgrp 17723  df-mnd 17734  df-mhm 17774  df-submnd 17775  df-grp 17864  df-minusg 17865  df-sbg 17866  df-mulg 17982  df-subg 18030  df-ghm 18097  df-cntz 18188  df-cmn 18635  df-abl 18636  df-mgp 18930  df-ur 18942  df-ring 18989  df-lmod 19326  df-lss 19394  df-lsp 19434  df-linc 43941  df-lco 43942
This theorem is referenced by:  lindslininds  43999
  Copyright terms: Public domain W3C validator