Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lbsdiflsp0 Structured version   Visualization version   GIF version

Theorem lbsdiflsp0 30651
Description: The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 30650. (Contributed by Thierry Arnoux, 17-May-2023.)
Hypotheses
Ref Expression
lbsdiflsp0.j 𝐽 = (LBasis‘𝑊)
lbsdiflsp0.n 𝑁 = (LSpan‘𝑊)
lbsdiflsp0.1 0 = (0g𝑊)
Assertion
Ref Expression
lbsdiflsp0 ((𝑊 ∈ LVec ∧ 𝐵𝐽𝑉𝐵) → ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉)) = { 0 })

Proof of Theorem lbsdiflsp0
Dummy variables 𝑎 𝑏 𝑐 𝑢 𝑣 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp-4r 771 . . . . . . . . 9 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣))))
2 fveq2 6493 . . . . . . . . . . . 12 (𝑢 = 𝑣 → (𝑎𝑢) = (𝑎𝑣))
3 id 22 . . . . . . . . . . . 12 (𝑢 = 𝑣𝑢 = 𝑣)
42, 3oveq12d 6988 . . . . . . . . . . 11 (𝑢 = 𝑣 → ((𝑎𝑢)( ·𝑠𝑊)𝑢) = ((𝑎𝑣)( ·𝑠𝑊)𝑣))
54cbvmptv 5022 . . . . . . . . . 10 (𝑢𝑉 ↦ ((𝑎𝑢)( ·𝑠𝑊)𝑢)) = (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣))
65oveq2i 6981 . . . . . . . . 9 (𝑊 Σg (𝑢𝑉 ↦ ((𝑎𝑢)( ·𝑠𝑊)𝑢))) = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))
71, 6syl6eqr 2826 . . . . . . . 8 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑥 = (𝑊 Σg (𝑢𝑉 ↦ ((𝑎𝑢)( ·𝑠𝑊)𝑢))))
8 simp-4r 771 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → 𝑎 finSupp (0g‘(Scalar‘𝑊)))
9 simpr 477 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → 𝑏 finSupp (0g‘(Scalar‘𝑊)))
10 simp-8l 778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → 𝑊 ∈ LVec)
11 simplr 756 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → 𝐵𝐽)
1211ad6antr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → 𝐵𝐽)
13 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → 𝑉𝐵)
1413ad6antr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → 𝑉𝐵)
15 simp-5r 773 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉))
16 fvexd 6508 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → (Base‘(Scalar‘𝑊)) ∈ V)
1711, 13ssexd 5078 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → 𝑉 ∈ V)
1816, 17elmapd 8214 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → (𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉) ↔ 𝑎:𝑉⟶(Base‘(Scalar‘𝑊))))
1918biimpa 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) → 𝑎:𝑉⟶(Base‘(Scalar‘𝑊)))
2010, 12, 14, 15, 19syl1111anc 827 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → 𝑎:𝑉⟶(Base‘(Scalar‘𝑊)))
21 simplr 756 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉)))
22 lveclmod 19594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
2322ad2antrr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → 𝑊 ∈ LMod)
24 eqid 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (Base‘𝑊) = (Base‘𝑊)
25 lbsdiflsp0.j . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝐽 = (LBasis‘𝑊)
2624, 25lbsss 19565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐵𝐽𝐵 ⊆ (Base‘𝑊))
2726ad2antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → 𝐵 ⊆ (Base‘𝑊))
2827ssdifssd 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → (𝐵𝑉) ⊆ (Base‘𝑊))
29 lbsdiflsp0.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 = (0g𝑊)
30 lbsdiflsp0.n . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑁 = (LSpan‘𝑊)
3129, 24, 300ellsp 30607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑊 ∈ LMod ∧ (𝐵𝑉) ⊆ (Base‘𝑊)) → 0 ∈ (𝑁‘(𝐵𝑉)))
3223, 28, 31syl2anc 576 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → 0 ∈ (𝑁‘(𝐵𝑉)))
3332elfvexd 6528 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → (𝐵𝑉) ∈ V)
3416, 33elmapd 8214 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → (𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉)) ↔ 𝑏:(𝐵𝑉)⟶(Base‘(Scalar‘𝑊))))
3534biimpa 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) → 𝑏:(𝐵𝑉)⟶(Base‘(Scalar‘𝑊)))
3610, 12, 14, 21, 35syl1111anc 827 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → 𝑏:(𝐵𝑉)⟶(Base‘(Scalar‘𝑊)))
37 disjdif 4298 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑉 ∩ (𝐵𝑉)) = ∅
3837a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → (𝑉 ∩ (𝐵𝑉)) = ∅)
3920, 36, 38fun2d 6365 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → (𝑎𝑏):(𝑉 ∪ (𝐵𝑉))⟶(Base‘(Scalar‘𝑊)))
40 undif 4307 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑉𝐵 ↔ (𝑉 ∪ (𝐵𝑉)) = 𝐵)
4114, 40sylib 210 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → (𝑉 ∪ (𝐵𝑉)) = 𝐵)
4241feq2d 6324 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → ((𝑎𝑏):(𝑉 ∪ (𝐵𝑉))⟶(Base‘(Scalar‘𝑊)) ↔ (𝑎𝑏):𝐵⟶(Base‘(Scalar‘𝑊))))
4339, 42mpbid 224 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → (𝑎𝑏):𝐵⟶(Base‘(Scalar‘𝑊)))
4443ffund 6342 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → Fun (𝑎𝑏))
4544fsuppunbi 8643 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → ((𝑎𝑏) finSupp (0g‘(Scalar‘𝑊)) ↔ (𝑎 finSupp (0g‘(Scalar‘𝑊)) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊)))))
468, 9, 45mpbir2and 700 . . . . . . . . . . . . . . . . . . 19 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) → (𝑎𝑏) finSupp (0g‘(Scalar‘𝑊)))
4746adantr 473 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑎𝑏) finSupp (0g‘(Scalar‘𝑊)))
48 eqid 2772 . . . . . . . . . . . . . . . . . . . 20 (+g𝑊) = (+g𝑊)
49 lmodcmn 19398 . . . . . . . . . . . . . . . . . . . . . 22 (𝑊 ∈ LMod → 𝑊 ∈ CMnd)
5022, 49syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑊 ∈ LVec → 𝑊 ∈ CMnd)
5150ad9antr 729 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑊 ∈ CMnd)
5211ad7antr 725 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝐵𝐽)
5323ad8antr 727 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) → 𝑊 ∈ LMod)
54 elmapfn 8223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉) → 𝑎 Fn 𝑉)
5554ad6antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑎 Fn 𝑉)
5655adantr 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → 𝑎 Fn 𝑉)
57 elmapfn 8223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉)) → 𝑏 Fn (𝐵𝑉))
5857ad3antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑏 Fn (𝐵𝑉))
5958adantr 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → 𝑏 Fn (𝐵𝑉))
6037a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → (𝑉 ∩ (𝐵𝑉)) = ∅)
61 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → 𝑢𝑉)
62 fvun1 6576 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 Fn 𝑉𝑏 Fn (𝐵𝑉) ∧ ((𝑉 ∩ (𝐵𝑉)) = ∅ ∧ 𝑢𝑉)) → ((𝑎𝑏)‘𝑢) = (𝑎𝑢))
6356, 59, 60, 61, 62syl112anc 1354 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → ((𝑎𝑏)‘𝑢) = (𝑎𝑢))
6463adantlr 702 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) ∧ 𝑢𝑉) → ((𝑎𝑏)‘𝑢) = (𝑎𝑢))
6520ad3antrrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) ∧ 𝑢𝑉) → 𝑎:𝑉⟶(Base‘(Scalar‘𝑊)))
66 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) ∧ 𝑢𝑉) → 𝑢𝑉)
6765, 66ffvelrnd 6671 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) ∧ 𝑢𝑉) → (𝑎𝑢) ∈ (Base‘(Scalar‘𝑊)))
6864, 67eqeltrd 2860 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) ∧ 𝑢𝑉) → ((𝑎𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊)))
6955adantr 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵𝑉)) → 𝑎 Fn 𝑉)
7058adantr 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵𝑉)) → 𝑏 Fn (𝐵𝑉))
7137a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵𝑉)) → (𝑉 ∩ (𝐵𝑉)) = ∅)
72 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵𝑉)) → 𝑢 ∈ (𝐵𝑉))
73 fvun2 6577 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 Fn 𝑉𝑏 Fn (𝐵𝑉) ∧ ((𝑉 ∩ (𝐵𝑉)) = ∅ ∧ 𝑢 ∈ (𝐵𝑉))) → ((𝑎𝑏)‘𝑢) = (𝑏𝑢))
7469, 70, 71, 72, 73syl112anc 1354 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵𝑉)) → ((𝑎𝑏)‘𝑢) = (𝑏𝑢))
7574adantlr 702 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) ∧ 𝑢 ∈ (𝐵𝑉)) → ((𝑎𝑏)‘𝑢) = (𝑏𝑢))
7636ad3antrrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) ∧ 𝑢 ∈ (𝐵𝑉)) → 𝑏:(𝐵𝑉)⟶(Base‘(Scalar‘𝑊)))
77 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) ∧ 𝑢 ∈ (𝐵𝑉)) → 𝑢 ∈ (𝐵𝑉))
7876, 77ffvelrnd 6671 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) ∧ 𝑢 ∈ (𝐵𝑉)) → (𝑏𝑢) ∈ (Base‘(Scalar‘𝑊)))
7975, 78eqeltrd 2860 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) ∧ 𝑢 ∈ (𝐵𝑉)) → ((𝑎𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊)))
80 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) → 𝑢𝐵)
8140biimpi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑉𝐵 → (𝑉 ∪ (𝐵𝑉)) = 𝐵)
8281ad8antlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑉 ∪ (𝐵𝑉)) = 𝐵)
8382eqcomd 2778 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝐵 = (𝑉 ∪ (𝐵𝑉)))
8483adantr 473 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) → 𝐵 = (𝑉 ∪ (𝐵𝑉)))
8580, 84eleqtrd 2862 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) → 𝑢 ∈ (𝑉 ∪ (𝐵𝑉)))
86 elun 4008 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ (𝑉 ∪ (𝐵𝑉)) ↔ (𝑢𝑉𝑢 ∈ (𝐵𝑉)))
8785, 86sylib 210 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) → (𝑢𝑉𝑢 ∈ (𝐵𝑉)))
8868, 79, 87mpjaodan 941 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) → ((𝑎𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊)))
8927ad8antr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) → 𝐵 ⊆ (Base‘𝑊))
9089, 80sseldd 3853 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) → 𝑢 ∈ (Base‘𝑊))
91 eqid 2772 . . . . . . . . . . . . . . . . . . . . . 22 (Scalar‘𝑊) = (Scalar‘𝑊)
92 eqid 2772 . . . . . . . . . . . . . . . . . . . . . 22 ( ·𝑠𝑊) = ( ·𝑠𝑊)
93 eqid 2772 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
9424, 91, 92, 93lmodvscl 19367 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ LMod ∧ ((𝑎𝑏)‘𝑢) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑢 ∈ (Base‘𝑊)) → (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢) ∈ (Base‘𝑊))
9553, 88, 90, 94syl3anc 1351 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝐵) → (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢) ∈ (Base‘𝑊))
96 simp-9l 780 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑊 ∈ LVec)
9796, 22syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑊 ∈ LMod)
98 eqidd 2773 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (Scalar‘𝑊) = (Scalar‘𝑊))
99 eqid 2772 . . . . . . . . . . . . . . . . . . . . 21 (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
10043adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑎𝑏):𝐵⟶(Base‘(Scalar‘𝑊)))
101100feqmptd 6556 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑎𝑏) = (𝑢𝐵 ↦ ((𝑎𝑏)‘𝑢)))
102101, 47eqbrtrrd 4947 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑢𝐵 ↦ ((𝑎𝑏)‘𝑢)) finSupp (0g‘(Scalar‘𝑊)))
10352, 97, 98, 24, 88, 90, 29, 99, 92, 102mptscmfsupp0 19415 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑢𝐵 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢)) finSupp 0 )
10437a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑉 ∩ (𝐵𝑉)) = ∅)
10524, 29, 48, 51, 52, 95, 103, 104, 83gsumsplit2 18796 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑊 Σg (𝑢𝐵 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢))) = ((𝑊 Σg (𝑢𝑉 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢)))(+g𝑊)(𝑊 Σg (𝑢 ∈ (𝐵𝑉) ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢)))))
10663oveq1d 6985 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢) = ((𝑎𝑢)( ·𝑠𝑊)𝑢))
107106mpteq2dva 5016 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑢𝑉 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢)) = (𝑢𝑉 ↦ ((𝑎𝑢)( ·𝑠𝑊)𝑢)))
108107oveq2d 6986 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑊 Σg (𝑢𝑉 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢))) = (𝑊 Σg (𝑢𝑉 ↦ ((𝑎𝑢)( ·𝑠𝑊)𝑢))))
10974oveq1d 6985 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢 ∈ (𝐵𝑉)) → (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢) = ((𝑏𝑢)( ·𝑠𝑊)𝑢))
110109mpteq2dva 5016 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑢 ∈ (𝐵𝑉) ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢)) = (𝑢 ∈ (𝐵𝑉) ↦ ((𝑏𝑢)( ·𝑠𝑊)𝑢)))
111110oveq2d 6986 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑊 Σg (𝑢 ∈ (𝐵𝑉) ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢))) = (𝑊 Σg (𝑢 ∈ (𝐵𝑉) ↦ ((𝑏𝑢)( ·𝑠𝑊)𝑢))))
112108, 111oveq12d 6988 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → ((𝑊 Σg (𝑢𝑉 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢)))(+g𝑊)(𝑊 Σg (𝑢 ∈ (𝐵𝑉) ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢)))) = ((𝑊 Σg (𝑢𝑉 ↦ ((𝑎𝑢)( ·𝑠𝑊)𝑢)))(+g𝑊)(𝑊 Σg (𝑢 ∈ (𝐵𝑉) ↦ ((𝑏𝑢)( ·𝑠𝑊)𝑢)))))
113 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣))))
114 fveq2 6493 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = 𝑣 → (𝑏𝑢) = (𝑏𝑣))
115114, 3oveq12d 6988 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = 𝑣 → ((𝑏𝑢)( ·𝑠𝑊)𝑢) = ((𝑏𝑣)( ·𝑠𝑊)𝑣))
116115cbvmptv 5022 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ (𝐵𝑉) ↦ ((𝑏𝑢)( ·𝑠𝑊)𝑢)) = (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣))
117116oveq2i 6981 . . . . . . . . . . . . . . . . . . . . . 22 (𝑊 Σg (𝑢 ∈ (𝐵𝑉) ↦ ((𝑏𝑢)( ·𝑠𝑊)𝑢))) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))
118113, 117syl6eqr 2826 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑢 ∈ (𝐵𝑉) ↦ ((𝑏𝑢)( ·𝑠𝑊)𝑢))))
1197, 118oveq12d 6988 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑥(+g𝑊)((invg𝑊)‘𝑥)) = ((𝑊 Σg (𝑢𝑉 ↦ ((𝑎𝑢)( ·𝑠𝑊)𝑢)))(+g𝑊)(𝑊 Σg (𝑢 ∈ (𝐵𝑉) ↦ ((𝑏𝑢)( ·𝑠𝑊)𝑢)))))
120 lmodgrp 19357 . . . . . . . . . . . . . . . . . . . . . 22 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
12196, 22, 1203syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑊 ∈ Grp)
12213, 27sstrd 3862 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → 𝑉 ⊆ (Base‘𝑊))
12324, 30lspssv 19471 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑊 ∈ LMod ∧ 𝑉 ⊆ (Base‘𝑊)) → (𝑁𝑉) ⊆ (Base‘𝑊))
12423, 122, 123syl2anc 576 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → (𝑁𝑉) ⊆ (Base‘𝑊))
125124ad7antr 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑁𝑉) ⊆ (Base‘𝑊))
126 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) → 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉)))
127126elin2d 4058 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) → 𝑥 ∈ (𝑁𝑉))
128127ad6antr 723 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑥 ∈ (𝑁𝑉))
129125, 128sseldd 3853 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑥 ∈ (Base‘𝑊))
130 eqid 2772 . . . . . . . . . . . . . . . . . . . . . 22 (invg𝑊) = (invg𝑊)
13124, 48, 29, 130grprinv 17934 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ Grp ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑥(+g𝑊)((invg𝑊)‘𝑥)) = 0 )
132121, 129, 131syl2anc 576 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑥(+g𝑊)((invg𝑊)‘𝑥)) = 0 )
133112, 119, 1323eqtr2d 2814 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → ((𝑊 Σg (𝑢𝑉 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢)))(+g𝑊)(𝑊 Σg (𝑢 ∈ (𝐵𝑉) ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢)))) = 0 )
134105, 133eqtrd 2808 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑊 Σg (𝑢𝐵 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢))) = 0 )
135 breq1 4926 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (𝑎𝑏) → (𝑐 finSupp (0g‘(Scalar‘𝑊)) ↔ (𝑎𝑏) finSupp (0g‘(Scalar‘𝑊))))
136 fveq1 6492 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑎𝑏) → (𝑐𝑢) = ((𝑎𝑏)‘𝑢))
137136oveq1d 6985 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑎𝑏) → ((𝑐𝑢)( ·𝑠𝑊)𝑢) = (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢))
138137mpteq2dv 5017 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑎𝑏) → (𝑢𝐵 ↦ ((𝑐𝑢)( ·𝑠𝑊)𝑢)) = (𝑢𝐵 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢)))
139138oveq2d 6986 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = (𝑎𝑏) → (𝑊 Σg (𝑢𝐵 ↦ ((𝑐𝑢)( ·𝑠𝑊)𝑢))) = (𝑊 Σg (𝑢𝐵 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢))))
140139eqeq1d 2774 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (𝑎𝑏) → ((𝑊 Σg (𝑢𝐵 ↦ ((𝑐𝑢)( ·𝑠𝑊)𝑢))) = 0 ↔ (𝑊 Σg (𝑢𝐵 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢))) = 0 ))
141135, 140anbi12d 621 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑎𝑏) → ((𝑐 finSupp (0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢𝐵 ↦ ((𝑐𝑢)( ·𝑠𝑊)𝑢))) = 0 ) ↔ ((𝑎𝑏) finSupp (0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢𝐵 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢))) = 0 )))
142 eqeq1 2776 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑎𝑏) → (𝑐 = (𝐵 × {(0g‘(Scalar‘𝑊))}) ↔ (𝑎𝑏) = (𝐵 × {(0g‘(Scalar‘𝑊))})))
143141, 142imbi12d 337 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑎𝑏) → (((𝑐 finSupp (0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢𝐵 ↦ ((𝑐𝑢)( ·𝑠𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 × {(0g‘(Scalar‘𝑊))})) ↔ (((𝑎𝑏) finSupp (0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢𝐵 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢))) = 0 ) → (𝑎𝑏) = (𝐵 × {(0g‘(Scalar‘𝑊))}))))
14425lbslinds 20673 . . . . . . . . . . . . . . . . . . . . . 22 𝐽 ⊆ (LIndS‘𝑊)
145144, 11sseldi 3850 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → 𝐵 ∈ (LIndS‘𝑊))
14624, 93, 91, 92, 29, 99islinds5 30605 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑊 ∈ LMod ∧ 𝐵 ⊆ (Base‘𝑊)) → (𝐵 ∈ (LIndS‘𝑊) ↔ ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝐵)((𝑐 finSupp (0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢𝐵 ↦ ((𝑐𝑢)( ·𝑠𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 × {(0g‘(Scalar‘𝑊))}))))
147146biimpa 469 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊 ∈ LMod ∧ 𝐵 ⊆ (Base‘𝑊)) ∧ 𝐵 ∈ (LIndS‘𝑊)) → ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝐵)((𝑐 finSupp (0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢𝐵 ↦ ((𝑐𝑢)( ·𝑠𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 × {(0g‘(Scalar‘𝑊))})))
14823, 27, 145, 147syl21anc 825 . . . . . . . . . . . . . . . . . . . 20 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝐵)((𝑐 finSupp (0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢𝐵 ↦ ((𝑐𝑢)( ·𝑠𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 × {(0g‘(Scalar‘𝑊))})))
149148ad7antr 725 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → ∀𝑐 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝐵)((𝑐 finSupp (0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢𝐵 ↦ ((𝑐𝑢)( ·𝑠𝑊)𝑢))) = 0 ) → 𝑐 = (𝐵 × {(0g‘(Scalar‘𝑊))})))
150 fvexd 6508 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (Base‘(Scalar‘𝑊)) ∈ V)
151150, 52elmapd 8214 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → ((𝑎𝑏) ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝐵) ↔ (𝑎𝑏):𝐵⟶(Base‘(Scalar‘𝑊))))
152100, 151mpbird 249 . . . . . . . . . . . . . . . . . . 19 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑎𝑏) ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝐵))
153143, 149, 152rspcdva 3535 . . . . . . . . . . . . . . . . . 18 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (((𝑎𝑏) finSupp (0g‘(Scalar‘𝑊)) ∧ (𝑊 Σg (𝑢𝐵 ↦ (((𝑎𝑏)‘𝑢)( ·𝑠𝑊)𝑢))) = 0 ) → (𝑎𝑏) = (𝐵 × {(0g‘(Scalar‘𝑊))})))
15447, 134, 153mp2and 686 . . . . . . . . . . . . . . . . 17 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑎𝑏) = (𝐵 × {(0g‘(Scalar‘𝑊))}))
155154reseq1d 5688 . . . . . . . . . . . . . . . 16 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → ((𝑎𝑏) ↾ 𝑉) = ((𝐵 × {(0g‘(Scalar‘𝑊))}) ↾ 𝑉))
156 fnunres1 30114 . . . . . . . . . . . . . . . . 17 ((𝑎 Fn 𝑉𝑏 Fn (𝐵𝑉) ∧ (𝑉 ∩ (𝐵𝑉)) = ∅) → ((𝑎𝑏) ↾ 𝑉) = 𝑎)
15755, 58, 104, 156syl3anc 1351 . . . . . . . . . . . . . . . 16 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → ((𝑎𝑏) ↾ 𝑉) = 𝑎)
158 xpssres 5728 . . . . . . . . . . . . . . . . 17 (𝑉𝐵 → ((𝐵 × {(0g‘(Scalar‘𝑊))}) ↾ 𝑉) = (𝑉 × {(0g‘(Scalar‘𝑊))}))
159158ad8antlr 728 . . . . . . . . . . . . . . . 16 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → ((𝐵 × {(0g‘(Scalar‘𝑊))}) ↾ 𝑉) = (𝑉 × {(0g‘(Scalar‘𝑊))}))
160155, 157, 1593eqtr3d 2816 . . . . . . . . . . . . . . 15 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑎 = (𝑉 × {(0g‘(Scalar‘𝑊))}))
161160adantr 473 . . . . . . . . . . . . . 14 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → 𝑎 = (𝑉 × {(0g‘(Scalar‘𝑊))}))
162161fveq1d 6495 . . . . . . . . . . . . 13 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → (𝑎𝑢) = ((𝑉 × {(0g‘(Scalar‘𝑊))})‘𝑢))
163 fvex 6506 . . . . . . . . . . . . . . 15 (0g‘(Scalar‘𝑊)) ∈ V
164163fvconst2 6787 . . . . . . . . . . . . . 14 (𝑢𝑉 → ((𝑉 × {(0g‘(Scalar‘𝑊))})‘𝑢) = (0g‘(Scalar‘𝑊)))
16561, 164syl 17 . . . . . . . . . . . . 13 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → ((𝑉 × {(0g‘(Scalar‘𝑊))})‘𝑢) = (0g‘(Scalar‘𝑊)))
166162, 165eqtrd 2808 . . . . . . . . . . . 12 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → (𝑎𝑢) = (0g‘(Scalar‘𝑊)))
167166oveq1d 6985 . . . . . . . . . . 11 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → ((𝑎𝑢)( ·𝑠𝑊)𝑢) = ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)𝑢))
168122ad8antr 727 . . . . . . . . . . . . 13 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → 𝑉 ⊆ (Base‘𝑊))
169168, 61sseldd 3853 . . . . . . . . . . . 12 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → 𝑢 ∈ (Base‘𝑊))
17024, 91, 92, 99, 29lmod0vs 19383 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ 𝑢 ∈ (Base‘𝑊)) → ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)𝑢) = 0 )
17197, 169, 170syl2an2r 672 . . . . . . . . . . 11 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)𝑢) = 0 )
172167, 171eqtrd 2808 . . . . . . . . . 10 (((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑢𝑉) → ((𝑎𝑢)( ·𝑠𝑊)𝑢) = 0 )
173172mpteq2dva 5016 . . . . . . . . 9 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑢𝑉 ↦ ((𝑎𝑢)( ·𝑠𝑊)𝑢)) = (𝑢𝑉0 ))
174173oveq2d 6986 . . . . . . . 8 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑊 Σg (𝑢𝑉 ↦ ((𝑎𝑢)( ·𝑠𝑊)𝑢))) = (𝑊 Σg (𝑢𝑉0 )))
175 cmnmnd 18675 . . . . . . . . . 10 (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
17651, 175syl 17 . . . . . . . . 9 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑊 ∈ Mnd)
177128elfvexd 6528 . . . . . . . . 9 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑉 ∈ V)
17829gsumz 17836 . . . . . . . . 9 ((𝑊 ∈ Mnd ∧ 𝑉 ∈ V) → (𝑊 Σg (𝑢𝑉0 )) = 0 )
179176, 177, 178syl2anc 576 . . . . . . . 8 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → (𝑊 Σg (𝑢𝑉0 )) = 0 )
1807, 174, 1793eqtrd 2812 . . . . . . 7 ((((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ 𝑏 finSupp (0g‘(Scalar‘𝑊))) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))) → 𝑥 = 0 )
181180anasss 459 . . . . . 6 (((((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))) ∧ (𝑏 finSupp (0g‘(Scalar‘𝑊)) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣))))) → 𝑥 = 0 )
182 eqid 2772 . . . . . . . . . . . . 13 (LSubSp‘𝑊) = (LSubSp‘𝑊)
18324, 182, 30lspcl 19464 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ (𝐵𝑉) ⊆ (Base‘𝑊)) → (𝑁‘(𝐵𝑉)) ∈ (LSubSp‘𝑊))
18423, 28, 183syl2anc 576 . . . . . . . . . . 11 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → (𝑁‘(𝐵𝑉)) ∈ (LSubSp‘𝑊))
185184adantr 473 . . . . . . . . . 10 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) → (𝑁‘(𝐵𝑉)) ∈ (LSubSp‘𝑊))
186182lsssubg 19445 . . . . . . . . . 10 ((𝑊 ∈ LMod ∧ (𝑁‘(𝐵𝑉)) ∈ (LSubSp‘𝑊)) → (𝑁‘(𝐵𝑉)) ∈ (SubGrp‘𝑊))
18723, 185, 186syl2an2r 672 . . . . . . . . 9 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) → (𝑁‘(𝐵𝑉)) ∈ (SubGrp‘𝑊))
188126elin1d 4057 . . . . . . . . 9 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) → 𝑥 ∈ (𝑁‘(𝐵𝑉)))
189130subginvcl 18066 . . . . . . . . 9 (((𝑁‘(𝐵𝑉)) ∈ (SubGrp‘𝑊) ∧ 𝑥 ∈ (𝑁‘(𝐵𝑉))) → ((invg𝑊)‘𝑥) ∈ (𝑁‘(𝐵𝑉)))
190187, 188, 189syl2anc 576 . . . . . . . 8 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) → ((invg𝑊)‘𝑥) ∈ (𝑁‘(𝐵𝑉)))
19130, 24, 93, 91, 99, 92, 23, 28ellspds 30606 . . . . . . . . 9 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → (((invg𝑊)‘𝑥) ∈ (𝑁‘(𝐵𝑉)) ↔ ∃𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))(𝑏 finSupp (0g‘(Scalar‘𝑊)) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣))))))
192191biimpa 469 . . . . . . . 8 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ ((invg𝑊)‘𝑥) ∈ (𝑁‘(𝐵𝑉))) → ∃𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))(𝑏 finSupp (0g‘(Scalar‘𝑊)) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))))
193190, 192syldan 582 . . . . . . 7 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) → ∃𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))(𝑏 finSupp (0g‘(Scalar‘𝑊)) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))))
194193ad3antrrr 717 . . . . . 6 (((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) → ∃𝑏 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 (𝐵𝑉))(𝑏 finSupp (0g‘(Scalar‘𝑊)) ∧ ((invg𝑊)‘𝑥) = (𝑊 Σg (𝑣 ∈ (𝐵𝑉) ↦ ((𝑏𝑣)( ·𝑠𝑊)𝑣)))))
195181, 194r19.29a 3228 . . . . 5 (((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ 𝑎 finSupp (0g‘(Scalar‘𝑊))) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))) → 𝑥 = 0 )
196195anasss 459 . . . 4 ((((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)) ∧ (𝑎 finSupp (0g‘(Scalar‘𝑊)) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣))))) → 𝑥 = 0 )
19730, 24, 93, 91, 99, 92, 23, 122ellspds 30606 . . . . . 6 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → (𝑥 ∈ (𝑁𝑉) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)(𝑎 finSupp (0g‘(Scalar‘𝑊)) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣))))))
198197biimpa 469 . . . . 5 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ (𝑁𝑉)) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)(𝑎 finSupp (0g‘(Scalar‘𝑊)) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))))
199127, 198syldan 582 . . . 4 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑊)) ↑𝑚 𝑉)(𝑎 finSupp (0g‘(Scalar‘𝑊)) ∧ 𝑥 = (𝑊 Σg (𝑣𝑉 ↦ ((𝑎𝑣)( ·𝑠𝑊)𝑣)))))
200196, 199r19.29a 3228 . . 3 ((((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) ∧ 𝑥 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉))) → 𝑥 = 0 )
20129, 24, 300ellsp 30607 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑉 ⊆ (Base‘𝑊)) → 0 ∈ (𝑁𝑉))
20223, 122, 201syl2anc 576 . . . 4 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → 0 ∈ (𝑁𝑉))
20332, 202elind 4053 . . 3 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → 0 ∈ ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉)))
204200, 203eqsnd 30057 . 2 (((𝑊 ∈ LVec ∧ 𝐵𝐽) ∧ 𝑉𝐵) → ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉)) = { 0 })
2052043impa 1090 1 ((𝑊 ∈ LVec ∧ 𝐵𝐽𝑉𝐵) → ((𝑁‘(𝐵𝑉)) ∩ (𝑁𝑉)) = { 0 })
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wo 833  w3a 1068   = wceq 1507  wcel 2050  wral 3082  wrex 3083  Vcvv 3409  cdif 3820  cun 3821  cin 3822  wss 3823  c0 4172  {csn 4435   class class class wbr 4923  cmpt 5002   × cxp 5399  cres 5403   Fn wfn 6177  wf 6178  cfv 6182  (class class class)co 6970  𝑚 cmap 8200   finSupp cfsupp 8622  Basecbs 16333  +gcplusg 16415  Scalarcsca 16418   ·𝑠 cvsca 16419  0gc0g 16563   Σg cgsu 16564  Mndcmnd 17756  Grpcgrp 17885  invgcminusg 17886  SubGrpcsubg 18051  CMndccmn 18660  LModclmod 19350  LSubSpclss 19419  LSpanclspn 19459  LBasisclbs 19562  LVecclvec 19590  LIndSclinds 20645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-cnex 10385  ax-resscn 10386  ax-1cn 10387  ax-icn 10388  ax-addcl 10389  ax-addrcl 10390  ax-mulcl 10391  ax-mulrcl 10392  ax-mulcom 10393  ax-addass 10394  ax-mulass 10395  ax-distr 10396  ax-i2m1 10397  ax-1ne0 10398  ax-1rid 10399  ax-rnegex 10400  ax-rrecex 10401  ax-cnre 10402  ax-pre-lttri 10403  ax-pre-lttrn 10404  ax-pre-ltadd 10405  ax-pre-mulgt0 10406
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-pss 3839  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-iin 4789  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5306  df-eprel 5311  df-po 5320  df-so 5321  df-fr 5360  df-se 5361  df-we 5362  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-of 7221  df-om 7391  df-1st 7495  df-2nd 7496  df-supp 7628  df-wrecs 7744  df-recs 7806  df-rdg 7844  df-1o 7899  df-oadd 7903  df-er 8083  df-map 8202  df-ixp 8254  df-en 8301  df-dom 8302  df-sdom 8303  df-fin 8304  df-fsupp 8623  df-sup 8695  df-oi 8763  df-card 9156  df-pnf 10470  df-mnf 10471  df-xr 10472  df-ltxr 10473  df-le 10474  df-sub 10666  df-neg 10667  df-nn 11434  df-2 11497  df-3 11498  df-4 11499  df-5 11500  df-6 11501  df-7 11502  df-8 11503  df-9 11504  df-n0 11702  df-z 11788  df-dec 11906  df-uz 12053  df-fz 12703  df-fzo 12844  df-seq 13179  df-hash 13500  df-struct 16335  df-ndx 16336  df-slot 16337  df-base 16339  df-sets 16340  df-ress 16341  df-plusg 16428  df-mulr 16429  df-sca 16431  df-vsca 16432  df-ip 16433  df-tset 16434  df-ple 16435  df-ds 16437  df-hom 16439  df-cco 16440  df-0g 16565  df-gsum 16566  df-prds 16571  df-pws 16573  df-mre 16709  df-mrc 16710  df-acs 16712  df-mgm 17704  df-sgrp 17746  df-mnd 17757  df-mhm 17797  df-submnd 17798  df-grp 17888  df-minusg 17889  df-sbg 17890  df-mulg 18006  df-subg 18054  df-ghm 18121  df-cntz 18212  df-cmn 18662  df-abl 18663  df-mgp 18957  df-ur 18969  df-ring 19016  df-subrg 19250  df-lmod 19352  df-lss 19420  df-lsp 19460  df-lmhm 19510  df-lbs 19563  df-lvec 19591  df-sra 19660  df-rgmod 19661  df-nzr 19746  df-dsmm 20572  df-frlm 20587  df-uvc 20623  df-lindf 20646  df-linds 20647
This theorem is referenced by:  dimkerim  30652
  Copyright terms: Public domain W3C validator