Step | Hyp | Ref
| Expression |
1 | | simp-4r 781 |
. . . . . . . . 9
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) |
2 | | fveq2 6774 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → (𝑎‘𝑢) = (𝑎‘𝑣)) |
3 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → 𝑢 = 𝑣) |
4 | 2, 3 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢) = ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)) |
5 | 4 | cbvmptv 5187 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)) |
6 | 5 | oveq2i 7286 |
. . . . . . . . 9
⊢ (𝑊 Σg
(𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣))) |
7 | 1, 6 | eqtr4di 2796 |
. . . . . . . 8
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 = (𝑊 Σg (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)))) |
8 | | simp-4r 781 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑎 finSupp
(0g‘(Scalar‘𝑊))) |
9 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑏 finSupp
(0g‘(Scalar‘𝑊))) |
10 | | simp-8l 788 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑊 ∈ LVec) |
11 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝐵 ∈ 𝐽) |
12 | 11 | ad6antr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝐵 ∈ 𝐽) |
13 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝑉 ⊆ 𝐵) |
14 | 13 | ad6antr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑉 ⊆ 𝐵) |
15 | | simp-5r 783 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) |
16 | | fvexd 6789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (Base‘(Scalar‘𝑊)) ∈ V) |
17 | 11, 13 | ssexd 5248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝑉 ∈ V) |
18 | 16, 17 | elmapd 8629 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉) ↔ 𝑎:𝑉⟶(Base‘(Scalar‘𝑊)))) |
19 | 18 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) → 𝑎:𝑉⟶(Base‘(Scalar‘𝑊))) |
20 | 10, 12, 14, 15, 19 | syl1111anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑎:𝑉⟶(Base‘(Scalar‘𝑊))) |
21 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) |
22 | | lveclmod 20368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
23 | 22 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝑊 ∈ LMod) |
24 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(Base‘𝑊) =
(Base‘𝑊) |
25 | | lbsdiflsp0.j |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 𝐽 = (LBasis‘𝑊) |
26 | 24, 25 | lbsss 20339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐵 ∈ 𝐽 → 𝐵 ⊆ (Base‘𝑊)) |
27 | 26 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝐵 ⊆ (Base‘𝑊)) |
28 | 27 | ssdifssd 4077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝐵 ∖ 𝑉) ⊆ (Base‘𝑊)) |
29 | | lbsdiflsp0.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 =
(0g‘𝑊) |
30 | | lbsdiflsp0.n |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 𝑁 = (LSpan‘𝑊) |
31 | 29, 24, 30 | 0ellsp 31565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑊 ∈ LMod ∧ (𝐵 ∖ 𝑉) ⊆ (Base‘𝑊)) → 0 ∈ (𝑁‘(𝐵 ∖ 𝑉))) |
32 | 23, 28, 31 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 0 ∈ (𝑁‘(𝐵 ∖ 𝑉))) |
33 | 32 | elfvexd 6808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝐵 ∖ 𝑉) ∈ V) |
34 | 16, 33 | elmapd 8629 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉)) ↔ 𝑏:(𝐵 ∖ 𝑉)⟶(Base‘(Scalar‘𝑊)))) |
35 | 34 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) → 𝑏:(𝐵 ∖ 𝑉)⟶(Base‘(Scalar‘𝑊))) |
36 | 10, 12, 14, 21, 35 | syl1111anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑏:(𝐵 ∖ 𝑉)⟶(Base‘(Scalar‘𝑊))) |
37 | | disjdif 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅ |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → (𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅) |
39 | 20, 36, 38 | fun2d 6638 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → (𝑎 ∪ 𝑏):(𝑉 ∪ (𝐵 ∖ 𝑉))⟶(Base‘(Scalar‘𝑊))) |
40 | | undif 4415 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑉 ⊆ 𝐵 ↔ (𝑉 ∪ (𝐵 ∖ 𝑉)) = 𝐵) |
41 | 14, 40 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → (𝑉 ∪ (𝐵 ∖ 𝑉)) = 𝐵) |
42 | 41 | feq2d 6586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → ((𝑎 ∪ 𝑏):(𝑉 ∪ (𝐵 ∖ 𝑉))⟶(Base‘(Scalar‘𝑊)) ↔ (𝑎 ∪ 𝑏):𝐵⟶(Base‘(Scalar‘𝑊)))) |
43 | 39, 42 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → (𝑎 ∪ 𝑏):𝐵⟶(Base‘(Scalar‘𝑊))) |
44 | 43 | ffund 6604 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → Fun (𝑎 ∪ 𝑏)) |
45 | 44 | fsuppunbi 9149 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → ((𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊)) ↔ (𝑎 finSupp
(0g‘(Scalar‘𝑊)) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))))) |
46 | 8, 9, 45 | mpbir2and 710 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → (𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊))) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊))) |
48 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(+g‘𝑊) = (+g‘𝑊) |
49 | | lmodcmn 20171 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd) |
50 | 22, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 ∈ LVec → 𝑊 ∈ CMnd) |
51 | 50 | ad9antr 739 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑊 ∈ CMnd) |
52 | 11 | ad7antr 735 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝐵 ∈ 𝐽) |
53 | 23 | ad8antr 737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝑊 ∈ LMod) |
54 | | elmapfn 8653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 ∈
((Base‘(Scalar‘𝑊)) ↑m 𝑉) → 𝑎 Fn 𝑉) |
55 | 54 | ad6antlr 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑎 Fn 𝑉) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → 𝑎 Fn 𝑉) |
57 | | elmapfn 8653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑏 ∈
((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉)) → 𝑏 Fn (𝐵 ∖ 𝑉)) |
58 | 57 | ad3antlr 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑏 Fn (𝐵 ∖ 𝑉)) |
59 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → 𝑏 Fn (𝐵 ∖ 𝑉)) |
60 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → (𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅) |
61 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → 𝑢 ∈ 𝑉) |
62 | | fvun1 6859 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 Fn 𝑉 ∧ 𝑏 Fn (𝐵 ∖ 𝑉) ∧ ((𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅ ∧ 𝑢 ∈ 𝑉)) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑎‘𝑢)) |
63 | 56, 59, 60, 61, 62 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑎‘𝑢)) |
64 | 63 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ 𝑉) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑎‘𝑢)) |
65 | 20 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ 𝑉) → 𝑎:𝑉⟶(Base‘(Scalar‘𝑊))) |
66 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ 𝑉) → 𝑢 ∈ 𝑉) |
67 | 65, 66 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ 𝑉) → (𝑎‘𝑢) ∈ (Base‘(Scalar‘𝑊))) |
68 | 64, 67 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ 𝑉) → ((𝑎 ∪ 𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊))) |
69 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → 𝑎 Fn 𝑉) |
70 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → 𝑏 Fn (𝐵 ∖ 𝑉)) |
71 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → (𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅) |
72 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → 𝑢 ∈ (𝐵 ∖ 𝑉)) |
73 | | fvun2 6860 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 Fn 𝑉 ∧ 𝑏 Fn (𝐵 ∖ 𝑉) ∧ ((𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅ ∧ 𝑢 ∈ (𝐵 ∖ 𝑉))) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑏‘𝑢)) |
74 | 69, 70, 71, 72, 73 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑏‘𝑢)) |
75 | 74 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑏‘𝑢)) |
76 | 36 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → 𝑏:(𝐵 ∖ 𝑉)⟶(Base‘(Scalar‘𝑊))) |
77 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → 𝑢 ∈ (𝐵 ∖ 𝑉)) |
78 | 76, 77 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → (𝑏‘𝑢) ∈ (Base‘(Scalar‘𝑊))) |
79 | 75, 78 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → ((𝑎 ∪ 𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊))) |
80 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ 𝐵) |
81 | 40 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑉 ⊆ 𝐵 → (𝑉 ∪ (𝐵 ∖ 𝑉)) = 𝐵) |
82 | 81 | ad8antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑉 ∪ (𝐵 ∖ 𝑉)) = 𝐵) |
83 | 82 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝐵 = (𝑉 ∪ (𝐵 ∖ 𝑉))) |
84 | 83 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝐵 = (𝑉 ∪ (𝐵 ∖ 𝑉))) |
85 | 80, 84 | eleqtrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ (𝑉 ∪ (𝐵 ∖ 𝑉))) |
86 | | elun 4083 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈ (𝑉 ∪ (𝐵 ∖ 𝑉)) ↔ (𝑢 ∈ 𝑉 ∨ 𝑢 ∈ (𝐵 ∖ 𝑉))) |
87 | 85, 86 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → (𝑢 ∈ 𝑉 ∨ 𝑢 ∈ (𝐵 ∖ 𝑉))) |
88 | 68, 79, 87 | mpjaodan 956 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → ((𝑎 ∪ 𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊))) |
89 | 27 | ad8antr 737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝐵 ⊆ (Base‘𝑊)) |
90 | 89, 80 | sseldd 3922 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ (Base‘𝑊)) |
91 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
92 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
93 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
94 | 24, 91, 92, 93 | lmodvscl 20140 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ LMod ∧ ((𝑎 ∪ 𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑢 ∈ (Base‘𝑊)) → (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢) ∈ (Base‘𝑊)) |
95 | 53, 88, 90, 94 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢) ∈ (Base‘𝑊)) |
96 | | simp-9l 790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑊 ∈ LVec) |
97 | 96, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑊 ∈ LMod) |
98 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (Scalar‘𝑊) = (Scalar‘𝑊)) |
99 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
100 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑎 ∪ 𝑏):𝐵⟶(Base‘(Scalar‘𝑊))) |
101 | 100 | feqmptd 6837 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑎 ∪ 𝑏) = (𝑢 ∈ 𝐵 ↦ ((𝑎 ∪ 𝑏)‘𝑢))) |
102 | 101, 47 | eqbrtrrd 5098 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑢 ∈ 𝐵 ↦ ((𝑎 ∪ 𝑏)‘𝑢)) finSupp
(0g‘(Scalar‘𝑊))) |
103 | 52, 97, 98, 24, 88, 90, 29, 99, 92, 102 | mptscmfsupp0 20188 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)) finSupp 0 ) |
104 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅) |
105 | 24, 29, 48, 51, 52, 95, 103, 104, 83 | gsumsplit2 19530 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = ((𝑊 Σg (𝑢 ∈ 𝑉 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)))(+g‘𝑊)(𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))))) |
106 | 63 | oveq1d 7290 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢) = ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)) |
107 | 106 | mpteq2dva 5174 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑢 ∈ 𝑉 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢))) |
108 | 107 | oveq2d 7291 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ 𝑉 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)))) |
109 | 74 | oveq1d 7290 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢) = ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢)) |
110 | 109 | mpteq2dva 5174 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢))) |
111 | 110 | oveq2d 7291 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢)))) |
112 | 108, 111 | oveq12d 7293 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((𝑊 Σg (𝑢 ∈ 𝑉 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)))(+g‘𝑊)(𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)))) = ((𝑊 Σg (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)))(+g‘𝑊)(𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢))))) |
113 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) |
114 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = 𝑣 → (𝑏‘𝑢) = (𝑏‘𝑣)) |
115 | 114, 3 | oveq12d 7293 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = 𝑣 → ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢) = ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)) |
116 | 115 | cbvmptv 5187 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)) |
117 | 116 | oveq2i 7286 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 Σg
(𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣))) |
118 | 113, 117 | eqtr4di 2796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢)))) |
119 | 7, 118 | oveq12d 7293 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑥(+g‘𝑊)((invg‘𝑊)‘𝑥)) = ((𝑊 Σg (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)))(+g‘𝑊)(𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢))))) |
120 | | lmodgrp 20130 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
121 | 96, 22, 120 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑊 ∈ Grp) |
122 | 13, 27 | sstrd 3931 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝑉 ⊆ (Base‘𝑊)) |
123 | 24, 30 | lspssv 20245 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ (Base‘𝑊)) → (𝑁‘𝑉) ⊆ (Base‘𝑊)) |
124 | 23, 122, 123 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝑁‘𝑉) ⊆ (Base‘𝑊)) |
125 | 124 | ad7antr 735 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑁‘𝑉) ⊆ (Base‘𝑊)) |
126 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) |
127 | 126 | elin2d 4133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → 𝑥 ∈ (𝑁‘𝑉)) |
128 | 127 | ad6antr 733 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 ∈ (𝑁‘𝑉)) |
129 | 125, 128 | sseldd 3922 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 ∈ (Base‘𝑊)) |
130 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(invg‘𝑊) = (invg‘𝑊) |
131 | 24, 48, 29, 130 | grprinv 18629 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Grp ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(+g‘𝑊)((invg‘𝑊)‘𝑥)) = 0 ) |
132 | 121, 129,
131 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑥(+g‘𝑊)((invg‘𝑊)‘𝑥)) = 0 ) |
133 | 112, 119,
132 | 3eqtr2d 2784 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((𝑊 Σg (𝑢 ∈ 𝑉 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)))(+g‘𝑊)(𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)))) = 0 ) |
134 | 105, 133 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) |
135 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (𝑐 finSupp
(0g‘(Scalar‘𝑊)) ↔ (𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊)))) |
136 | | fveq1 6773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (𝑐‘𝑢) = ((𝑎 ∪ 𝑏)‘𝑢)) |
137 | 136 | oveq1d 7290 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 = (𝑎 ∪ 𝑏) → ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢) = (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)) |
138 | 137 | mpteq2dv 5176 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) |
139 | 138 | oveq2d 7291 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)))) |
140 | 139 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = (𝑎 ∪ 𝑏) → ((𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ↔ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 )) |
141 | 135, 140 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = (𝑎 ∪ 𝑏) → ((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) ↔ ((𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ))) |
142 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))}) ↔ (𝑎 ∪ 𝑏) = (𝐵 ×
{(0g‘(Scalar‘𝑊))}))) |
143 | 141, 142 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))})) ↔ (((𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → (𝑎 ∪ 𝑏) = (𝐵 ×
{(0g‘(Scalar‘𝑊))})))) |
144 | 25 | lbslinds 21040 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐽 ⊆ (LIndS‘𝑊) |
145 | 144, 11 | sselid 3919 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝐵 ∈ (LIndS‘𝑊)) |
146 | 24, 93, 91, 92, 29, 99 | islinds5 31563 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ LMod ∧ 𝐵 ⊆ (Base‘𝑊)) → (𝐵 ∈ (LIndS‘𝑊) ↔ ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝐵)((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))})))) |
147 | 146 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LMod ∧ 𝐵 ⊆ (Base‘𝑊)) ∧ 𝐵 ∈ (LIndS‘𝑊)) → ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝐵)((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))}))) |
148 | 23, 27, 145, 147 | syl21anc 835 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝐵)((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))}))) |
149 | 148 | ad7antr 735 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝐵)((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))}))) |
150 | | fvexd 6789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (Base‘(Scalar‘𝑊)) ∈ V) |
151 | 150, 52 | elmapd 8629 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((𝑎 ∪ 𝑏) ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝐵) ↔ (𝑎 ∪ 𝑏):𝐵⟶(Base‘(Scalar‘𝑊)))) |
152 | 100, 151 | mpbird 256 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑎 ∪ 𝑏) ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝐵)) |
153 | 143, 149,
152 | rspcdva 3562 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (((𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → (𝑎 ∪ 𝑏) = (𝐵 ×
{(0g‘(Scalar‘𝑊))}))) |
154 | 47, 134, 153 | mp2and 696 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑎 ∪ 𝑏) = (𝐵 ×
{(0g‘(Scalar‘𝑊))})) |
155 | 154 | reseq1d 5890 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((𝑎 ∪ 𝑏) ↾ 𝑉) = ((𝐵 ×
{(0g‘(Scalar‘𝑊))}) ↾ 𝑉)) |
156 | | fnunres1 30945 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 Fn 𝑉 ∧ 𝑏 Fn (𝐵 ∖ 𝑉) ∧ (𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅) → ((𝑎 ∪ 𝑏) ↾ 𝑉) = 𝑎) |
157 | 55, 58, 104, 156 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((𝑎 ∪ 𝑏) ↾ 𝑉) = 𝑎) |
158 | | xpssres 5928 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ⊆ 𝐵 → ((𝐵 ×
{(0g‘(Scalar‘𝑊))}) ↾ 𝑉) = (𝑉 ×
{(0g‘(Scalar‘𝑊))})) |
159 | 158 | ad8antlr 738 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((𝐵 ×
{(0g‘(Scalar‘𝑊))}) ↾ 𝑉) = (𝑉 ×
{(0g‘(Scalar‘𝑊))})) |
160 | 155, 157,
159 | 3eqtr3d 2786 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑎 = (𝑉 ×
{(0g‘(Scalar‘𝑊))})) |
161 | 160 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → 𝑎 = (𝑉 ×
{(0g‘(Scalar‘𝑊))})) |
162 | 161 | fveq1d 6776 |
. . . . . . . . . . . . 13
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → (𝑎‘𝑢) = ((𝑉 ×
{(0g‘(Scalar‘𝑊))})‘𝑢)) |
163 | | fvex 6787 |
. . . . . . . . . . . . . . 15
⊢
(0g‘(Scalar‘𝑊)) ∈ V |
164 | 163 | fvconst2 7079 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ 𝑉 → ((𝑉 ×
{(0g‘(Scalar‘𝑊))})‘𝑢) = (0g‘(Scalar‘𝑊))) |
165 | 61, 164 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → ((𝑉 ×
{(0g‘(Scalar‘𝑊))})‘𝑢) = (0g‘(Scalar‘𝑊))) |
166 | 162, 165 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → (𝑎‘𝑢) = (0g‘(Scalar‘𝑊))) |
167 | 166 | oveq1d 7290 |
. . . . . . . . . . 11
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢) = ((0g‘(Scalar‘𝑊))(
·𝑠 ‘𝑊)𝑢)) |
168 | 122 | ad8antr 737 |
. . . . . . . . . . . . 13
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → 𝑉 ⊆ (Base‘𝑊)) |
169 | 168, 61 | sseldd 3922 |
. . . . . . . . . . . 12
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → 𝑢 ∈ (Base‘𝑊)) |
170 | 24, 91, 92, 99, 29 | lmod0vs 20156 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑢 ∈ (Base‘𝑊)) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑢) = 0 ) |
171 | 97, 169, 170 | syl2an2r 682 |
. . . . . . . . . . 11
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑢) = 0 ) |
172 | 167, 171 | eqtrd 2778 |
. . . . . . . . . 10
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢) = 0 ) |
173 | 172 | mpteq2dva 5174 |
. . . . . . . . 9
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑢 ∈ 𝑉 ↦ 0 )) |
174 | 173 | oveq2d 7291 |
. . . . . . . 8
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑢 ∈ 𝑉 ↦ 0 ))) |
175 | | cmnmnd 19402 |
. . . . . . . . . 10
⊢ (𝑊 ∈ CMnd → 𝑊 ∈ Mnd) |
176 | 51, 175 | syl 17 |
. . . . . . . . 9
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑊 ∈ Mnd) |
177 | 128 | elfvexd 6808 |
. . . . . . . . 9
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑉 ∈ V) |
178 | 29 | gsumz 18474 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Mnd ∧ 𝑉 ∈ V) → (𝑊 Σg
(𝑢 ∈ 𝑉 ↦ 0 )) = 0 ) |
179 | 176, 177,
178 | syl2anc 584 |
. . . . . . . 8
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ 𝑉 ↦ 0 )) = 0 ) |
180 | 7, 174, 179 | 3eqtrd 2782 |
. . . . . . 7
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 = 0 ) |
181 | 180 | anasss 467 |
. . . . . 6
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ (𝑏 finSupp
(0g‘(Scalar‘𝑊)) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣))))) → 𝑥 = 0 ) |
182 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
183 | 24, 182, 30 | lspcl 20238 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝐵 ∖ 𝑉) ⊆ (Base‘𝑊)) → (𝑁‘(𝐵 ∖ 𝑉)) ∈ (LSubSp‘𝑊)) |
184 | 23, 28, 183 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝑁‘(𝐵 ∖ 𝑉)) ∈ (LSubSp‘𝑊)) |
185 | 184 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → (𝑁‘(𝐵 ∖ 𝑉)) ∈ (LSubSp‘𝑊)) |
186 | 182 | lsssubg 20219 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘(𝐵 ∖ 𝑉)) ∈ (LSubSp‘𝑊)) → (𝑁‘(𝐵 ∖ 𝑉)) ∈ (SubGrp‘𝑊)) |
187 | 23, 185, 186 | syl2an2r 682 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → (𝑁‘(𝐵 ∖ 𝑉)) ∈ (SubGrp‘𝑊)) |
188 | 126 | elin1d 4132 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → 𝑥 ∈ (𝑁‘(𝐵 ∖ 𝑉))) |
189 | 130 | subginvcl 18764 |
. . . . . . . . 9
⊢ (((𝑁‘(𝐵 ∖ 𝑉)) ∈ (SubGrp‘𝑊) ∧ 𝑥 ∈ (𝑁‘(𝐵 ∖ 𝑉))) → ((invg‘𝑊)‘𝑥) ∈ (𝑁‘(𝐵 ∖ 𝑉))) |
190 | 187, 188,
189 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → ((invg‘𝑊)‘𝑥) ∈ (𝑁‘(𝐵 ∖ 𝑉))) |
191 | 30, 24, 93, 91, 99, 92, 23, 28 | ellspds 31564 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (((invg‘𝑊)‘𝑥) ∈ (𝑁‘(𝐵 ∖ 𝑉)) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))(𝑏 finSupp
(0g‘(Scalar‘𝑊)) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))))) |
192 | 191 | biimpa 477 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ ((invg‘𝑊)‘𝑥) ∈ (𝑁‘(𝐵 ∖ 𝑉))) → ∃𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))(𝑏 finSupp
(0g‘(Scalar‘𝑊)) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣))))) |
193 | 190, 192 | syldan 591 |
. . . . . . 7
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → ∃𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))(𝑏 finSupp
(0g‘(Scalar‘𝑊)) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣))))) |
194 | 193 | ad3antrrr 727 |
. . . . . 6
⊢
(((((((𝑊 ∈ LVec
∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ∃𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))(𝑏 finSupp
(0g‘(Scalar‘𝑊)) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣))))) |
195 | 181, 194 | r19.29a 3218 |
. . . . 5
⊢
(((((((𝑊 ∈ LVec
∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 = 0 ) |
196 | 195 | anasss 467 |
. . . 4
⊢
((((((𝑊 ∈ LVec
∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ (𝑎 finSupp
(0g‘(Scalar‘𝑊)) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣))))) → 𝑥 = 0 ) |
197 | 30, 24, 93, 91, 99, 92, 23, 122 | ellspds 31564 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝑥 ∈ (𝑁‘𝑉) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)(𝑎 finSupp
(0g‘(Scalar‘𝑊)) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))))) |
198 | 197 | biimpa 477 |
. . . . 5
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ (𝑁‘𝑉)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)(𝑎 finSupp
(0g‘(Scalar‘𝑊)) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣))))) |
199 | 127, 198 | syldan 591 |
. . . 4
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)(𝑎 finSupp
(0g‘(Scalar‘𝑊)) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣))))) |
200 | 196, 199 | r19.29a 3218 |
. . 3
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → 𝑥 = 0 ) |
201 | 29, 24, 30 | 0ellsp 31565 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ (Base‘𝑊)) → 0 ∈ (𝑁‘𝑉)) |
202 | 23, 122, 201 | syl2anc 584 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 0 ∈ (𝑁‘𝑉)) |
203 | 32, 202 | elind 4128 |
. . 3
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 0 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) |
204 | 200, 203 | eqsnd 30877 |
. 2
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 }) |
205 | 204 | 3impa 1109 |
1
⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 }) |