Metamath Proof Explorer

Theorem lbsdiflsp0

Description: The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun . (Contributed by Thierry Arnoux, 17-May-2023)

Ref Expression
Hypotheses lbsdiflsp0.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
lbsdiflsp0.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lbsdiflsp0.1 ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion lbsdiflsp0 ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵 ) → ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) = { 0 } )

Proof

Step Hyp Ref Expression
1 lbsdiflsp0.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
2 lbsdiflsp0.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lbsdiflsp0.1 ⊢ 0 = ( 0g ‘ 𝑊 )
4 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) )
5 fveq2 ⊢ ( 𝑢 = 𝑣 → ( 𝑎 ‘ 𝑢 ) = ( 𝑎 ‘ 𝑣 ) )
6 id ⊢ ( 𝑢 = 𝑣 → 𝑢 = 𝑣 )
7 5 6 oveq12d ⊢ ( 𝑢 = 𝑣 → ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) = ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) )
8 7 cbvmptv ⊢ ( 𝑢 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) )
9 8 oveq2i ⊢ ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) )
10 4 9 eqtr4di ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑥 = ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) )
11 simp-4r ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
12 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
13 simp-8l ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑊 ∈ LVec )
14 simplr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → 𝐵 ∈ 𝐽 )
15 14 ad6antr ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝐵 ∈ 𝐽 )
16 simpr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ⊆ 𝐵 )
17 16 ad6antr ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑉 ⊆ 𝐵 )
18 simp-5r ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) )
19 fvexd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ V )
20 14 16 ssexd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ∈ V )
21 19 20 elmapd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ↔ 𝑎 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
22 21 biimpa ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) → 𝑎 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
23 13 15 17 18 22 syl1111anc ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑎 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
24 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) )
25 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
26 25 ad2antrr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → 𝑊 ∈ LMod )
27 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
28 27 1 lbsss ⊢ ( 𝐵 ∈ 𝐽 → 𝐵 ⊆ ( Base ‘ 𝑊 ) )
29 28 ad2antlr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → 𝐵 ⊆ ( Base ‘ 𝑊 ) )
30 29 ssdifssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) )
31 3 27 2 0ellsp ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐵 ∖ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) ) → 0 ∈ ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) )
32 26 30 31 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → 0 ∈ ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) )
33 32 elfvexd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑉 ) ∈ V )
34 19 33 elmapd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ↔ 𝑏 : ( 𝐵 ∖ 𝑉 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
35 34 biimpa ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) → 𝑏 : ( 𝐵 ∖ 𝑉 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
36 13 15 17 24 35 syl1111anc ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑏 : ( 𝐵 ∖ 𝑉 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
37 disjdif ⊢ ( 𝑉 ∩ ( 𝐵 ∖ 𝑉 ) ) = ∅
38 37 a1i ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑉 ∩ ( 𝐵 ∖ 𝑉 ) ) = ∅ )
39 23 36 38 fun2d ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑎 ∪ 𝑏 ) : ( 𝑉 ∪ ( 𝐵 ∖ 𝑉 ) ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
40 undif ⊢ ( 𝑉 ⊆ 𝐵 ↔ ( 𝑉 ∪ ( 𝐵 ∖ 𝑉 ) ) = 𝐵 )
41 17 40 sylib ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑉 ∪ ( 𝐵 ∖ 𝑉 ) ) = 𝐵 )
42 41 feq2d ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝑎 ∪ 𝑏 ) : ( 𝑉 ∪ ( 𝐵 ∖ 𝑉 ) ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝑎 ∪ 𝑏 ) : 𝐵 ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
43 39 42 mpbid ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑎 ∪ 𝑏 ) : 𝐵 ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
44 43 ffund ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → Fun ( 𝑎 ∪ 𝑏 ) )
45 44 fsuppunbi ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝑎 ∪ 𝑏 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
46 11 12 45 mpbir2and ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑎 ∪ 𝑏 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
47 46 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑎 ∪ 𝑏 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
48 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
49 lmodcmn ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ CMnd )
50 25 49 syl ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ CMnd )
51 50 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑊 ∈ CMnd )
52 14 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝐵 ∈ 𝐽 )
53 26 ad8antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) → 𝑊 ∈ LMod )
54 elmapfn ⊢ ( 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) → 𝑎 Fn 𝑉 )
55 54 ad6antlr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑎 Fn 𝑉 )
56 55 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → 𝑎 Fn 𝑉 )
57 elmapfn ⊢ ( 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) → 𝑏 Fn ( 𝐵 ∖ 𝑉 ) )
58 57 ad3antlr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑏 Fn ( 𝐵 ∖ 𝑉 ) )
59 58 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → 𝑏 Fn ( 𝐵 ∖ 𝑉 ) )
60 37 a1i ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → ( 𝑉 ∩ ( 𝐵 ∖ 𝑉 ) ) = ∅ )
61 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → 𝑢 ∈ 𝑉 )
62 fvun1 ⊢ ( ( 𝑎 Fn 𝑉 ∧ 𝑏 Fn ( 𝐵 ∖ 𝑉 ) ∧ ( ( 𝑉 ∩ ( 𝐵 ∖ 𝑉 ) ) = ∅ ∧ 𝑢 ∈ 𝑉 ) ) → ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) = ( 𝑎 ‘ 𝑢 ) )
63 56 59 60 61 62 syl112anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) = ( 𝑎 ‘ 𝑢 ) )
64 63 adantlr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝑉 ) → ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) = ( 𝑎 ‘ 𝑢 ) )
65 23 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝑉 ) → 𝑎 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
66 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝑉 ) → 𝑢 ∈ 𝑉 )
67 65 66 ffvelrnd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝑉 ) → ( 𝑎 ‘ 𝑢 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
68 64 67 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝑉 ) → ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
69 55 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → 𝑎 Fn 𝑉 )
70 58 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → 𝑏 Fn ( 𝐵 ∖ 𝑉 ) )
71 37 a1i ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → ( 𝑉 ∩ ( 𝐵 ∖ 𝑉 ) ) = ∅ )
72 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) )
73 fvun2 ⊢ ( ( 𝑎 Fn 𝑉 ∧ 𝑏 Fn ( 𝐵 ∖ 𝑉 ) ∧ ( ( 𝑉 ∩ ( 𝐵 ∖ 𝑉 ) ) = ∅ ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) ) → ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) = ( 𝑏 ‘ 𝑢 ) )
74 69 70 71 72 73 syl112anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) = ( 𝑏 ‘ 𝑢 ) )
75 74 adantlr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) = ( 𝑏 ‘ 𝑢 ) )
76 36 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → 𝑏 : ( 𝐵 ∖ 𝑉 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
77 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) )
78 76 77 ffvelrnd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → ( 𝑏 ‘ 𝑢 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
79 75 78 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
80 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
81 40 biimpi ⊢ ( 𝑉 ⊆ 𝐵 → ( 𝑉 ∪ ( 𝐵 ∖ 𝑉 ) ) = 𝐵 )
82 81 ad8antlr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑉 ∪ ( 𝐵 ∖ 𝑉 ) ) = 𝐵 )
83 82 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝐵 = ( 𝑉 ∪ ( 𝐵 ∖ 𝑉 ) ) )
84 83 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) → 𝐵 = ( 𝑉 ∪ ( 𝐵 ∖ 𝑉 ) ) )
85 80 84 eleqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ ( 𝑉 ∪ ( 𝐵 ∖ 𝑉 ) ) )
86 elun ⊢ ( 𝑢 ∈ ( 𝑉 ∪ ( 𝐵 ∖ 𝑉 ) ) ↔ ( 𝑢 ∈ 𝑉 ∨ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) )
87 85 86 sylib ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑢 ∈ 𝑉 ∨ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) )
88 68 79 87 mpjaodan ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
89 29 ad8antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) → 𝐵 ⊆ ( Base ‘ 𝑊 ) )
90 89 80 sseldd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ ( Base ‘ 𝑊 ) )
91 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
92 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
93 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
94 27 91 92 93 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑢 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ∈ ( Base ‘ 𝑊 ) )
95 53 88 90 94 syl3anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ∈ ( Base ‘ 𝑊 ) )
96 simp-9l ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑊 ∈ LVec )
97 96 25 syl ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑊 ∈ LMod )
98 eqidd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) )
99 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
100 43 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑎 ∪ 𝑏 ) : 𝐵 ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
101 100 feqmptd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑎 ∪ 𝑏 ) = ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ) )
102 101 47 eqbrtrrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
103 52 97 98 27 88 90 3 99 92 102 mptscmfsupp0 ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑢 ∈ 𝐵 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) finSupp 0 )
104 37 a1i ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑉 ∩ ( 𝐵 ∖ 𝑉 ) ) = ∅ )
105 27 3 48 51 52 95 103 104 83 gsumsplit2 ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = ( ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) ( +g ‘ 𝑊 ) ( 𝑊 Σg ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) ) )
106 63 oveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) = ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) )
107 106 mpteq2dva ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑢 ∈ 𝑉 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) )
108 107 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) )
109 74 oveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ) → ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) = ( ( 𝑏 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) )
110 109 mpteq2dva ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) = ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) )
111 110 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑊 Σg ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = ( 𝑊 Σg ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) )
112 108 111 oveq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) ( +g ‘ 𝑊 ) ( 𝑊 Σg ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) ) = ( ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) ( +g ‘ 𝑊 ) ( 𝑊 Σg ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) ) )
113 simpr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) )
114 fveq2 ⊢ ( 𝑢 = 𝑣 → ( 𝑏 ‘ 𝑢 ) = ( 𝑏 ‘ 𝑣 ) )
115 114 6 oveq12d ⊢ ( 𝑢 = 𝑣 → ( ( 𝑏 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) = ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) )
116 115 cbvmptv ⊢ ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) = ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) )
117 116 oveq2i ⊢ ( 𝑊 Σg ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) )
118 113 117 eqtr4di ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) )
119 10 118 oveq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑥 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ) = ( ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) ( +g ‘ 𝑊 ) ( 𝑊 Σg ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) ) )
120 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
121 96 25 120 3syl ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑊 ∈ Grp )
122 16 29 sstrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ⊆ ( Base ‘ 𝑊 ) )
123 27 2 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) )
124 26 122 123 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑁 ‘ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) )
125 124 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑁 ‘ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) )
126 simpr ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) → 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) )
127 126 elin2d ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) → 𝑥 ∈ ( 𝑁 ‘ 𝑉 ) )
128 127 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑥 ∈ ( 𝑁 ‘ 𝑉 ) )
129 125 128 sseldd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
130 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
131 27 48 3 130 grprinv ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ) = 0 )
132 121 129 131 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑥 ( +g ‘ 𝑊 ) ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ) = 0 )
133 112 119 132 3eqtr2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) ( +g ‘ 𝑊 ) ( 𝑊 Σg ( 𝑢 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) ) = 0 )
134 105 133 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = 0 )
135 breq1 ⊢ ( 𝑐 = ( 𝑎 ∪ 𝑏 ) → ( 𝑐 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝑎 ∪ 𝑏 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
136 fveq1 ⊢ ( 𝑐 = ( 𝑎 ∪ 𝑏 ) → ( 𝑐 ‘ 𝑢 ) = ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) )
137 136 oveq1d ⊢ ( 𝑐 = ( 𝑎 ∪ 𝑏 ) → ( ( 𝑐 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) = ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) )
138 137 mpteq2dv ⊢ ( 𝑐 = ( 𝑎 ∪ 𝑏 ) → ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑐 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) = ( 𝑢 ∈ 𝐵 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) )
139 138 oveq2d ⊢ ( 𝑐 = ( 𝑎 ∪ 𝑏 ) → ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑐 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) )
140 139 eqeq1d ⊢ ( 𝑐 = ( 𝑎 ∪ 𝑏 ) → ( ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑐 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = 0 ↔ ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = 0 ) )
141 135 140 anbi12d ⊢ ( 𝑐 = ( 𝑎 ∪ 𝑏 ) → ( ( 𝑐 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑐 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = 0 ) ↔ ( ( 𝑎 ∪ 𝑏 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = 0 ) ) )
142 eqeq1 ⊢ ( 𝑐 = ( 𝑎 ∪ 𝑏 ) → ( 𝑐 = ( 𝐵 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ↔ ( 𝑎 ∪ 𝑏 ) = ( 𝐵 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
143 141 142 imbi12d ⊢ ( 𝑐 = ( 𝑎 ∪ 𝑏 ) → ( ( ( 𝑐 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑐 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = 0 ) → 𝑐 = ( 𝐵 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ↔ ( ( ( 𝑎 ∪ 𝑏 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( ( 𝑎 ∪ 𝑏 ) ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = 0 ) → ( 𝑎 ∪ 𝑏 ) = ( 𝐵 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) )
144 1 lbslinds ⊢ 𝐽 ⊆ ( LIndS ‘ 𝑊 )
145 144 14 sselid ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → 𝐵 ∈ ( LIndS ‘ 𝑊 ) )
146 27 93 91 92 3 99 islinds5 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ ( Base ‘ 𝑊 ) ) → ( 𝐵 ∈ ( LIndS ‘ 𝑊 ) ↔ ∀ 𝑐 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝐵 ) ( ( 𝑐 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑐 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = 0 ) → 𝑐 = ( 𝐵 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) )
147 146 biimpa ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐵 ⊆ ( Base ‘ 𝑊 ) ) ∧ 𝐵 ∈ ( LIndS ‘ 𝑊 ) ) → ∀ 𝑐 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝐵 ) ( ( 𝑐 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑐 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = 0 ) → 𝑐 = ( 𝐵 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
148 26 29 145 147 syl21anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ∀ 𝑐 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝐵 ) ( ( 𝑐 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑊 Σg ( 𝑢 ∈ 𝐵 ↦ ( ( 𝑐 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = 0 ) → 𝑐 = ( 𝐵 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
149 148 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ 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 ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∈ V )
151 150 52 elmapd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ 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 ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑎 ∪ 𝑏 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝐵 ) )
153 143 149 152 rspcdva ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ 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 ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑎 ∪ 𝑏 ) = ( 𝐵 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
155 154 reseq1d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( ( 𝑎 ∪ 𝑏 ) ↾ 𝑉 ) = ( ( 𝐵 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ↾ 𝑉 ) )
156 fnunres1 ⊢ ( ( 𝑎 Fn 𝑉 ∧ 𝑏 Fn ( 𝐵 ∖ 𝑉 ) ∧ ( 𝑉 ∩ ( 𝐵 ∖ 𝑉 ) ) = ∅ ) → ( ( 𝑎 ∪ 𝑏 ) ↾ 𝑉 ) = 𝑎 )
157 55 58 104 156 syl3anc ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( ( 𝑎 ∪ 𝑏 ) ↾ 𝑉 ) = 𝑎 )
158 xpssres ⊢ ( 𝑉 ⊆ 𝐵 → ( ( 𝐵 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ↾ 𝑉 ) = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
159 158 ad8antlr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ 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 ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑎 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
161 160 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → 𝑎 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
162 161 fveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → ( 𝑎 ‘ 𝑢 ) = ( ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ‘ 𝑢 ) )
163 fvex ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ V
164 163 fvconst2 ⊢ ( 𝑢 ∈ 𝑉 → ( ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ‘ 𝑢 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
165 61 164 syl ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → ( ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ‘ 𝑢 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
166 162 165 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → ( 𝑎 ‘ 𝑢 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
167 166 oveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) )
168 122 ad8antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → 𝑉 ⊆ ( Base ‘ 𝑊 ) )
169 168 61 sseldd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → 𝑢 ∈ ( Base ‘ 𝑊 ) )
170 27 91 92 99 3 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑢 ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) = 0 )
171 97 169 170 syl2an2r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) = 0 )
172 167 171 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑢 ∈ 𝑉 ) → ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) = 0 )
173 172 mpteq2dva ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑢 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) = ( 𝑢 ∈ 𝑉 ↦ 0 ) )
174 173 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑢 ) ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ) ) = ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ 0 ) ) )
175 cmnmnd ⊢ ( 𝑊 ∈ CMnd → 𝑊 ∈ Mnd )
176 51 175 syl ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑊 ∈ Mnd )
177 128 elfvexd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑉 ∈ V )
178 3 gsumz ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑉 ∈ V ) → ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ 0 ) ) = 0 )
179 176 177 178 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ( 𝑊 Σg ( 𝑢 ∈ 𝑉 ↦ 0 ) ) = 0 )
180 10 174 179 3eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑥 = 0 )
181 180 anasss ⊢ ( ( ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ) ∧ ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ) → 𝑥 = 0 )
182 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
183 27 182 2 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐵 ∖ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∈ ( LSubSp ‘ 𝑊 ) )
184 26 30 183 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∈ ( LSubSp ‘ 𝑊 ) )
185 184 adantr ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) → ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∈ ( LSubSp ‘ 𝑊 ) )
186 182 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∈ ( SubGrp ‘ 𝑊 ) )
187 26 185 186 syl2an2r ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) → ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∈ ( SubGrp ‘ 𝑊 ) )
188 126 elin1d ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) → 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) )
189 130 subginvcl ⊢ ( ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ) → ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) )
190 187 188 189 syl2anc ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) → ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) )
191 2 27 93 91 99 92 26 30 ellspds ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ( ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ↔ ∃ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ) )
192 191 biimpa ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ) → ∃ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) )
193 190 192 syldan ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) → ∃ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) )
194 193 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → ∃ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m ( 𝐵 ∖ 𝑉 ) ) ( 𝑏 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 Σg ( 𝑣 ∈ ( 𝐵 ∖ 𝑉 ) ↦ ( ( 𝑏 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) )
195 181 194 r19.29a ⊢ ( ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) → 𝑥 = 0 )
196 195 anasss ⊢ ( ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ) ∧ ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ) → 𝑥 = 0 )
197 2 27 93 91 99 92 26 122 ellspds ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑁 ‘ 𝑉 ) ↔ ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) ) )
198 197 biimpa ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( 𝑁 ‘ 𝑉 ) ) → ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) )
199 127 198 syldan ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) → ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↑m 𝑉 ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 = ( 𝑊 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑊 ) 𝑣 ) ) ) ) )
200 196 199 r19.29a ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) ) → 𝑥 = 0 )
201 3 27 2 0ellsp ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ⊆ ( Base ‘ 𝑊 ) ) → 0 ∈ ( 𝑁 ‘ 𝑉 ) )
202 26 122 201 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → 0 ∈ ( 𝑁 ‘ 𝑉 ) )
203 32 202 elind ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → 0 ∈ ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) )
204 200 203 eqsnd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑉 ⊆ 𝐵 ) → ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) = { 0 } )
205 204 3impa ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵 ) → ( ( 𝑁 ‘ ( 𝐵 ∖ 𝑉 ) ) ∩ ( 𝑁 ‘ 𝑉 ) ) = { 0 } )