Metamath Proof Explorer

Theorem lspexch

Description: Exchange property for span of a pair. TODO: see if a version with Y,Z and X,Z reversed will shorten proofs (analogous to lspexchn1 versus lspexchn2 ); look for lspexch and prcom in same proof. TODO: would a hypothesis of -. X e. ( N{ Z } ) instead of ( N{ X } ) =/= ( N{ Z } ) be better overall? This would be shorter and also satisfy the X =/= .0. condition. Here and also lspindp* and all proofs affected by them (all in NM's mathbox); there are 58 hypotheses with the =/= pattern as of 24-May-2015. (Contributed by NM, 11-Apr-2015)

Ref Expression
Hypotheses lspexch.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspexch.o ⊢ 0 = ( 0g ‘ 𝑊 )
lspexch.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspexch.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lspexch.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lspexch.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lspexch.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
lspexch.q ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
lspexch.e ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
Assertion lspexch ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )

Proof

Step Hyp Ref Expression
1 lspexch.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspexch.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lspexch.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspexch.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lspexch.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
6 lspexch.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 lspexch.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
8 lspexch.q ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
9 lspexch.e ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
10 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
11 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
13 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
14 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
15 4 14 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
16 1 10 11 12 13 3 15 6 7 lspprel ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ∃ 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) )
17 9 16 mpbid ⊢ ( 𝜑 → ∃ 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
18 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
19 eqid ⊢ ( invg ‘ ( Scalar ‘ 𝑊 ) ) = ( invg ‘ ( Scalar ‘ 𝑊 ) )
20 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑊 ∈ LVec )
21 20 14 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑊 ∈ LMod )
22 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
23 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
24 23 eldifad ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑋 ∈ 𝑉 )
25 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑍 ∈ 𝑉 )
26 1 10 18 13 11 12 19 21 22 24 25 lmodsubvs ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
27 simp3 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
28 27 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = 𝑋 )
29 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑊 ∈ LMod )
30 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
31 29 30 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑊 ∈ Grp )
32 1 11 13 12 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑍 ∈ 𝑉 ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 )
33 21 22 25 32 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 )
34 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
35 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑌 ∈ 𝑉 )
36 1 11 13 12 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
37 21 34 35 36 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
38 1 10 18 grpsubadd ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑋 ∈ 𝑉 ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 ∧ ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ↔ ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = 𝑋 ) )
39 31 24 33 37 38 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ↔ ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = 𝑋 ) )
40 28 39 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
41 26 40 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
42 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
43 eqid ⊢ ( invr ‘ ( Scalar ‘ 𝑊 ) ) = ( invr ‘ ( Scalar ‘ 𝑊 ) )
44 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
45 20 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑊 ∈ LVec )
46 25 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑍 ∈ 𝑉 )
47 27 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
48 oveq1 ⊢ ( 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
49 48 oveq1d ⊢ ( 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
50 1 11 13 42 2 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 0 )
51 21 35 50 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 0 )
52 51 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 0 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
53 1 10 2 lmod0vlid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 ) → ( 0 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) )
54 21 33 53 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 0 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) )
55 52 54 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) )
56 49 55 sylan9eqr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) )
57 47 56 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) )
58 1 13 11 12 3 21 22 25 lspsneli ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
60 57 59 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑍 } ) )
61 eldifsni ⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
62 23 61 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑋 ≠ 0 )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 ≠ 0 )
64 1 2 3 45 46 60 63 lspsneleq ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑍 } ) )
65 64 ex ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑗 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑍 } ) ) )
66 65 necon3d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) → 𝑗 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
67 44 66 mpd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑗 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
68 eldifsn ⊢ ( 𝑗 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ↔ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑗 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
69 34 67 68 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑗 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
70 11 lmodfgrp ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Grp )
71 29 70 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( Scalar ‘ 𝑊 ) ∈ Grp )
72 12 19 grpinvcl ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
73 71 22 72 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
74 1 11 13 12 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑍 ∈ 𝑉 ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 )
75 21 73 25 74 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 )
76 1 10 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ 𝑉 )
77 21 24 75 76 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ 𝑉 )
78 1 13 11 12 42 43 20 69 77 35 lvecinv ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ↔ 𝑌 = ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ) )
79 41 78 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑌 = ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) )
80 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
81 1 80 3 21 24 25 lspprcl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
82 11 lvecdrng ⊢ ( 𝑊 ∈ LVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
83 20 82 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( Scalar ‘ 𝑊 ) ∈ DivRing )
84 12 42 43 drnginvrcl ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑗 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
85 83 34 67 84 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
86 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
87 1 11 13 86 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 𝑋 )
88 21 24 87 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 𝑋 )
89 88 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
90 11 lmodring ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring )
91 12 86 ringidcl ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Ring → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
92 21 90 91 3syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
93 1 10 13 11 12 3 21 92 73 24 25 lsppreli ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
94 89 93 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
95 11 13 12 80 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
96 21 81 85 94 95 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
97 79 96 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
98 97 3exp ⊢ ( 𝜑 → ( ( 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ) )
99 98 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑋 = ( ( 𝑗 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
100 17 99 mpd ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )