Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑀) =
(Base‘𝑀) |
2 | | eqid 2610 |
. . . . 5
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
3 | | eqid 2610 |
. . . . 5
⊢
(0g‘(Scalar‘𝑀)) =
(0g‘(Scalar‘𝑀)) |
4 | | eqid 2610 |
. . . . 5
⊢
(1r‘(Scalar‘𝑀)) =
(1r‘(Scalar‘𝑀)) |
5 | | eqeq1 2614 |
. . . . . . 7
⊢ (𝑠 = 𝑦 → (𝑠 = (0g‘𝑀) ↔ 𝑦 = (0g‘𝑀))) |
6 | 5 | ifbid 4058 |
. . . . . 6
⊢ (𝑠 = 𝑦 → if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) = if(𝑦 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) |
7 | 6 | cbvmptv 4678 |
. . . . 5
⊢ (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) = (𝑦 ∈ 𝑆 ↦ if(𝑦 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) |
8 | 1, 2, 3, 4, 7 | mptcfsupp 41955 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀))) |
9 | 8 | 3adant1r 1311 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀))) |
10 | | simp1l 1078 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → 𝑀 ∈ LMod) |
11 | | simp2 1055 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → 𝑆 ∈ 𝒫
(Base‘𝑀)) |
12 | | eqid 2610 |
. . . . 5
⊢
(0g‘𝑀) = (0g‘𝑀) |
13 | | eqid 2610 |
. . . . 5
⊢ (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) |
14 | 1, 2, 3, 4, 12, 13 | linc0scn0 42006 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀)) →
((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆) = (0g‘𝑀)) |
15 | 10, 11, 14 | syl2anc 691 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆) = (0g‘𝑀)) |
16 | | simp3 1056 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
(0g‘𝑀)
∈ 𝑆) |
17 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = (0g‘𝑀) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) = ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘(0g‘𝑀))) |
18 | 17 | neeq1d 2841 |
. . . . 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 | | fvex 6113 |
. . . . . . 7
⊢
(1r‘(Scalar‘𝑀)) ∈ V |
21 | 20 | a1i 11 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
(1r‘(Scalar‘𝑀)) ∈ V) |
22 | | iftrue 4042 |
. . . . . . 7
⊢ (𝑠 = (0g‘𝑀) → if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) =
(1r‘(Scalar‘𝑀))) |
23 | 22, 13 | fvmptg 6189 |
. . . . . 6
⊢
(((0g‘𝑀) ∈ 𝑆 ∧
(1r‘(Scalar‘𝑀)) ∈ V) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘(0g‘𝑀)) =
(1r‘(Scalar‘𝑀))) |
24 | 16, 21, 23 | syl2anc 691 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘(0g‘𝑀)) =
(1r‘(Scalar‘𝑀))) |
25 | 2 | lmodring 18694 |
. . . . . . . 8
⊢ (𝑀 ∈ LMod →
(Scalar‘𝑀) ∈
Ring) |
26 | 25 | anim1i 590 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) → ((Scalar‘𝑀) ∈ Ring ∧ 1 <
(#‘(Base‘(Scalar‘𝑀))))) |
27 | 26 | 3ad2ant1 1075 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
((Scalar‘𝑀) ∈
Ring ∧ 1 < (#‘(Base‘(Scalar‘𝑀))))) |
28 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
29 | 28, 4, 3 | ring1ne0 18414 |
. . . . . 6
⊢
(((Scalar‘𝑀)
∈ Ring ∧ 1 < (#‘(Base‘(Scalar‘𝑀)))) →
(1r‘(Scalar‘𝑀)) ≠
(0g‘(Scalar‘𝑀))) |
30 | 27, 29 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
(1r‘(Scalar‘𝑀)) ≠
(0g‘(Scalar‘𝑀))) |
31 | 24, 30 | eqnetrd 2849 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘(0g‘𝑀)) ≠
(0g‘(Scalar‘𝑀))) |
32 | 16, 19, 31 | rspcedvd 3289 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
∃𝑥 ∈ 𝑆 ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀))) |
33 | 2, 28, 4 | lmod1cl 18713 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod →
(1r‘(Scalar‘𝑀)) ∈ (Base‘(Scalar‘𝑀))) |
34 | 2, 28, 3 | lmod0cl 18712 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod →
(0g‘(Scalar‘𝑀)) ∈ (Base‘(Scalar‘𝑀))) |
35 | 33, 34 | ifcld 4081 |
. . . . . . . . 9
⊢ (𝑀 ∈ LMod → if(𝑠 = (0g‘𝑀),
(1r‘(Scalar‘𝑀)), (0g‘(Scalar‘𝑀))) ∈
(Base‘(Scalar‘𝑀))) |
36 | 35 | adantr 480 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) → if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) ∈ (Base‘(Scalar‘𝑀))) |
37 | 36 | 3ad2ant1 1075 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → if(𝑠 = (0g‘𝑀),
(1r‘(Scalar‘𝑀)), (0g‘(Scalar‘𝑀))) ∈
(Base‘(Scalar‘𝑀))) |
38 | 37 | adantr 480 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) ∧ 𝑠 ∈ 𝑆) → if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) ∈ (Base‘(Scalar‘𝑀))) |
39 | 38, 13 | fmptd 6292 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))):𝑆⟶(Base‘(Scalar‘𝑀))) |
40 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
41 | 40 | a1i 11 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
(Base‘(Scalar‘𝑀)) ∈ V) |
42 | 41, 11 | elmapd 7758 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑆) ↔ (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))):𝑆⟶(Base‘(Scalar‘𝑀)))) |
43 | 39, 42 | mpbird 246 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑆)) |
44 | | breq1 4586 |
. . . . . 6
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (𝑓 finSupp
(0g‘(Scalar‘𝑀)) ↔ (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀)))) |
45 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (𝑓( linC ‘𝑀)𝑆) = ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆)) |
46 | 45 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → ((𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ↔ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑆) = (0g‘𝑀))) |
47 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (𝑓‘𝑥) = ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥)) |
48 | 47 | neeq1d 2841 |
. . . . . . 7
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → ((𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀)) ↔ ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀)))) |
49 | 48 | rexbidv 3034 |
. . . . . 6
⊢ (𝑓 = (𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀)) ↔ ∃𝑥 ∈ 𝑆 ((𝑠 ∈ 𝑆 ↦ if(𝑠 = (0g‘𝑀), (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))‘𝑥) ≠
(0g‘(Scalar‘𝑀)))) |
50 | 44, 46, 49 | 3anbi123d 1391 |
. . . . 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‘𝑀))))) |
51 | 50 | 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‘𝑀))))) |
52 | 43, 51 | rspcedv 3286 |
. . 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‘𝑀)) ↑𝑚
𝑆)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀))))) |
53 | 9, 15, 32, 52 | mp3and 1419 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) →
∃𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑆)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀)))) |
54 | 1, 12, 2, 28, 3 | islindeps 42036 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀)) →
(𝑆 linDepS 𝑀 ↔ ∃𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑆)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀))))) |
55 | 10, 11, 54 | syl2anc 691 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → (𝑆 linDepS 𝑀 ↔ ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑆)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝑓( linC ‘𝑀)𝑆) = (0g‘𝑀) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠
(0g‘(Scalar‘𝑀))))) |
56 | 53, 55 | mpbird 246 |
1
⊢ (((𝑀 ∈ LMod ∧ 1 <
(#‘(Base‘(Scalar‘𝑀)))) ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝑆) → 𝑆 linDepS 𝑀) |