Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . 3
⊢ ((𝑓‘𝑥) = 0 → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 )) |
2 | 1 | 2a1d 26 |
. 2
⊢ ((𝑓‘𝑥) = 0 → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 )))) |
3 | | elmapi 7765 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) → 𝑓:𝑆⟶𝐵) |
4 | | ffvelrn 6265 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑆⟶𝐵 ∧ 𝑥 ∈ 𝑆) → (𝑓‘𝑥) ∈ 𝐵) |
5 | 4 | expcom 450 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑆 → (𝑓:𝑆⟶𝐵 → (𝑓‘𝑥) ∈ 𝐵)) |
6 | 5 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑓:𝑆⟶𝐵 → (𝑓‘𝑥) ∈ 𝐵)) |
7 | 6 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓:𝑆⟶𝐵 → (𝑓‘𝑥) ∈ 𝐵)) |
8 | 7 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑓:𝑆⟶𝐵 → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓‘𝑥) ∈ 𝐵)) |
9 | 3, 8 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓‘𝑥) ∈ 𝐵)) |
10 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓‘𝑥) ∈ 𝐵)) |
11 | 10 | impcom 445 |
. . . . . . . 8
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑓‘𝑥) ∈ 𝐵) |
12 | 11 | biantrurd 528 |
. . . . . . 7
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → ((𝑓‘𝑥) ≠ 0 ↔ ((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑓‘𝑥) ≠ 0 ))) |
13 | | df-ne 2782 |
. . . . . . . 8
⊢ ((𝑓‘𝑥) ≠ 0 ↔ ¬ (𝑓‘𝑥) = 0 ) |
14 | 13 | bicomi 213 |
. . . . . . 7
⊢ (¬
(𝑓‘𝑥) = 0 ↔ (𝑓‘𝑥) ≠ 0 ) |
15 | | eldifsn 4260 |
. . . . . . 7
⊢ ((𝑓‘𝑥) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑓‘𝑥) ∈ 𝐵 ∧ (𝑓‘𝑥) ≠ 0 )) |
16 | 12, 14, 15 | 3bitr4g 302 |
. . . . . 6
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (¬ (𝑓‘𝑥) = 0 ↔ (𝑓‘𝑥) ∈ (𝐵 ∖ { 0 }))) |
17 | | lindslinind.r |
. . . . . . . . . . . 12
⊢ 𝑅 = (Scalar‘𝑀) |
18 | 17 | lmodfgrp 18695 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ LMod → 𝑅 ∈ Grp) |
19 | 18 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → 𝑅 ∈ Grp) |
20 | 19 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → 𝑅 ∈ Grp) |
21 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → 𝑅 ∈ Grp) |
22 | | lindslinind.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
23 | | lindslinind.0 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑅) |
24 | | eqid 2610 |
. . . . . . . . 9
⊢
(invg‘𝑅) = (invg‘𝑅) |
25 | 22, 23, 24 | grpinvnzcl 17310 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ (𝑓‘𝑥) ∈ (𝐵 ∖ { 0 })) →
((invg‘𝑅)‘(𝑓‘𝑥)) ∈ (𝐵 ∖ { 0 })) |
26 | 21, 25 | sylan 487 |
. . . . . . 7
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) ∧ (𝑓‘𝑥) ∈ (𝐵 ∖ { 0 })) →
((invg‘𝑅)‘(𝑓‘𝑥)) ∈ (𝐵 ∖ { 0 })) |
27 | 26 | ex 449 |
. . . . . 6
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → ((𝑓‘𝑥) ∈ (𝐵 ∖ { 0 }) →
((invg‘𝑅)‘(𝑓‘𝑥)) ∈ (𝐵 ∖ { 0 }))) |
28 | 16, 27 | sylbid 229 |
. . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (¬ (𝑓‘𝑥) = 0 →
((invg‘𝑅)‘(𝑓‘𝑥)) ∈ (𝐵 ∖ { 0 }))) |
29 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((invg‘𝑅)‘(𝑓‘𝑥)) → (𝑦( ·𝑠
‘𝑀)𝑥) = (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥)) |
30 | 29 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑦 = ((invg‘𝑅)‘(𝑓‘𝑥)) → ((𝑦( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))) |
31 | 30 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑦 = ((invg‘𝑅)‘(𝑓‘𝑥)) → (¬ (𝑦( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))) |
32 | 31 | orbi2d 734 |
. . . . . . . . 9
⊢ (𝑦 = ((invg‘𝑅)‘(𝑓‘𝑥)) → ((¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) ↔ (¬ 𝑔 finSupp 0 ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))))) |
33 | 32 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑦 = ((invg‘𝑅)‘(𝑓‘𝑥)) → (∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) ↔ ∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))))) |
34 | 33 | rspcva 3280 |
. . . . . . 7
⊢
((((invg‘𝑅)‘(𝑓‘𝑥)) ∈ (𝐵 ∖ { 0 }) ∧ ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))) → ∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))) |
35 | | simpl 472 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) |
36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) |
37 | | simplrl 796 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → 𝑆 ⊆ (Base‘𝑀)) |
38 | | simplrr 797 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → 𝑥 ∈ 𝑆) |
39 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → 𝑓 ∈ (𝐵 ↑𝑚 𝑆)) |
40 | 39 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → 𝑓 ∈ (𝐵 ↑𝑚 𝑆)) |
41 | | lindslinind.z |
. . . . . . . . . 10
⊢ 𝑍 = (0g‘𝑀) |
42 | | eqid 2610 |
. . . . . . . . . 10
⊢
((invg‘𝑅)‘(𝑓‘𝑥)) = ((invg‘𝑅)‘(𝑓‘𝑥)) |
43 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑓 ↾ (𝑆 ∖ {𝑥})) = (𝑓 ↾ (𝑆 ∖ {𝑥})) |
44 | 17, 22, 23, 41, 42, 43 | lindslinindimp2lem2 42042 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑𝑚 𝑆))) → (𝑓 ↾ (𝑆 ∖ {𝑥})) ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))) |
45 | 36, 37, 38, 40, 44 | syl13anc 1320 |
. . . . . . . 8
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑓 ↾ (𝑆 ∖ {𝑥})) ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))) |
46 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑓 ↾ (𝑆 ∖ {𝑥})) → 𝑔 = (𝑓 ↾ (𝑆 ∖ {𝑥}))) |
47 | 23 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑓 ↾ (𝑆 ∖ {𝑥})) → 0 =
(0g‘𝑅)) |
48 | 46, 47 | breq12d 4596 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ↾ (𝑆 ∖ {𝑥})) → (𝑔 finSupp 0 ↔ (𝑓 ↾ (𝑆 ∖ {𝑥})) finSupp (0g‘𝑅))) |
49 | 48 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑓 ↾ (𝑆 ∖ {𝑥})) → (¬ 𝑔 finSupp 0 ↔ ¬ (𝑓 ↾ (𝑆 ∖ {𝑥})) finSupp (0g‘𝑅))) |
50 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑓 ↾ (𝑆 ∖ {𝑥})) → (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥}))) |
51 | 50 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ↾ (𝑆 ∖ {𝑥})) → ((((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥})))) |
52 | 51 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑓 ↾ (𝑆 ∖ {𝑥})) → (¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥})))) |
53 | 49, 52 | orbi12d 742 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑓 ↾ (𝑆 ∖ {𝑥})) → ((¬ 𝑔 finSupp 0 ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) ↔ (¬ (𝑓 ↾ (𝑆 ∖ {𝑥})) finSupp (0g‘𝑅) ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥}))))) |
54 | 53 | rspcva 3280 |
. . . . . . . . . . 11
⊢ (((𝑓 ↾ (𝑆 ∖ {𝑥})) ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥})) ∧ ∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))) → (¬ (𝑓 ↾ (𝑆 ∖ {𝑥})) finSupp (0g‘𝑅) ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥})))) |
55 | 23 | breq2i 4591 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 finSupp 0 ↔ 𝑓 finSupp (0g‘𝑅)) |
56 | 55 | biimpi 205 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 finSupp 0 → 𝑓 finSupp (0g‘𝑅)) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → 𝑓 finSupp (0g‘𝑅)) |
58 | 57 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → 𝑓 finSupp (0g‘𝑅)) |
59 | 58 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → 𝑓 finSupp (0g‘𝑅)) |
60 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑅) ∈ V |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (0g‘𝑅) ∈ V) |
62 | 59, 61 | fsuppres 8183 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑓 ↾ (𝑆 ∖ {𝑥})) finSupp (0g‘𝑅)) |
63 | 62 | pm2.24d 146 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (¬ (𝑓 ↾ (𝑆 ∖ {𝑥})) finSupp (0g‘𝑅) → (𝑓‘𝑥) = 0 )) |
64 | 63 | com12 32 |
. . . . . . . . . . . 12
⊢ (¬
(𝑓 ↾ (𝑆 ∖ {𝑥})) finSupp (0g‘𝑅) → ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑓‘𝑥) = 0 )) |
65 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → 𝑀 ∈ LMod) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → 𝑀 ∈ LMod) |
67 | 17 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑅) =
(Base‘(Scalar‘𝑀)) |
68 | 22, 67 | eqtr2i 2633 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘(Scalar‘𝑀)) = 𝐵 |
69 | 68 | oveq1i 6559 |
. . . . . . . . . . . . . . . . 17
⊢
((Base‘(Scalar‘𝑀)) ↑𝑚 (𝑆 ∖ {𝑥})) = (𝐵 ↑𝑚 (𝑆 ∖ {𝑥})) |
70 | 45, 69 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑓 ↾ (𝑆 ∖ {𝑥})) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
(𝑆 ∖ {𝑥}))) |
71 | | ssdifss 3703 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ⊆ (Base‘𝑀) → (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀)) |
72 | 71 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀)) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀)) |
74 | | difexg 4735 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∖ {𝑥}) ∈ V) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → (𝑆 ∖ {𝑥}) ∈ V) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ∈ V) |
77 | | elpwg 4116 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∖ {𝑥}) ∈ V → ((𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀))) |
79 | 73, 78 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀)) |
80 | 79 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀)) |
81 | | lincval 41992 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ LMod ∧ (𝑓 ↾ (𝑆 ∖ {𝑥})) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
(𝑆 ∖ {𝑥})) ∧ (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀)) → ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥})) = (𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑥}) ↦ (((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑧)( ·𝑠
‘𝑀)𝑧)))) |
82 | 66, 70, 80, 81 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥})) = (𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑥}) ↦ (((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑧)( ·𝑠
‘𝑀)𝑧)))) |
83 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (𝑆 ∖ {𝑥}) → ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑧) = (𝑓‘𝑧)) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) ∧ 𝑧 ∈ (𝑆 ∖ {𝑥})) → ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑧) = (𝑓‘𝑧)) |
85 | 84 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) ∧ 𝑧 ∈ (𝑆 ∖ {𝑥})) → (((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑧)( ·𝑠
‘𝑀)𝑧) = ((𝑓‘𝑧)( ·𝑠
‘𝑀)𝑧)) |
86 | 85 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑧 ∈ (𝑆 ∖ {𝑥}) ↦ (((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑧)( ·𝑠
‘𝑀)𝑧)) = (𝑧 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑧)( ·𝑠
‘𝑀)𝑧))) |
87 | 86 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑥}) ↦ (((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑧)( ·𝑠
‘𝑀)𝑧))) = (𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑧)( ·𝑠
‘𝑀)𝑧)))) |
88 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) |
89 | | 3anass 1035 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) ↔ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) |
90 | 89 | bicomi 213 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) ↔ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) |
91 | 90 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) |
92 | 91 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) |
93 | 17, 22, 23, 41, 42, 43 | lindslinindimp2lem4 42044 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑧)( ·𝑠
‘𝑀)𝑧))) = (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥)) |
94 | 36, 88, 92, 93 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑀 Σg (𝑧 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑧)( ·𝑠
‘𝑀)𝑧))) = (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥)) |
95 | 82, 87, 94 | 3eqtrrd 2649 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥}))) |
96 | 95 | pm2.24d 146 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥})) → (𝑓‘𝑥) = 0 )) |
97 | 96 | com12 32 |
. . . . . . . . . . . 12
⊢ (¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥})) → ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑓‘𝑥) = 0 )) |
98 | 64, 97 | jaoi 393 |
. . . . . . . . . . 11
⊢ ((¬
(𝑓 ↾ (𝑆 ∖ {𝑥})) finSupp (0g‘𝑅) ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑓‘𝑥) = 0 )) |
99 | 54, 98 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑓 ↾ (𝑆 ∖ {𝑥})) ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥})) ∧ ∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))) → ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑓‘𝑥) = 0 )) |
100 | 99 | ex 449 |
. . . . . . . . 9
⊢ ((𝑓 ↾ (𝑆 ∖ {𝑥})) ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥})) → (∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (𝑓‘𝑥) = 0 ))) |
101 | 100 | com23 84 |
. . . . . . . 8
⊢ ((𝑓 ↾ (𝑆 ∖ {𝑥})) ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥})) → ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 ))) |
102 | 45, 101 | mpcom 37 |
. . . . . . 7
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬
(((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 )) |
103 | 34, 102 | syl5 33 |
. . . . . 6
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → ((((invg‘𝑅)‘(𝑓‘𝑥)) ∈ (𝐵 ∖ { 0 }) ∧ ∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥})))) → (𝑓‘𝑥) = 0 )) |
104 | 103 | expd 451 |
. . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (((invg‘𝑅)‘(𝑓‘𝑥)) ∈ (𝐵 ∖ { 0 }) → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 ))) |
105 | 28, 104 | syld 46 |
. . . 4
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (¬ (𝑓‘𝑥) = 0 → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 ))) |
106 | 105 | com12 32 |
. . 3
⊢ (¬
(𝑓‘𝑥) = 0 → ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍))) → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 ))) |
107 | 106 | expd 451 |
. 2
⊢ (¬
(𝑓‘𝑥) = 0 → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 )))) |
108 | 2, 107 | pm2.61i 175 |
1
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (∀𝑦 ∈ (𝐵 ∖ { 0 })∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑥) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑥}))) → (𝑓‘𝑥) = 0 ))) |