Step | Hyp | Ref
| Expression |
1 | | df-ne 2782 |
. . . . 5
⊢ ((𝑠 · 𝑋) ≠ 𝑍 ↔ ¬ (𝑠 · 𝑋) = 𝑍) |
2 | 1 | ralbii 2963 |
. . . 4
⊢
(∀𝑠 ∈
(𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ ∀𝑠 ∈ (𝑆 ∖ { 0 }) ¬ (𝑠 · 𝑋) = 𝑍) |
3 | | raldifsni 4265 |
. . . 4
⊢
(∀𝑠 ∈
(𝑆 ∖ { 0 }) ¬
(𝑠 · 𝑋) = 𝑍 ↔ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) |
4 | 2, 3 | bitri 263 |
. . 3
⊢
(∀𝑠 ∈
(𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) |
5 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → 𝑀 ∈ LMod) |
6 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → 𝑀 ∈ LMod) |
7 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → 𝑀 ∈ LMod) |
8 | | snlindsntor.s |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 = (Base‘𝑅) |
9 | | snlindsntor.r |
. . . . . . . . . . . . . . . . 17
⊢ 𝑅 = (Scalar‘𝑀) |
10 | 9 | fveq2i 6106 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝑅) =
(Base‘(Scalar‘𝑀)) |
11 | 8, 10 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢ 𝑆 =
(Base‘(Scalar‘𝑀)) |
12 | 11 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ↑𝑚
{𝑋}) =
((Base‘(Scalar‘𝑀)) ↑𝑚 {𝑋}) |
13 | 12 | eleq2i 2680 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝑆 ↑𝑚 {𝑋}) ↔ 𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
{𝑋})) |
14 | 13 | biimpi 205 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝑆 ↑𝑚 {𝑋}) → 𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
{𝑋})) |
15 | 14 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → 𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
{𝑋})) |
16 | | snelpwi 4839 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ (Base‘𝑀) → {𝑋} ∈ 𝒫 (Base‘𝑀)) |
17 | | snlindsntor.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑀) |
18 | 16, 17 | eleq2s 2706 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐵 → {𝑋} ∈ 𝒫 (Base‘𝑀)) |
19 | 18 | ad3antlr 763 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → {𝑋} ∈ 𝒫 (Base‘𝑀)) |
20 | | lincval 41992 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ LMod ∧ 𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 {𝑋}) ∧ {𝑋} ∈ 𝒫 (Base‘𝑀)) → (𝑓( linC ‘𝑀){𝑋}) = (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
21 | 7, 15, 19, 20 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → (𝑓( linC ‘𝑀){𝑋}) = (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
22 | 21 | eqeq1d 2612 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 ↔ (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = 𝑍)) |
23 | 22 | anbi2d 736 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) ↔ (𝑓 finSupp 0 ∧ (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = 𝑍))) |
24 | | lmodgrp 18693 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Grp) |
25 | | grpmnd 17252 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ Grp → 𝑀 ∈ Mnd) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Mnd) |
27 | 26 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → 𝑀 ∈ Mnd) |
28 | | simpllr 795 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → 𝑋 ∈ 𝐵) |
29 | | elmapi 7765 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (𝑆 ↑𝑚 {𝑋}) → 𝑓:{𝑋}⟶𝑆) |
30 | 6 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → 𝑀 ∈ LMod) |
31 | | snidg 4153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ {𝑋}) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ {𝑋}) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → 𝑋 ∈ {𝑋}) |
34 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ 𝑋 ∈ {𝑋}) → (𝑓‘𝑋) ∈ 𝑆) |
35 | 33, 34 | sylan2 490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → (𝑓‘𝑋) ∈ 𝑆) |
36 | | simprlr 799 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → 𝑋 ∈ 𝐵) |
37 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
38 | 17, 9, 37, 8 | lmodvscl 18703 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ LMod ∧ (𝑓‘𝑋) ∈ 𝑆 ∧ 𝑋 ∈ 𝐵) → ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵) |
39 | 30, 35, 36, 38 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵) |
40 | 39 | expcom 450 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → (𝑓:{𝑋}⟶𝑆 → ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵)) |
41 | 29, 40 | syl5com 31 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝑆 ↑𝑚 {𝑋}) → (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵)) |
42 | 41 | impcom 445 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵) |
43 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → (𝑓‘𝑥) = (𝑓‘𝑋)) |
44 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
45 | 43, 44 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥) = ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋)) |
46 | 17, 45 | gsumsn 18177 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵) → (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋)) |
47 | 27, 28, 42, 46 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋)) |
48 | 47 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → ((𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = 𝑍 ↔ ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍)) |
49 | 31, 34 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ 𝑋 ∈ 𝐵) → (𝑓‘𝑋) ∈ 𝑆) |
50 | 49 | expcom 450 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐵 → (𝑓:{𝑋}⟶𝑆 → (𝑓‘𝑋) ∈ 𝑆)) |
51 | 50 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (𝑓:{𝑋}⟶𝑆 → (𝑓‘𝑋) ∈ 𝑆)) |
52 | | snlindsntor.t |
. . . . . . . . . . . . . . . . 17
⊢ · = (
·𝑠 ‘𝑀) |
53 | 52 | oveqi 6562 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑋) · 𝑋) = ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) |
54 | 53 | eqeq1i 2615 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑋) · 𝑋) = 𝑍 ↔ ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍) |
55 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (𝑓‘𝑋) → (𝑠 · 𝑋) = ((𝑓‘𝑋) · 𝑋)) |
56 | 55 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑓‘𝑋) → ((𝑠 · 𝑋) = 𝑍 ↔ ((𝑓‘𝑋) · 𝑋) = 𝑍)) |
57 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑓‘𝑋) → (𝑠 = 0 ↔ (𝑓‘𝑋) = 0 )) |
58 | 56, 57 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑓‘𝑋) → (((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) ↔ (((𝑓‘𝑋) · 𝑋) = 𝑍 → (𝑓‘𝑋) = 0 ))) |
59 | 58 | rspcva 3280 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑋) ∈ 𝑆 ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → (((𝑓‘𝑋) · 𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )) |
60 | 54, 59 | syl5bir 232 |
. . . . . . . . . . . . . 14
⊢ (((𝑓‘𝑋) ∈ 𝑆 ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → (((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )) |
61 | 60 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑋) ∈ 𝑆 → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → (((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 ))) |
62 | 29, 51, 61 | syl56 35 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (𝑓 ∈ (𝑆 ↑𝑚 {𝑋}) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → (((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )))) |
63 | 62 | com23 84 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → (𝑓 ∈ (𝑆 ↑𝑚 {𝑋}) → (((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )))) |
64 | 63 | imp31 447 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → (((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )) |
65 | 48, 64 | sylbid 229 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → ((𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = 𝑍 → (𝑓‘𝑋) = 0 )) |
66 | 65 | adantld 482 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → ((𝑓 finSupp 0 ∧ (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = 𝑍) → (𝑓‘𝑋) = 0 )) |
67 | 23, 66 | sylbid 229 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 )) |
68 | 67 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → ∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 )) |
69 | 68 | ex 449 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → ∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ))) |
70 | | impexp 461 |
. . . . . . . 8
⊢ (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) ↔ (𝑓 finSupp 0 → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ))) |
71 | 29 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → 𝑓:{𝑋}⟶𝑆) |
72 | | snfi 7923 |
. . . . . . . . . . 11
⊢ {𝑋} ∈ Fin |
73 | 72 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → {𝑋} ∈ Fin) |
74 | | snlindsntor.0 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑅) |
75 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) ∈ V |
76 | 74, 75 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
77 | 76 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → 0 ∈ V) |
78 | 71, 73, 77 | fdmfifsupp 8168 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → 𝑓 finSupp 0 ) |
79 | | pm2.27 41 |
. . . . . . . . 9
⊢ (𝑓 finSupp 0 → ((𝑓 finSupp 0 → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ))) |
80 | 78, 79 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → ((𝑓 finSupp 0 → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ))) |
81 | 70, 80 | syl5bi 231 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑𝑚 {𝑋})) → (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ))) |
82 | 81 | ralimdva 2945 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) → ∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ))) |
83 | | snlindsntor.z |
. . . . . . 7
⊢ 𝑍 = (0g‘𝑀) |
84 | 17, 9, 8, 74, 83, 52 | snlindsntorlem 42053 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ) → ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) |
85 | 82, 84 | syld 46 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) → ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) |
86 | 69, 85 | impbid 201 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) ↔ ∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ))) |
87 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → (𝑓‘𝑦) = (𝑓‘𝑋)) |
88 | 87 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → ((𝑓‘𝑦) = 0 ↔ (𝑓‘𝑋) = 0 )) |
89 | 88 | ralsng 4165 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ↔ (𝑓‘𝑋) = 0 )) |
90 | 89 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ↔ (𝑓‘𝑋) = 0 )) |
91 | 90 | bicomd 212 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → ((𝑓‘𝑋) = 0 ↔ ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )) |
92 | 91 | imbi2d 329 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) ↔ ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ))) |
93 | 92 | ralbidv 2969 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) ↔ ∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ))) |
94 | | snelpwi 4839 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → {𝑋} ∈ 𝒫 𝐵) |
95 | 94 | adantl 481 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → {𝑋} ∈ 𝒫 𝐵) |
96 | 95 | biantrurd 528 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ) ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))) |
97 | 86, 93, 96 | 3bitrd 293 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))) |
98 | 4, 97 | syl5bb 271 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))) |
99 | | snex 4835 |
. . 3
⊢ {𝑋} ∈ V |
100 | 17, 83, 9, 8, 74 | islininds 42029 |
. . 3
⊢ (({𝑋} ∈ V ∧ 𝑀 ∈ LMod) → ({𝑋} linIndS 𝑀 ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))) |
101 | 99, 5, 100 | sylancr 694 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → ({𝑋} linIndS 𝑀 ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑𝑚 {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))) |
102 | 98, 101 | bitr4d 270 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ {𝑋} linIndS 𝑀)) |