| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-ne 2940 | . . . . 5
⊢ ((𝑠 · 𝑋) ≠ 𝑍 ↔ ¬ (𝑠 · 𝑋) = 𝑍) | 
| 2 | 1 | ralbii 3092 | . . . 4
⊢
(∀𝑠 ∈
(𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ ∀𝑠 ∈ (𝑆 ∖ { 0 }) ¬ (𝑠 · 𝑋) = 𝑍) | 
| 3 |  | raldifsni 4794 | . . . 4
⊢
(∀𝑠 ∈
(𝑆 ∖ { 0 }) ¬
(𝑠 · 𝑋) = 𝑍 ↔ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) | 
| 4 | 2, 3 | bitri 275 | . . 3
⊢
(∀𝑠 ∈
(𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) | 
| 5 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → 𝑀 ∈ LMod) | 
| 6 | 5 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → 𝑀 ∈ LMod) | 
| 7 | 6 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑀 ∈ LMod) | 
| 8 |  | snlindsntor.s | . . . . . . . . . . . . . . . 16
⊢ 𝑆 = (Base‘𝑅) | 
| 9 |  | snlindsntor.r | . . . . . . . . . . . . . . . . 17
⊢ 𝑅 = (Scalar‘𝑀) | 
| 10 | 9 | fveq2i 6908 | . . . . . . . . . . . . . . . 16
⊢
(Base‘𝑅) =
(Base‘(Scalar‘𝑀)) | 
| 11 | 8, 10 | eqtri 2764 | . . . . . . . . . . . . . . 15
⊢ 𝑆 =
(Base‘(Scalar‘𝑀)) | 
| 12 | 11 | oveq1i 7442 | . . . . . . . . . . . . . 14
⊢ (𝑆 ↑m {𝑋}) =
((Base‘(Scalar‘𝑀)) ↑m {𝑋}) | 
| 13 | 12 | eleq2i 2832 | . . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝑆 ↑m {𝑋}) ↔ 𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑋})) | 
| 14 | 13 | biimpi 216 | . . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝑆 ↑m {𝑋}) → 𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑋})) | 
| 15 | 14 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑋})) | 
| 16 |  | snelpwi 5447 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ (Base‘𝑀) → {𝑋} ∈ 𝒫 (Base‘𝑀)) | 
| 17 |  | snlindsntor.b | . . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑀) | 
| 18 | 16, 17 | eleq2s 2858 | . . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐵 → {𝑋} ∈ 𝒫 (Base‘𝑀)) | 
| 19 | 18 | ad3antlr 731 | . . . . . . . . . . 11
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → {𝑋} ∈ 𝒫 (Base‘𝑀)) | 
| 20 |  | lincval 48331 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ LMod ∧ 𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m {𝑋}) ∧ {𝑋} ∈ 𝒫 (Base‘𝑀)) → (𝑓( linC ‘𝑀){𝑋}) = (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)))) | 
| 21 | 7, 15, 19, 20 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → (𝑓( linC ‘𝑀){𝑋}) = (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)))) | 
| 22 | 21 | eqeq1d 2738 | . . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 ↔ (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = 𝑍)) | 
| 23 | 22 | anbi2d 630 | . . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) ↔ (𝑓 finSupp 0 ∧ (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = 𝑍))) | 
| 24 |  | lmodgrp 20866 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Grp) | 
| 25 | 24 | grpmndd 18965 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Mnd) | 
| 26 | 25 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑀 ∈ Mnd) | 
| 27 |  | simpllr 775 | . . . . . . . . . . . 12
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑋 ∈ 𝐵) | 
| 28 |  | elmapi 8890 | . . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (𝑆 ↑m {𝑋}) → 𝑓:{𝑋}⟶𝑆) | 
| 29 | 6 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → 𝑀 ∈ LMod) | 
| 30 |  | snidg 4659 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ {𝑋}) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ {𝑋}) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → 𝑋 ∈ {𝑋}) | 
| 33 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ 𝑋 ∈ {𝑋}) → (𝑓‘𝑋) ∈ 𝑆) | 
| 34 | 32, 33 | sylan2 593 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → (𝑓‘𝑋) ∈ 𝑆) | 
| 35 |  | simprlr 779 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → 𝑋 ∈ 𝐵) | 
| 36 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) | 
| 37 | 17, 9, 36, 8 | lmodvscl 20877 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ LMod ∧ (𝑓‘𝑋) ∈ 𝑆 ∧ 𝑋 ∈ 𝐵) → ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵) | 
| 38 | 29, 34, 35, 37 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) → ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵) | 
| 39 | 38 | expcom 413 | . . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → (𝑓:{𝑋}⟶𝑆 → ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵)) | 
| 40 | 28, 39 | syl5com 31 | . . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝑆 ↑m {𝑋}) → (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵)) | 
| 41 | 40 | impcom 407 | . . . . . . . . . . . 12
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵) | 
| 42 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → (𝑓‘𝑥) = (𝑓‘𝑋)) | 
| 43 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) | 
| 44 | 42, 43 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥) = ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋)) | 
| 45 | 17, 44 | gsumsn 19973 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) ∈ 𝐵) → (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋)) | 
| 46 | 26, 27, 41, 45 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋)) | 
| 47 | 46 | eqeq1d 2738 | . . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = 𝑍 ↔ ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍)) | 
| 48 | 30, 33 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ ((𝑓:{𝑋}⟶𝑆 ∧ 𝑋 ∈ 𝐵) → (𝑓‘𝑋) ∈ 𝑆) | 
| 49 | 48 | expcom 413 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐵 → (𝑓:{𝑋}⟶𝑆 → (𝑓‘𝑋) ∈ 𝑆)) | 
| 50 | 49 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (𝑓:{𝑋}⟶𝑆 → (𝑓‘𝑋) ∈ 𝑆)) | 
| 51 |  | snlindsntor.t | . . . . . . . . . . . . . . . . 17
⊢  · = (
·𝑠 ‘𝑀) | 
| 52 | 51 | oveqi 7445 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓‘𝑋) · 𝑋) = ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) | 
| 53 | 52 | eqeq1i 2741 | . . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑋) · 𝑋) = 𝑍 ↔ ((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍) | 
| 54 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (𝑓‘𝑋) → (𝑠 · 𝑋) = ((𝑓‘𝑋) · 𝑋)) | 
| 55 | 54 | eqeq1d 2738 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑓‘𝑋) → ((𝑠 · 𝑋) = 𝑍 ↔ ((𝑓‘𝑋) · 𝑋) = 𝑍)) | 
| 56 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑓‘𝑋) → (𝑠 = 0 ↔ (𝑓‘𝑋) = 0 )) | 
| 57 | 55, 56 | imbi12d 344 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑓‘𝑋) → (((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) ↔ (((𝑓‘𝑋) · 𝑋) = 𝑍 → (𝑓‘𝑋) = 0 ))) | 
| 58 | 57 | rspcva 3619 | . . . . . . . . . . . . . . 15
⊢ (((𝑓‘𝑋) ∈ 𝑆 ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → (((𝑓‘𝑋) · 𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )) | 
| 59 | 53, 58 | biimtrrid 243 | . . . . . . . . . . . . . 14
⊢ (((𝑓‘𝑋) ∈ 𝑆 ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → (((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )) | 
| 60 | 59 | ex 412 | . . . . . . . . . . . . 13
⊢ ((𝑓‘𝑋) ∈ 𝑆 → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → (((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 ))) | 
| 61 | 28, 50, 60 | syl56 36 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (𝑓 ∈ (𝑆 ↑m {𝑋}) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → (((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )))) | 
| 62 | 61 | com23 86 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → (𝑓 ∈ (𝑆 ↑m {𝑋}) → (((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )))) | 
| 63 | 62 | imp31 417 | . . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → (((𝑓‘𝑋)( ·𝑠
‘𝑀)𝑋) = 𝑍 → (𝑓‘𝑋) = 0 )) | 
| 64 | 47, 63 | sylbid 240 | . . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = 𝑍 → (𝑓‘𝑋) = 0 )) | 
| 65 | 64 | adantld 490 | . . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓 finSupp 0 ∧ (𝑀 Σg (𝑥 ∈ {𝑋} ↦ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) = 𝑍) → (𝑓‘𝑋) = 0 )) | 
| 66 | 23, 65 | sylbid 240 | . . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 )) | 
| 67 | 66 | ralrimiva 3145 | . . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 )) → ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 )) | 
| 68 | 67 | ex 412 | . . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) → ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ))) | 
| 69 |  | impexp 450 | . . . . . . . 8
⊢ (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) ↔ (𝑓 finSupp 0 → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ))) | 
| 70 | 28 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑓:{𝑋}⟶𝑆) | 
| 71 |  | snfi 9084 | . . . . . . . . . . 11
⊢ {𝑋} ∈ Fin | 
| 72 | 71 | a1i 11 | . . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → {𝑋} ∈ Fin) | 
| 73 |  | snlindsntor.0 | . . . . . . . . . . . 12
⊢  0 =
(0g‘𝑅) | 
| 74 | 73 | fvexi 6919 | . . . . . . . . . . 11
⊢  0 ∈
V | 
| 75 | 74 | a1i 11 | . . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 0 ∈ V) | 
| 76 | 70, 72, 75 | fdmfifsupp 9416 | . . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → 𝑓 finSupp 0 ) | 
| 77 |  | pm2.27 42 | . . . . . . . . 9
⊢ (𝑓 finSupp 0 → ((𝑓 finSupp 0 → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ))) | 
| 78 | 76, 77 | syl 17 | . . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → ((𝑓 finSupp 0 → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 )) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ))) | 
| 79 | 69, 78 | biimtrid 242 | . . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) ∧ 𝑓 ∈ (𝑆 ↑m {𝑋})) → (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) → ((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ))) | 
| 80 | 79 | ralimdva 3166 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) → ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ))) | 
| 81 |  | snlindsntor.z | . . . . . . 7
⊢ 𝑍 = (0g‘𝑀) | 
| 82 | 17, 9, 8, 73, 81, 51 | snlindsntorlem 48392 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓( linC ‘𝑀){𝑋}) = 𝑍 → (𝑓‘𝑋) = 0 ) → ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) | 
| 83 | 80, 82 | syld 47 | . . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) → ∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ))) | 
| 84 | 68, 83 | impbid 212 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) ↔ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ))) | 
| 85 |  | fveqeq2 6914 | . . . . . . . . 9
⊢ (𝑦 = 𝑋 → ((𝑓‘𝑦) = 0 ↔ (𝑓‘𝑋) = 0 )) | 
| 86 | 85 | ralsng 4674 | . . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ↔ (𝑓‘𝑋) = 0 )) | 
| 87 | 86 | adantl 481 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ↔ (𝑓‘𝑋) = 0 )) | 
| 88 | 87 | bicomd 223 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → ((𝑓‘𝑋) = 0 ↔ ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )) | 
| 89 | 88 | imbi2d 340 | . . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) ↔ ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ))) | 
| 90 | 89 | ralbidv 3177 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → (𝑓‘𝑋) = 0 ) ↔ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ))) | 
| 91 |  | snelpwi 5447 | . . . . . 6
⊢ (𝑋 ∈ 𝐵 → {𝑋} ∈ 𝒫 𝐵) | 
| 92 | 91 | adantl 481 | . . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → {𝑋} ∈ 𝒫 𝐵) | 
| 93 | 92 | biantrurd 532 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 ) ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))) | 
| 94 | 84, 90, 93 | 3bitrd 305 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ 𝑆 ((𝑠 · 𝑋) = 𝑍 → 𝑠 = 0 ) ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))) | 
| 95 | 4, 94 | bitrid 283 | . 2
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))) | 
| 96 |  | snex 5435 | . . 3
⊢ {𝑋} ∈ V | 
| 97 | 17, 81, 9, 8, 73 | islininds 48368 | . . 3
⊢ (({𝑋} ∈ V ∧ 𝑀 ∈ LMod) → ({𝑋} linIndS 𝑀 ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))) | 
| 98 | 96, 5, 97 | sylancr 587 | . 2
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → ({𝑋} linIndS 𝑀 ↔ ({𝑋} ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝑆 ↑m {𝑋})((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀){𝑋}) = 𝑍) → ∀𝑦 ∈ {𝑋} (𝑓‘𝑦) = 0 )))) | 
| 99 | 95, 98 | bitr4d 282 | 1
⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵) → (∀𝑠 ∈ (𝑆 ∖ { 0 })(𝑠 · 𝑋) ≠ 𝑍 ↔ {𝑋} linIndS 𝑀)) |