Step | Hyp | Ref
| Expression |
1 | | lveclmod 18927 |
. . . 4
⊢ (𝑀 ∈ LVec → 𝑀 ∈ LMod) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → 𝑀 ∈ LMod) |
3 | | simpr 476 |
. . 3
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → 𝑆 ∈ 𝒫 𝐵) |
4 | | islindeps2.r |
. . . . . 6
⊢ 𝑅 = (Scalar‘𝑀) |
5 | 4 | lvecdrng 18926 |
. . . . 5
⊢ (𝑀 ∈ LVec → 𝑅 ∈
DivRing) |
6 | | drngnzr 19083 |
. . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝑀 ∈ LVec → 𝑅 ∈ NzRing) |
8 | 7 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → 𝑅 ∈ NzRing) |
9 | | islindeps2.b |
. . . 4
⊢ 𝐵 = (Base‘𝑀) |
10 | | islindeps2.z |
. . . 4
⊢ 𝑍 = (0g‘𝑀) |
11 | | islindeps2.e |
. . . 4
⊢ 𝐸 = (Base‘𝑅) |
12 | | islindeps2.0 |
. . . 4
⊢ 0 =
(0g‘𝑅) |
13 | 9, 10, 4, 11, 12 | islindeps2 42066 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing) → (∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) → 𝑆 linDepS 𝑀)) |
14 | 2, 3, 8, 13 | syl3anc 1318 |
. 2
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → (∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) → 𝑆 linDepS 𝑀)) |
15 | 9, 10, 4, 11, 12 | islindeps 42036 |
. . 3
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑆 linDepS 𝑀 ↔ ∃𝑔 ∈ (𝐸 ↑𝑚 𝑆)(𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑠 ∈ 𝑆 (𝑔‘𝑠) ≠ 0 ))) |
16 | | df-3an 1033 |
. . . . . . 7
⊢ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑠 ∈ 𝑆 (𝑔‘𝑠) ≠ 0 ) ↔ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ ∃𝑠 ∈ 𝑆 (𝑔‘𝑠) ≠ 0 )) |
17 | | r19.42v 3073 |
. . . . . . 7
⊢
(∃𝑠 ∈
𝑆 ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 ) ↔ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ ∃𝑠 ∈ 𝑆 (𝑔‘𝑠) ≠ 0 )) |
18 | 16, 17 | bitr4i 266 |
. . . . . 6
⊢ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑠 ∈ 𝑆 (𝑔‘𝑠) ≠ 0 ) ↔ ∃𝑠 ∈ 𝑆 ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) |
19 | 18 | rexbii 3023 |
. . . . 5
⊢
(∃𝑔 ∈
(𝐸
↑𝑚 𝑆)(𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑠 ∈ 𝑆 (𝑔‘𝑠) ≠ 0 ) ↔ ∃𝑔 ∈ (𝐸 ↑𝑚 𝑆)∃𝑠 ∈ 𝑆 ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) |
20 | | rexcom 3080 |
. . . . 5
⊢
(∃𝑔 ∈
(𝐸
↑𝑚 𝑆)∃𝑠 ∈ 𝑆 ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 ) ↔ ∃𝑠 ∈ 𝑆 ∃𝑔 ∈ (𝐸 ↑𝑚 𝑆)((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) |
21 | 19, 20 | bitri 263 |
. . . 4
⊢
(∃𝑔 ∈
(𝐸
↑𝑚 𝑆)(𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑠 ∈ 𝑆 (𝑔‘𝑠) ≠ 0 ) ↔ ∃𝑠 ∈ 𝑆 ∃𝑔 ∈ (𝐸 ↑𝑚 𝑆)((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) |
22 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) ∧ 𝑠 ∈ 𝑆) → 𝑆 ∈ 𝒫 𝐵) |
23 | 1 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) ∧ 𝑠 ∈ 𝑆) → 𝑀 ∈ LMod) |
24 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆) |
25 | 22, 23, 24 | 3jca 1235 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) ∧ 𝑠 ∈ 𝑆) → (𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑠 ∈ 𝑆)) |
26 | 25 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → (𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑠 ∈ 𝑆)) |
27 | | simplr 788 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) |
28 | | elmapi 7765 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (𝐸 ↑𝑚 𝑆) → 𝑔:𝑆⟶𝐸) |
29 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝑔:𝑆⟶𝐸 ∧ 𝑠 ∈ 𝑆) → (𝑔‘𝑠) ∈ 𝐸) |
30 | 28, 24, 29 | syl2anr 494 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) → (𝑔‘𝑠) ∈ 𝐸) |
31 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 ) → (𝑔‘𝑠) ≠ 0 ) |
32 | 30, 31 | anim12i 588 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → ((𝑔‘𝑠) ∈ 𝐸 ∧ (𝑔‘𝑠) ≠ 0 )) |
33 | 5 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) ∧ 𝑠 ∈ 𝑆) → 𝑅 ∈ DivRing) |
34 | 33 | ad2antrr 758 |
. . . . . . . . . . 11
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → 𝑅 ∈
DivRing) |
35 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
36 | 11, 35, 12 | drngunit 18575 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ DivRing → ((𝑔‘𝑠) ∈ (Unit‘𝑅) ↔ ((𝑔‘𝑠) ∈ 𝐸 ∧ (𝑔‘𝑠) ≠ 0 ))) |
37 | 34, 36 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → ((𝑔‘𝑠) ∈ (Unit‘𝑅) ↔ ((𝑔‘𝑠) ∈ 𝐸 ∧ (𝑔‘𝑠) ≠ 0 ))) |
38 | 32, 37 | mpbird 246 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → (𝑔‘𝑠) ∈ (Unit‘𝑅)) |
39 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 ) → 𝑔 finSupp 0 ) |
40 | 39 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → 𝑔 finSupp 0 ) |
41 | | eqid 2610 |
. . . . . . . . . 10
⊢
(invg‘𝑅) = (invg‘𝑅) |
42 | | eqid 2610 |
. . . . . . . . . 10
⊢
(invr‘𝑅) = (invr‘𝑅) |
43 | | eqid 2610 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
44 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) = (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) |
45 | 9, 4, 11, 35, 12, 10, 41, 42, 43, 44 | lincresunit2 42061 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑠 ∈ 𝑆) ∧ (𝑔 ∈ (𝐸 ↑𝑚 𝑆) ∧ (𝑔‘𝑠) ∈ (Unit‘𝑅) ∧ 𝑔 finSupp 0 )) → (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) finSupp 0 ) |
46 | 26, 27, 38, 40, 45 | syl13anc 1320 |
. . . . . . . 8
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) finSupp 0 ) |
47 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) ∧ 𝑠 ∈ 𝑆) → 𝑀 ∈ LVec) |
48 | 22, 47, 24 | 3jca 1235 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) ∧ 𝑠 ∈ 𝑆) → (𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LVec ∧ 𝑠 ∈ 𝑆)) |
49 | 48 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → (𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LVec ∧ 𝑠 ∈ 𝑆)) |
50 | | simprr 792 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → (𝑔‘𝑠) ≠ 0 ) |
51 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 ) → (𝑔( linC ‘𝑀)𝑆) = 𝑍) |
52 | 51 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → (𝑔( linC ‘𝑀)𝑆) = 𝑍) |
53 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑔‘𝑧) = (𝑔‘𝑦)) |
54 | 53 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧)) = (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑦))) |
55 | 54 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) = (𝑦 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑦))) |
56 | 9, 4, 11, 35, 12, 10, 41, 42, 43, 55 | lincreslvec3 42065 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LVec ∧ 𝑠 ∈ 𝑆) ∧ (𝑔 ∈ (𝐸 ↑𝑚 𝑆) ∧ (𝑔‘𝑠) ≠ 0 ∧ 𝑔 finSupp 0 ) ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) → ((𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧)))( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) |
57 | 49, 27, 50, 40, 52, 56 | syl131anc 1331 |
. . . . . . . 8
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → ((𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧)))( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) |
58 | 9, 4, 11, 35, 12, 10, 41, 42, 43, 44 | lincresunit1 42060 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑠 ∈ 𝑆) ∧ (𝑔 ∈ (𝐸 ↑𝑚 𝑆) ∧ (𝑔‘𝑠) ∈ (Unit‘𝑅))) → (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))) |
59 | 26, 27, 38, 58 | syl12anc 1316 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))) |
60 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) → (𝑓 finSupp 0 ↔ (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) finSupp 0 )) |
61 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) → (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = ((𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧)))( linC ‘𝑀)(𝑆 ∖ {𝑠}))) |
62 | 61 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) → ((𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠 ↔ ((𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧)))( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠)) |
63 | 60, 62 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) ↔ ((𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧)))( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠))) |
64 | 63 | adantl 481 |
. . . . . . . . 9
⊢
((((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) ∧ 𝑓 = (𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧)))) → ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) ↔ ((𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧)))( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠))) |
65 | 59, 64 | rspcedv 3286 |
. . . . . . . 8
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → (((𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧))) finSupp 0 ∧ ((𝑧 ∈ (𝑆 ∖ {𝑠}) ↦ (((invr‘𝑅)‘((invg‘𝑅)‘(𝑔‘𝑠)))(.r‘𝑅)(𝑔‘𝑧)))( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) → ∃𝑓 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠))) |
66 | 46, 57, 65 | mp2and 711 |
. . . . . . 7
⊢
(((((𝑀 ∈ LVec
∧ 𝑆 ∈ 𝒫
𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) ∧ ((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 )) → ∃𝑓 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠)) |
67 | 66 | ex 449 |
. . . . . 6
⊢ ((((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ (𝐸 ↑𝑚 𝑆)) → (((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 ) → ∃𝑓 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠))) |
68 | 67 | rexlimdva 3013 |
. . . . 5
⊢ (((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) ∧ 𝑠 ∈ 𝑆) → (∃𝑔 ∈ (𝐸 ↑𝑚 𝑆)((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 ) → ∃𝑓 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠))) |
69 | 68 | reximdva 3000 |
. . . 4
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → (∃𝑠 ∈ 𝑆 ∃𝑔 ∈ (𝐸 ↑𝑚 𝑆)((𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍) ∧ (𝑔‘𝑠) ≠ 0 ) → ∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠))) |
70 | 21, 69 | syl5bi 231 |
. . 3
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → (∃𝑔 ∈ (𝐸 ↑𝑚 𝑆)(𝑔 finSupp 0 ∧ (𝑔( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑠 ∈ 𝑆 (𝑔‘𝑠) ≠ 0 ) → ∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠))) |
71 | 15, 70 | sylbid 229 |
. 2
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑆 linDepS 𝑀 → ∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠))) |
72 | 14, 71 | impbid 201 |
1
⊢ ((𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵) → (∃𝑠 ∈ 𝑆 ∃𝑓 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑠}))(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)(𝑆 ∖ {𝑠})) = 𝑠) ↔ 𝑆 linDepS 𝑀)) |