| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝑀) =
(Base‘𝑀) | 
| 2 |  | eqid 2736 | . . . . 5
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) | 
| 3 |  | eqid 2736 | . . . . 5
⊢
(0g‘(Scalar‘𝑀)) =
(0g‘(Scalar‘𝑀)) | 
| 4 |  | eqid 2736 | . . . . 5
⊢
(1r‘(Scalar‘𝑀)) =
(1r‘(Scalar‘𝑀)) | 
| 5 |  | eqeq1 2740 | . . . . . . 7
⊢ (𝑠 = 𝑦 → (𝑠 = (0g‘𝑀) ↔ 𝑦 = (0g‘𝑀))) | 
| 6 | 5 | ifbid 4548 | . . . . . 6
⊢ (𝑠 = 𝑦 → if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) = if(𝑦 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) | 
| 7 | 6 | cbvmptv 5254 | . . . . 5
⊢ (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) = (𝑦 ∈ 𝑆 ↦ if(𝑦 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) | 
| 8 | 1, 2, 3, 4, 7 | mptcfsupp 48298 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀))) | 
| 9 | 8 | 3adant1r 1177 | . . 3
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀))) | 
| 10 |  | simp1l 1197 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → 𝑀 ∈ LMod) | 
| 11 |  | simp2 1137 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → 𝑆 ∈ 𝒫
(Base‘𝑀)) | 
| 12 |  | eqid 2736 | . . . . 5
⊢
(0g‘𝑀) = (0g‘𝑀) | 
| 13 |  | eqid 2736 | . . . . 5
⊢ (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) | 
| 14 | 1, 2, 3, 4, 12, 13 | linc0scn0 48345 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀)) →
((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆) = (0g‘𝑀)) | 
| 15 | 10, 11, 14 | syl2anc 584 | . . 3
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆) = (0g‘𝑀)) | 
| 16 |  | simp3 1138 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
(0g‘𝑀)
∈ 𝑆) | 
| 17 |  | fveq2 6905 | . . . . . 6
⊢ (𝑥 = (0g‘𝑀) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) = ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘(0g‘𝑀))) | 
| 18 | 17 | neeq1d 2999 | . . . . 5
⊢ (𝑥 = (0g‘𝑀) → (((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀)) ↔ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘(0g‘𝑀)) ≠
(0g‘(Scalar‘𝑀)))) | 
| 19 | 18 | adantl 481 | . . . 4
⊢ ((((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) ∧ 𝑥 = (0g‘𝑀)) → (((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀)) ↔ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘(0g‘𝑀)) ≠
(0g‘(Scalar‘𝑀)))) | 
| 20 |  | iftrue 4530 | . . . . . 6
⊢ (𝑠 = (0g‘𝑀) → if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) =
(1r‘(Scalar‘𝑀))) | 
| 21 |  | fvexd 6920 | . . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
(1r‘(Scalar‘𝑀)) ∈ V) | 
| 22 | 13, 20, 16, 21 | fvmptd3 7038 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘(0g‘𝑀)) =
(1r‘(Scalar‘𝑀))) | 
| 23 | 2 | lmodring 20867 | . . . . . . . 8
⊢ (𝑀 ∈ LMod →
(Scalar‘𝑀) ∈
Ring) | 
| 24 | 23 | anim1i 615 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) → ((Scalar‘𝑀) ∈ Ring ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀))))) | 
| 25 | 24 | 3ad2ant1 1133 | . . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
((Scalar‘𝑀) ∈
Ring ∧ 1 < (♯‘(Base‘(Scalar‘𝑀))))) | 
| 26 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) | 
| 27 | 26, 4, 3 | ring1ne0 20297 | . . . . . 6
⊢
(((Scalar‘𝑀)
∈ Ring ∧ 1 < (♯‘(Base‘(Scalar‘𝑀)))) →
(1r‘(Scalar‘𝑀)) ≠
(0g‘(Scalar‘𝑀))) | 
| 28 | 25, 27 | syl 17 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
(1r‘(Scalar‘𝑀)) ≠
(0g‘(Scalar‘𝑀))) | 
| 29 | 22, 28 | eqnetrd 3007 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘(0g‘𝑀)) ≠
(0g‘(Scalar‘𝑀))) | 
| 30 | 16, 19, 29 | rspcedvd 3623 | . . 3
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
∃𝑥 ∈ 𝑆 ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀))) | 
| 31 | 2, 26, 4 | lmod1cl 20888 | . . . . . . . . . 10
⊢ (𝑀 ∈ LMod →
(1r‘(Scalar‘𝑀)) ∈ (Base‘(Scalar‘𝑀))) | 
| 32 | 2, 26, 3 | lmod0cl 20887 | . . . . . . . . . 10
⊢ (𝑀 ∈ LMod →
(0g‘(Scalar‘𝑀)) ∈ (Base‘(Scalar‘𝑀))) | 
| 33 | 31, 32 | ifcld 4571 | . . . . . . . . 9
⊢ (𝑀 ∈ LMod → if(𝑠 = (0g‘𝑀),
(1r‘(Scalar‘𝑀)), (0g‘(Scalar‘𝑀))) ∈
(Base‘(Scalar‘𝑀))) | 
| 34 | 33 | adantr 480 | . . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) → if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) ∈ (Base‘(Scalar‘𝑀))) | 
| 35 | 34 | 3ad2ant1 1133 | . . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → if(𝑠 = (0g‘𝑀),
(1r‘(Scalar‘𝑀)), (0g‘(Scalar‘𝑀))) ∈
(Base‘(Scalar‘𝑀))) | 
| 36 | 35 | adantr 480 | . . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) ∧ 𝑠 ∈ 𝑆) → if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) ∈ (Base‘(Scalar‘𝑀))) | 
| 37 | 36 | fmpttd 7134 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))):𝑆⟶(Base‘(Scalar‘𝑀))) | 
| 38 |  | fvexd 6920 | . . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
(Base‘(Scalar‘𝑀)) ∈ V) | 
| 39 | 38, 11 | elmapd 8881 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑆) ↔ (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))):𝑆⟶(Base‘(Scalar‘𝑀)))) | 
| 40 | 37, 39 | mpbird 257 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑆)) | 
| 41 |  | breq1 5145 | . . . . . 6
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (𝑓 finSupp
(0g‘(Scalar‘𝑀)) ↔ (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀)))) | 
| 42 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (𝑓( linC ‘𝑀)𝑆) = ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆)) | 
| 43 | 42 | eqeq1d 2738 | . . . . . 6
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → ((𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ↔ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆) = (0g‘𝑀))) | 
| 44 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (𝑓‘𝑥) = ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥)) | 
| 45 | 44 | neeq1d 2999 | . . . . . . 7
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → ((𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀)) ↔ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀)))) | 
| 46 | 45 | rexbidv 3178 | . . . . . 6
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀)) ↔ ∃𝑥 ∈ 𝑆 ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀)))) | 
| 47 | 41, 43, 46 | 3anbi123d 1437 | . . . . 5
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → ((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀))) ↔ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀)) ∧ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀))))) | 
| 48 | 47 | adantl 481 | . . . 4
⊢ ((((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) ∧ 𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))) → ((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀))) ↔ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀)) ∧ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀))))) | 
| 49 | 40, 48 | rspcedv 3614 | . . 3
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀)) ∧ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀))) → ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑆)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀))))) | 
| 50 | 9, 15, 30, 49 | mp3and 1465 | . 2
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
∃𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑆)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀)))) | 
| 51 | 1, 12, 2, 26, 3 | islindeps 48375 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀)) →
(𝑆 linDepS 𝑀 ↔ ∃𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑆)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀))))) | 
| 52 | 10, 11, 51 | syl2anc 584 | . 2
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (𝑆 linDepS 𝑀 ↔ ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑆)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀))))) | 
| 53 | 50, 52 | mpbird 257 | 1
⊢ (((𝑀 ∈ LMod ∧ 1 <
(♯‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → 𝑆 linDepS 𝑀) |