Step | Hyp | Ref
| Expression |
1 | | elpwi 4117 |
. . . 4
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) → 𝑆 ⊆ (Base‘𝑀)) |
2 | 1 | ad2antrl 760 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → 𝑆 ⊆ (Base‘𝑀)) |
3 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → 𝑀 ∈ LMod) |
4 | 3 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) → (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) |
5 | 4 | ancomd 466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀))) |
6 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀))) |
7 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) → 𝑦 ∈ 𝐵) |
8 | 7 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → 𝑦 ∈ 𝐵) |
9 | 8 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑦 ∈ 𝐵) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → 𝑦 ∈ 𝐵) |
11 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑠 ∈ 𝑆) |
12 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → 𝑠 ∈ 𝑆) |
13 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))) |
14 | 10, 12, 13 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})))) |
15 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → 𝑔 finSupp 0 ) |
16 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(Base‘𝑀) =
(Base‘𝑀) |
17 | | lindslinind.r |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑅 = (Scalar‘𝑀) |
18 | | lindslinind.b |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝐵 = (Base‘𝑅) |
19 | | lindslinind.0 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 =
(0g‘𝑅) |
20 | | lindslinind.z |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑍 = (0g‘𝑀) |
21 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(invg‘𝑅) = (invg‘𝑅) |
22 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) |
23 | 16, 17, 18, 19, 20, 21, 22 | lincext2 42038 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀)) ∧
(𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))) ∧ 𝑔 finSupp 0 ) → (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ) |
24 | 6, 14, 15, 23 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ) |
25 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑆 ∈ 𝒫
(Base‘𝑀) ∧ 𝑀 ∈ LMod)) |
26 | 25 | ancomd 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀))) |
27 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀))) |
28 | 16, 17, 18, 19, 20, 21, 22 | lincext1 42037 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀)) ∧
(𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})))) → (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) ∈ (𝐵 ↑𝑚 𝑆)) |
29 | 27, 14, 28 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) ∈ (𝐵 ↑𝑚 𝑆)) |
30 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → (𝑓 finSupp 0 ↔ (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 )) |
31 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → (𝑓( linC ‘𝑀)𝑆) = ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆)) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍)) |
33 | 30, 32 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍))) |
34 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → (𝑓‘𝑥) = ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥)) |
35 | 34 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → ((𝑓‘𝑥) = 0 ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 )) |
36 | 35 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → (∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 )) |
37 | 33, 36 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) → (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) ↔ (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ))) |
38 | 37 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) ∈ (𝐵 ↑𝑚 𝑆) → (∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ))) |
39 | 29, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ))) |
40 | 39 | exp4a 631 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) finSupp 0 → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍 → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 )))) |
41 | 24, 40 | mpid 43 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍 → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ))) |
42 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
43 | 16, 17, 18, 19, 20, 21, 22 | lincext3 42039 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀)) ∧
(𝑦 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍) |
44 | 6, 14, 42, 43 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍) |
45 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑠 → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠)) |
46 | 45 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑠 → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ↔ ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = 0 )) |
47 | 46 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = 0 )) |
48 | 12, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = 0 )) |
49 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧))) = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))) |
50 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑠 → if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)) = ((invg‘𝑅)‘𝑦)) |
51 | 50 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑧 = 𝑠) → if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)) = ((invg‘𝑅)‘𝑦)) |
52 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((invg‘𝑅)‘𝑦) ∈ V |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) →
((invg‘𝑅)‘𝑦) ∈ V) |
54 | 49, 51, 11, 53 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = ((invg‘𝑅)‘𝑦)) |
55 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = ((invg‘𝑅)‘𝑦)) |
56 | 55 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = 0 ↔
((invg‘𝑅)‘𝑦) = 0 )) |
57 | 17 | lmodfgrp 18695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑀 ∈ LMod → 𝑅 ∈ Grp) |
58 | 18, 19, 21 | grpinvnzcl 17310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) →
((invg‘𝑅)‘𝑦) ∈ (𝐵 ∖ { 0 })) |
59 | | eldif 3550 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((invg‘𝑅)‘𝑦) ∈ (𝐵 ∖ { 0 }) ↔
(((invg‘𝑅)‘𝑦) ∈ 𝐵 ∧ ¬ ((invg‘𝑅)‘𝑦) ∈ { 0 })) |
60 | 52 | elsn 4140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((invg‘𝑅)‘𝑦) ∈ { 0 } ↔
((invg‘𝑅)‘𝑦) = 0 ) |
61 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (¬
((invg‘𝑅)‘𝑦) = 0 →
(((invg‘𝑅)‘𝑦) = 0 → (𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (𝑆 ∈ 𝒫 (Base‘𝑀) → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) |
62 | 61 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (¬
((invg‘𝑅)‘𝑦) = 0 → (𝑆 ∈ 𝒫 (Base‘𝑀) → (𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) |
63 | 60, 62 | sylnbi 319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (¬
((invg‘𝑅)‘𝑦) ∈ { 0 } → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) |
64 | 63 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((invg‘𝑅)‘𝑦) ∈ 𝐵 ∧ ¬ ((invg‘𝑅)‘𝑦) ∈ { 0 }) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) |
65 | 59, 64 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((invg‘𝑅)‘𝑦) ∈ (𝐵 ∖ { 0 }) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) |
66 | 58, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) |
67 | 66 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑅 ∈ Grp → (𝑦 ∈ (𝐵 ∖ { 0 }) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))))) |
68 | 57, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑀 ∈ LMod → (𝑦 ∈ (𝐵 ∖ { 0 }) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∈ 𝑉 → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))))) |
69 | 68 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑀 ∈ LMod → (𝑆 ∈ 𝑉 → (𝑆 ∈ 𝒫 (Base‘𝑀) → (𝑦 ∈ (𝐵 ∖ { 0 }) → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))))) |
70 | 69 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → (𝑆 ∈ 𝒫 (Base‘𝑀) → (𝑦 ∈ (𝐵 ∖ { 0 }) → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) |
71 | 70 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) → (𝑦 ∈ (𝐵 ∖ { 0 }) → (𝑠 ∈ 𝑆 → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) |
72 | 71 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑠 ∈ 𝑆 → (𝑦 ∈ (𝐵 ∖ { 0 }) → ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) →
(((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) |
73 | 72 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) →
(((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) |
74 | 73 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) →
(((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (((invg‘𝑅)‘𝑦) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
76 | 56, 75 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑠) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
77 | 48, 76 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
78 | 44, 77 | embantd 57 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → ((((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))( linC ‘𝑀)𝑆) = 𝑍 → ∀𝑥 ∈ 𝑆 ((𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑠, ((invg‘𝑅)‘𝑦), (𝑔‘𝑧)))‘𝑥) = 0 ) → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
79 | 41, 78 | syld 46 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → (∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
80 | 79 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑓 ∈
(𝐵
↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → ((((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ (𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
81 | 80 | expd 451 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑓 ∈
(𝐵
↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → (((𝑆 ∈ 𝒫
(Base‘𝑀) ∧ (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) |
82 | 81 | exp4c 634 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑓 ∈
(𝐵
↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) → (𝑆 ∈ 𝒫
(Base‘𝑀) →
((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → ((𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))))) |
83 | 82 | impcom 445 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧
∀𝑓 ∈ (𝐵 ↑𝑚
𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )) → ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → ((𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) |
84 | 83 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → ((𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → ((𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) |
85 | 84 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})) ∧ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
86 | 85 | expdimp 452 |
. . . . . . . . . . . . 13
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))) → ((𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
87 | 86 | expd 451 |
. . . . . . . . . . . 12
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))) → (𝑔 finSupp 0 → ((𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) |
88 | 87 | impcom 445 |
. . . . . . . . . . 11
⊢ ((𝑔 finSupp 0 ∧ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})))) → ((𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
89 | 88 | pm2.01d 180 |
. . . . . . . . . 10
⊢ ((𝑔 finSupp 0 ∧ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})))) → ¬ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) |
90 | 89 | olcd 407 |
. . . . . . . . 9
⊢ ((𝑔 finSupp 0 ∧ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})))) → (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
91 | | simpl 472 |
. . . . . . . . . 10
⊢ ((¬
𝑔 finSupp 0 ∧
((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})))) → ¬ 𝑔 finSupp 0 ) |
92 | 91 | orcd 406 |
. . . . . . . . 9
⊢ ((¬
𝑔 finSupp 0 ∧
((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠})))) → (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
93 | 90, 92 | pm2.61ian 827 |
. . . . . . . 8
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) ∧ 𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))) → (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
94 | 93 | ralrimiva 2949 |
. . . . . . 7
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
95 | | ralnex 2975 |
. . . . . . . 8
⊢
(∀𝑔 ∈
(𝐵
↑𝑚 (𝑆 ∖ {𝑠})) ¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ¬ ∃𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
96 | | ianor 508 |
. . . . . . . . 9
⊢ (¬
(𝑔 finSupp 0 ∧ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ (¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
97 | 96 | ralbii 2963 |
. . . . . . . 8
⊢
(∀𝑔 ∈
(𝐵
↑𝑚 (𝑆 ∖ {𝑠})) ¬ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
98 | 95, 97 | bitr3i 265 |
. . . . . . 7
⊢ (¬
∃𝑔 ∈ (𝐵 ↑𝑚
(𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∀𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(¬ 𝑔 finSupp 0 ∨ ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
99 | 94, 98 | sylibr 223 |
. . . . . 6
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ¬
∃𝑔 ∈ (𝐵 ↑𝑚
(𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
100 | 99 | intnand 953 |
. . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ¬ ((𝑦(
·𝑠 ‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) |
101 | 3 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → 𝑀 ∈ LMod) |
102 | 1 | ssdifssd 3710 |
. . . . . . . . . 10
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀)) |
103 | 102 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀)) |
104 | | difexg 4735 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∖ {𝑠}) ∈ V) |
105 | 104 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑆 ∖ {𝑠}) ∈ V) |
106 | | elpwg 4116 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ {𝑠}) ∈ V → ((𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀))) |
107 | 105, 106 | syl 17 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → ((𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀))) |
108 | 103, 107 | mpbird 246 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) |
109 | 108 | adantr 480 |
. . . . . . 7
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) |
110 | 16 | lspeqlco 42022 |
. . . . . . . . 9
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → (𝑀 LinCo (𝑆 ∖ {𝑠})) = ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) |
111 | 110 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠
‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) |
112 | 111 | bicomd 212 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠
‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})))) |
113 | 101, 109,
112 | syl2anc 691 |
. . . . . 6
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ (𝑦( ·𝑠
‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})))) |
114 | 3 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → 𝑀 ∈ LMod) |
115 | | difexg 4735 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∖ {𝑠}) ∈ V) |
116 | 115, 106 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
((𝑆 ∖ {𝑠}) ∈ 𝒫
(Base‘𝑀) ↔
(𝑆 ∖ {𝑠}) ⊆ (Base‘𝑀))) |
117 | 102, 116 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) →
(𝑆 ∖ {𝑠}) ∈ 𝒫
(Base‘𝑀)) |
118 | 117 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) |
119 | 114, 118 | jca 553 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀))) |
120 | 119 | adantr 480 |
. . . . . . 7
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → (𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀))) |
121 | 16, 17, 18 | lcoval 41995 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g‘𝑅) ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) |
122 | 19 | eqcomi 2619 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) = 0 |
123 | 122 | breq2i 4591 |
. . . . . . . . . . 11
⊢ (𝑔 finSupp
(0g‘𝑅)
↔ 𝑔 finSupp 0
) |
124 | 123 | anbi1i 727 |
. . . . . . . . . 10
⊢ ((𝑔 finSupp
(0g‘𝑅)
∧ (𝑦(
·𝑠 ‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ (𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
125 | 124 | rexbii 3023 |
. . . . . . . . 9
⊢
(∃𝑔 ∈
(𝐵
↑𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g‘𝑅) ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))) ↔ ∃𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) |
126 | 125 | anbi2i 726 |
. . . . . . . 8
⊢ (((𝑦(
·𝑠 ‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp (0g‘𝑅) ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))) ↔ ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠}))))) |
127 | 121, 126 | syl6bb 275 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∖ {𝑠}) ∈ 𝒫 (Base‘𝑀)) → ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) |
128 | 120, 127 | syl 17 |
. . . . . 6
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑦(
·𝑠 ‘𝑀)𝑠) ∈ (𝑀 LinCo (𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) |
129 | 113, 128 | bitrd 267 |
. . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ((𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})) ↔ ((𝑦( ·𝑠
‘𝑀)𝑠) ∈ (Base‘𝑀) ∧ ∃𝑔 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑔 finSupp 0 ∧ (𝑦( ·𝑠
‘𝑀)𝑠) = (𝑔( linC ‘𝑀)(𝑆 ∖ {𝑠})))))) |
130 | 100, 129 | mtbird 314 |
. . . 4
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) → ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) |
131 | 130 | ralrimivva 2954 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → ∀𝑠 ∈ 𝑆 ∀𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))) |
132 | 2, 131 | jca 553 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) → (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠 ∈ 𝑆 ∀𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠})))) |
133 | 132 | ex 449 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → ((𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ∀𝑓 ∈ (𝐵 ↑𝑚 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )) → (𝑆 ⊆ (Base‘𝑀) ∧ ∀𝑠 ∈ 𝑆 ∀𝑦 ∈ (𝐵 ∖ { 0 }) ¬ (𝑦(
·𝑠 ‘𝑀)𝑠) ∈ ((LSpan‘𝑀)‘(𝑆 ∖ {𝑠}))))) |