| Step | Hyp | Ref
| Expression |
| 1 | | simp-4r 784 |
. . . . . . . . 9
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) |
| 2 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → (𝑎‘𝑢) = (𝑎‘𝑣)) |
| 3 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → 𝑢 = 𝑣) |
| 4 | 2, 3 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢) = ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)) |
| 5 | 4 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)) |
| 6 | 5 | oveq2i 7442 |
. . . . . . . . 9
⊢ (𝑊 Σg
(𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣))) |
| 7 | 1, 6 | eqtr4di 2795 |
. . . . . . . 8
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 = (𝑊 Σg (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)))) |
| 8 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑎 finSupp
(0g‘(Scalar‘𝑊))) |
| 9 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑏 finSupp
(0g‘(Scalar‘𝑊))) |
| 10 | | simp-8l 791 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑊 ∈ LVec) |
| 11 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝐵 ∈ 𝐽) |
| 12 | 11 | ad6antr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝐵 ∈ 𝐽) |
| 13 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝑉 ⊆ 𝐵) |
| 14 | 13 | ad6antr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑉 ⊆ 𝐵) |
| 15 | | simp-5r 786 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) |
| 16 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (Base‘(Scalar‘𝑊)) ∈ V) |
| 17 | 11, 13 | ssexd 5324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝑉 ∈ V) |
| 18 | 16, 17 | elmapd 8880 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉) ↔ 𝑎:𝑉⟶(Base‘(Scalar‘𝑊)))) |
| 19 | 18 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) → 𝑎:𝑉⟶(Base‘(Scalar‘𝑊))) |
| 20 | 10, 12, 14, 15, 19 | syl1111anc 841 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑎:𝑉⟶(Base‘(Scalar‘𝑊))) |
| 21 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) |
| 22 | | lveclmod 21105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
| 23 | 22 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝑊 ∈ LMod) |
| 24 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 25 | | lbsdiflsp0.j |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 𝐽 = (LBasis‘𝑊) |
| 26 | 24, 25 | lbsss 21076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐵 ∈ 𝐽 → 𝐵 ⊆ (Base‘𝑊)) |
| 27 | 26 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝐵 ⊆ (Base‘𝑊)) |
| 28 | 27 | ssdifssd 4147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝐵 ∖ 𝑉) ⊆ (Base‘𝑊)) |
| 29 | | lbsdiflsp0.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 =
(0g‘𝑊) |
| 30 | | lbsdiflsp0.n |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 𝑁 = (LSpan‘𝑊) |
| 31 | 29, 24, 30 | 0ellsp 33397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑊 ∈ LMod ∧ (𝐵 ∖ 𝑉) ⊆ (Base‘𝑊)) → 0 ∈ (𝑁‘(𝐵 ∖ 𝑉))) |
| 32 | 23, 28, 31 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 0 ∈ (𝑁‘(𝐵 ∖ 𝑉))) |
| 33 | 32 | elfvexd 6945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝐵 ∖ 𝑉) ∈ V) |
| 34 | 16, 33 | elmapd 8880 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉)) ↔ 𝑏:(𝐵 ∖ 𝑉)⟶(Base‘(Scalar‘𝑊)))) |
| 35 | 34 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) → 𝑏:(𝐵 ∖ 𝑉)⟶(Base‘(Scalar‘𝑊))) |
| 36 | 10, 12, 14, 21, 35 | syl1111anc 841 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → 𝑏:(𝐵 ∖ 𝑉)⟶(Base‘(Scalar‘𝑊))) |
| 37 | | disjdif 4472 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 6772 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → (𝑎 ∪ 𝑏):(𝑉 ∪ (𝐵 ∖ 𝑉))⟶(Base‘(Scalar‘𝑊))) |
| 40 | | undif 4482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑉 ⊆ 𝐵 ↔ (𝑉 ∪ (𝐵 ∖ 𝑉)) = 𝐵) |
| 41 | 14, 40 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → (𝑉 ∪ (𝐵 ∖ 𝑉)) = 𝐵) |
| 42 | 41 | feq2d 6722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → ((𝑎 ∪ 𝑏):(𝑉 ∪ (𝐵 ∖ 𝑉))⟶(Base‘(Scalar‘𝑊)) ↔ (𝑎 ∪ 𝑏):𝐵⟶(Base‘(Scalar‘𝑊)))) |
| 43 | 39, 42 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → (𝑎 ∪ 𝑏):𝐵⟶(Base‘(Scalar‘𝑊))) |
| 44 | 43 | ffund 6740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → Fun (𝑎 ∪ 𝑏)) |
| 45 | 44 | fsuppunbi 9429 |
. . . . . . . . . . . . . . . . . . . 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 713 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) → (𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊))) |
| 47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊))) |
| 48 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 49 | | lmodcmn 20908 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd) |
| 50 | 22, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 ∈ LVec → 𝑊 ∈ CMnd) |
| 51 | 50 | ad9antr 742 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑊 ∈ CMnd) |
| 52 | 11 | ad7antr 738 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝐵 ∈ 𝐽) |
| 53 | 23 | ad8antr 740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝑊 ∈ LMod) |
| 54 | | elmapfn 8905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 ∈
((Base‘(Scalar‘𝑊)) ↑m 𝑉) → 𝑎 Fn 𝑉) |
| 55 | 54 | ad6antlr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑎 Fn 𝑉) |
| 56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → 𝑎 Fn 𝑉) |
| 57 | | elmapfn 8905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑏 ∈
((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉)) → 𝑏 Fn (𝐵 ∖ 𝑉)) |
| 58 | 57 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑏 Fn (𝐵 ∖ 𝑉)) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → 𝑢 ∈ 𝑉) |
| 62 | | fvun1 7000 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 Fn 𝑉 ∧ 𝑏 Fn (𝐵 ∖ 𝑉) ∧ ((𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅ ∧ 𝑢 ∈ 𝑉)) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑎‘𝑢)) |
| 63 | 56, 59, 60, 61, 62 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑎‘𝑢)) |
| 64 | 63 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ 𝑉) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑎‘𝑢)) |
| 65 | 20 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ 𝑉) → 𝑎:𝑉⟶(Base‘(Scalar‘𝑊))) |
| 66 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ 𝑉) → 𝑢 ∈ 𝑉) |
| 67 | 65, 66 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ 𝑉) → (𝑎‘𝑢) ∈ (Base‘(Scalar‘𝑊))) |
| 68 | 64, 67 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ 𝑉) → ((𝑎 ∪ 𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊))) |
| 69 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → 𝑎 Fn 𝑉) |
| 70 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → 𝑢 ∈ (𝐵 ∖ 𝑉)) |
| 73 | | fvun2 7001 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 Fn 𝑉 ∧ 𝑏 Fn (𝐵 ∖ 𝑉) ∧ ((𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅ ∧ 𝑢 ∈ (𝐵 ∖ 𝑉))) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑏‘𝑢)) |
| 74 | 69, 70, 71, 72, 73 | syl112anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑏‘𝑢)) |
| 75 | 74 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → ((𝑎 ∪ 𝑏)‘𝑢) = (𝑏‘𝑢)) |
| 76 | 36 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → 𝑏:(𝐵 ∖ 𝑉)⟶(Base‘(Scalar‘𝑊))) |
| 77 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → 𝑢 ∈ (𝐵 ∖ 𝑉)) |
| 78 | 76, 77 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → (𝑏‘𝑢) ∈ (Base‘(Scalar‘𝑊))) |
| 79 | 75, 78 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → ((𝑎 ∪ 𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊))) |
| 80 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ 𝐵) |
| 81 | 40 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑉 ⊆ 𝐵 → (𝑉 ∪ (𝐵 ∖ 𝑉)) = 𝐵) |
| 82 | 81 | ad8antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑉 ∪ (𝐵 ∖ 𝑉)) = 𝐵) |
| 83 | 82 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝐵 = (𝑉 ∪ (𝐵 ∖ 𝑉))) |
| 84 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝐵 = (𝑉 ∪ (𝐵 ∖ 𝑉))) |
| 85 | 80, 84 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ (𝑉 ∪ (𝐵 ∖ 𝑉))) |
| 86 | | elun 4153 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈ (𝑉 ∪ (𝐵 ∖ 𝑉)) ↔ (𝑢 ∈ 𝑉 ∨ 𝑢 ∈ (𝐵 ∖ 𝑉))) |
| 87 | 85, 86 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → (𝑢 ∈ 𝑉 ∨ 𝑢 ∈ (𝐵 ∖ 𝑉))) |
| 88 | 68, 79, 87 | mpjaodan 961 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → ((𝑎 ∪ 𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊))) |
| 89 | 27 | ad8antr 740 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝐵 ⊆ (Base‘𝑊)) |
| 90 | 89, 80 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ (Base‘𝑊)) |
| 91 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 92 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
| 93 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 94 | 24, 91, 92, 93 | lmodvscl 20876 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ LMod ∧ ((𝑎 ∪ 𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑢 ∈ (Base‘𝑊)) → (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢) ∈ (Base‘𝑊)) |
| 95 | 53, 88, 90, 94 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝐵) → (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢) ∈ (Base‘𝑊)) |
| 96 | | simp-9l 793 |
. . . . . . . . . . . . . . . . . . . . . 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 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (Scalar‘𝑊) = (Scalar‘𝑊)) |
| 99 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
| 100 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑎 ∪ 𝑏):𝐵⟶(Base‘(Scalar‘𝑊))) |
| 101 | 100 | feqmptd 6977 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑎 ∪ 𝑏) = (𝑢 ∈ 𝐵 ↦ ((𝑎 ∪ 𝑏)‘𝑢))) |
| 102 | 101, 47 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . . . . . 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 20925 |
. . . . . . . . . . . . . . . . . . . 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 19947 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = ((𝑊 Σg (𝑢 ∈ 𝑉 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)))(+g‘𝑊)(𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))))) |
| 106 | 63 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢) = ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)) |
| 107 | 106 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑢 ∈ 𝑉 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢))) |
| 108 | 107 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ 𝑉 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)))) |
| 109 | 74 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵 ∖ 𝑉)) → (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢) = ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢)) |
| 110 | 109 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢))) |
| 111 | 110 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢)))) |
| 112 | 108, 111 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . 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 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) |
| 114 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = 𝑣 → (𝑏‘𝑢) = (𝑏‘𝑣)) |
| 115 | 114, 3 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = 𝑣 → ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢) = ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)) |
| 116 | 115 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)) |
| 117 | 116 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 Σg
(𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣))) |
| 118 | 113, 117 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢)))) |
| 119 | 7, 118 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑥(+g‘𝑊)((invg‘𝑊)‘𝑥)) = ((𝑊 Σg (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)))(+g‘𝑊)(𝑊 Σg (𝑢 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑢)( ·𝑠
‘𝑊)𝑢))))) |
| 120 | | lmodgrp 20865 |
. . . . . . . . . . . . . . . . . . . . . 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 3994 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝑉 ⊆ (Base‘𝑊)) |
| 123 | 24, 30 | lspssv 20981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ (Base‘𝑊)) → (𝑁‘𝑉) ⊆ (Base‘𝑊)) |
| 124 | 23, 122, 123 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝑁‘𝑉) ⊆ (Base‘𝑊)) |
| 125 | 124 | ad7antr 738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑁‘𝑉) ⊆ (Base‘𝑊)) |
| 126 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) |
| 127 | 126 | elin2d 4205 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → 𝑥 ∈ (𝑁‘𝑉)) |
| 128 | 127 | ad6antr 736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 ∈ (𝑁‘𝑉)) |
| 129 | 125, 128 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 ∈ (Base‘𝑊)) |
| 130 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(invg‘𝑊) = (invg‘𝑊) |
| 131 | 24, 48, 29, 130 | grprinv 19008 |
. . . . . . . . . . . . . . . . . . . . 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 2783 |
. . . . . . . . . . . . . . . . . . 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 2777 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) |
| 135 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (𝑐 finSupp
(0g‘(Scalar‘𝑊)) ↔ (𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊)))) |
| 136 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (𝑐‘𝑢) = ((𝑎 ∪ 𝑏)‘𝑢)) |
| 137 | 136 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 = (𝑎 ∪ 𝑏) → ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢) = (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)) |
| 138 | 137 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) |
| 139 | 138 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢)))) |
| 140 | 139 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = (𝑎 ∪ 𝑏) → ((𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ↔ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 )) |
| 141 | 135, 140 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = (𝑎 ∪ 𝑏) → ((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) ↔ ((𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ))) |
| 142 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))}) ↔ (𝑎 ∪ 𝑏) = (𝐵 ×
{(0g‘(Scalar‘𝑊))}))) |
| 143 | 141, 142 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = (𝑎 ∪ 𝑏) → (((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))})) ↔ (((𝑎 ∪ 𝑏) finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ (((𝑎 ∪ 𝑏)‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → (𝑎 ∪ 𝑏) = (𝐵 ×
{(0g‘(Scalar‘𝑊))})))) |
| 144 | 25 | lbslinds 21853 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐽 ⊆ (LIndS‘𝑊) |
| 145 | 144, 11 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 𝐵 ∈ (LIndS‘𝑊)) |
| 146 | 24, 93, 91, 92, 29, 99 | islinds5 33395 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ LMod ∧ 𝐵 ⊆ (Base‘𝑊)) → (𝐵 ∈ (LIndS‘𝑊) ↔ ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝐵)((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))})))) |
| 147 | 146 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LMod ∧ 𝐵 ⊆ (Base‘𝑊)) ∧ 𝐵 ∈ (LIndS‘𝑊)) → ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝐵)((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))}))) |
| 148 | 23, 27, 145, 147 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝐵)((𝑐 finSupp
(0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢 ∈ 𝐵 ↦ ((𝑐‘𝑢)( ·𝑠
‘𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 ×
{(0g‘(Scalar‘𝑊))}))) |
| 149 | 148 | ad7antr 738 |
. . . . . . . . . . . . . . . . . . 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 6921 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (Base‘(Scalar‘𝑊)) ∈ V) |
| 151 | 150, 52 | elmapd 8880 |
. . . . . . . . . . . . . . . . . . . 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 257 |
. . . . . . . . . . . . . . . . . . 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 3623 |
. . . . . . . . . . . . . . . . . 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 699 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑎 ∪ 𝑏) = (𝐵 ×
{(0g‘(Scalar‘𝑊))})) |
| 155 | 154 | reseq1d 5996 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((𝑎 ∪ 𝑏) ↾ 𝑉) = ((𝐵 ×
{(0g‘(Scalar‘𝑊))}) ↾ 𝑉)) |
| 156 | | fnunres1 6680 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 Fn 𝑉 ∧ 𝑏 Fn (𝐵 ∖ 𝑉) ∧ (𝑉 ∩ (𝐵 ∖ 𝑉)) = ∅) → ((𝑎 ∪ 𝑏) ↾ 𝑉) = 𝑎) |
| 157 | 55, 58, 104, 156 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ((𝑎 ∪ 𝑏) ↾ 𝑉) = 𝑎) |
| 158 | | xpssres 6036 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ⊆ 𝐵 → ((𝐵 ×
{(0g‘(Scalar‘𝑊))}) ↾ 𝑉) = (𝑉 ×
{(0g‘(Scalar‘𝑊))})) |
| 159 | 158 | ad8antlr 741 |
. . . . . . . . . . . . . . . 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 2785 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑎 = (𝑉 ×
{(0g‘(Scalar‘𝑊))})) |
| 161 | 160 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → 𝑎 = (𝑉 ×
{(0g‘(Scalar‘𝑊))})) |
| 162 | 161 | fveq1d 6908 |
. . . . . . . . . . . . 13
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → (𝑎‘𝑢) = ((𝑉 ×
{(0g‘(Scalar‘𝑊))})‘𝑢)) |
| 163 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢
(0g‘(Scalar‘𝑊)) ∈ V |
| 164 | 163 | fvconst2 7224 |
. . . . . . . . . . . . . 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 2777 |
. . . . . . . . . . . 12
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → (𝑎‘𝑢) = (0g‘(Scalar‘𝑊))) |
| 167 | 166 | oveq1d 7446 |
. . . . . . . . . . 11
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢) = ((0g‘(Scalar‘𝑊))(
·𝑠 ‘𝑊)𝑢)) |
| 168 | 122 | ad8antr 740 |
. . . . . . . . . . . . 13
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → 𝑉 ⊆ (Base‘𝑊)) |
| 169 | 168, 61 | sseldd 3984 |
. . . . . . . . . . . 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 20893 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑢 ∈ (Base‘𝑊)) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑢) = 0 ) |
| 171 | 97, 169, 170 | syl2an2r 685 |
. . . . . . . . . . 11
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑢) = 0 ) |
| 172 | 167, 171 | eqtrd 2777 |
. . . . . . . . . 10
⊢
(((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑢 ∈ 𝑉) → ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢) = 0 ) |
| 173 | 172 | mpteq2dva 5242 |
. . . . . . . . 9
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢)) = (𝑢 ∈ 𝑉 ↦ 0 )) |
| 174 | 173 | oveq2d 7447 |
. . . . . . . 8
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ 𝑉 ↦ ((𝑎‘𝑢)( ·𝑠
‘𝑊)𝑢))) = (𝑊 Σg (𝑢 ∈ 𝑉 ↦ 0 ))) |
| 175 | | cmnmnd 19815 |
. . . . . . . . . 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 6945 |
. . . . . . . . 9
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑉 ∈ V) |
| 178 | 29 | gsumz 18849 |
. . . . . . . . 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 2781 |
. . . . . . 7
⊢
((((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ 𝑏 finSupp
(0g‘(Scalar‘𝑊))) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 = 0 ) |
| 181 | 180 | anasss 466 |
. . . . . 6
⊢
(((((((((𝑊 ∈
LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))) ∧ (𝑏 finSupp
(0g‘(Scalar‘𝑊)) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣))))) → 𝑥 = 0 ) |
| 182 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
| 183 | 24, 182, 30 | lspcl 20974 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝐵 ∖ 𝑉) ⊆ (Base‘𝑊)) → (𝑁‘(𝐵 ∖ 𝑉)) ∈ (LSubSp‘𝑊)) |
| 184 | 23, 28, 183 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝑁‘(𝐵 ∖ 𝑉)) ∈ (LSubSp‘𝑊)) |
| 185 | 184 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → (𝑁‘(𝐵 ∖ 𝑉)) ∈ (LSubSp‘𝑊)) |
| 186 | 182 | lsssubg 20955 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘(𝐵 ∖ 𝑉)) ∈ (LSubSp‘𝑊)) → (𝑁‘(𝐵 ∖ 𝑉)) ∈ (SubGrp‘𝑊)) |
| 187 | 23, 185, 186 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → (𝑁‘(𝐵 ∖ 𝑉)) ∈ (SubGrp‘𝑊)) |
| 188 | 126 | elin1d 4204 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → 𝑥 ∈ (𝑁‘(𝐵 ∖ 𝑉))) |
| 189 | 130 | subginvcl 19153 |
. . . . . . . . 9
⊢ (((𝑁‘(𝐵 ∖ 𝑉)) ∈ (SubGrp‘𝑊) ∧ 𝑥 ∈ (𝑁‘(𝐵 ∖ 𝑉))) → ((invg‘𝑊)‘𝑥) ∈ (𝑁‘(𝐵 ∖ 𝑉))) |
| 190 | 187, 188,
189 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → ((invg‘𝑊)‘𝑥) ∈ (𝑁‘(𝐵 ∖ 𝑉))) |
| 191 | 30, 24, 93, 91, 99, 92, 23, 28 | ellspds 33396 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (((invg‘𝑊)‘𝑥) ∈ (𝑁‘(𝐵 ∖ 𝑉)) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))(𝑏 finSupp
(0g‘(Scalar‘𝑊)) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣)))))) |
| 192 | 191 | biimpa 476 |
. . . . . . . 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 730 |
. . . . . 6
⊢
(((((((𝑊 ∈ LVec
∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → ∃𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑m (𝐵 ∖ 𝑉))(𝑏 finSupp
(0g‘(Scalar‘𝑊)) ∧ ((invg‘𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵 ∖ 𝑉) ↦ ((𝑏‘𝑣)( ·𝑠
‘𝑊)𝑣))))) |
| 195 | 181, 194 | r19.29a 3162 |
. . . . 5
⊢
(((((((𝑊 ∈ LVec
∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))) → 𝑥 = 0 ) |
| 196 | 195 | anasss 466 |
. . . 4
⊢
((((((𝑊 ∈ LVec
∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)) ∧ (𝑎 finSupp
(0g‘(Scalar‘𝑊)) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣))))) → 𝑥 = 0 ) |
| 197 | 30, 24, 93, 91, 99, 92, 23, 122 | ellspds 33396 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → (𝑥 ∈ (𝑁‘𝑉) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑m 𝑉)(𝑎 finSupp
(0g‘(Scalar‘𝑊)) ∧ 𝑥 = (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣)( ·𝑠
‘𝑊)𝑣)))))) |
| 198 | 197 | biimpa 476 |
. . . . 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 3162 |
. . 3
⊢ ((((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) → 𝑥 = 0 ) |
| 201 | 29, 24, 30 | 0ellsp 33397 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ (Base‘𝑊)) → 0 ∈ (𝑁‘𝑉)) |
| 202 | 23, 122, 201 | syl2anc 584 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 0 ∈ (𝑁‘𝑉)) |
| 203 | 32, 202 | elind 4200 |
. . 3
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → 0 ∈ ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉))) |
| 204 | 200, 203 | eqsnd 4830 |
. 2
⊢ (((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽) ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 }) |
| 205 | 204 | 3impa 1110 |
1
⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 }) |