Metamath Proof Explorer

Theorem prjspeclsp

Description: The vectors equivalent to a vector X are the nonzero vectors in the span of X . (Contributed by Steven Nguyen, 6-Jun-2023)

Ref Expression
Hypotheses prjsprel.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
prjspertr.b ⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
prjspertr.s ⊢ 𝑆 = ( Scalar ‘ 𝑉 )
prjspertr.x ⊢ · = ( ·𝑠 ‘ 𝑉 )
prjspertr.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
prjsprellsp.n ⊢ 𝑁 = ( LSpan ‘ 𝑉 )
Assertion prjspeclsp ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → [ 𝑋 ] ∼ = ( ( 𝑁 ‘ { 𝑋 } ) ∖ { ( 0g ‘ 𝑉 ) } ) )

Proof

Step Hyp Ref Expression
1 prjsprel.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
2 prjspertr.b ⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
3 prjspertr.s ⊢ 𝑆 = ( Scalar ‘ 𝑉 )
4 prjspertr.x ⊢ · = ( ·𝑠 ‘ 𝑉 )
5 prjspertr.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
6 prjsprellsp.n ⊢ 𝑁 = ( LSpan ‘ 𝑉 )
7 1 cnveqi ⊢ ◡ ∼ = ◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
8 cnvopab ⊢ ◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
9 7 8 eqtri ⊢ ◡ ∼ = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
10 9 eceq2i ⊢ [ 𝑋 ] ◡ ∼ = [ 𝑋 ] { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
11 df-ec ⊢ [ 𝑋 ] { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } = ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } “ { 𝑋 } )
12 11 a1i ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → [ 𝑋 ] { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } = ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } “ { 𝑋 } ) )
13 imaopab ⊢ ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } “ { 𝑋 } ) = { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑋 } ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
14 13 a1i ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } “ { 𝑋 } ) = { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑋 } ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } )
15 df-rex ⊢ ( ∃ 𝑦 ∈ { 𝑋 } ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ { 𝑋 } ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ) )
16 velsn ⊢ ( 𝑦 ∈ { 𝑋 } ↔ 𝑦 = 𝑋 )
17 16 anbi1i ⊢ ( ( 𝑦 ∈ { 𝑋 } ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ) ↔ ( 𝑦 = 𝑋 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ) )
18 eleq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵 ) )
19 18 anbi2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) )
20 oveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝑙 · 𝑦 ) = ( 𝑙 · 𝑋 ) )
21 20 eqeq2d ⊢ ( 𝑦 = 𝑋 → ( 𝑥 = ( 𝑙 · 𝑦 ) ↔ 𝑥 = ( 𝑙 · 𝑋 ) ) )
22 21 rexbidv ⊢ ( 𝑦 = 𝑋 → ( ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ↔ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) )
23 19 22 anbi12d ⊢ ( 𝑦 = 𝑋 → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ) )
24 23 pm5.32i ⊢ ( ( 𝑦 = 𝑋 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ) ↔ ( 𝑦 = 𝑋 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ) )
25 17 24 bitri ⊢ ( ( 𝑦 ∈ { 𝑋 } ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ) ↔ ( 𝑦 = 𝑋 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ) )
26 25 exbii ⊢ ( ∃ 𝑦 ( 𝑦 ∈ { 𝑋 } ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ) ↔ ∃ 𝑦 ( 𝑦 = 𝑋 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ) )
27 19.41v ⊢ ( ∃ 𝑦 ( 𝑦 = 𝑋 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ) ↔ ( ∃ 𝑦 𝑦 = 𝑋 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ) )
28 elisset ⊢ ( 𝑋 ∈ 𝐵 → ∃ 𝑦 𝑦 = 𝑋 )
29 28 ad2antlr ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) → ∃ 𝑦 𝑦 = 𝑋 )
30 29 pm4.71ri ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ↔ ( ∃ 𝑦 𝑦 = 𝑋 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ) )
31 27 30 bitr4i ⊢ ( ∃ 𝑦 ( 𝑦 = 𝑋 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) )
32 15 26 31 3bitri ⊢ ( ∃ 𝑦 ∈ { 𝑋 } ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) )
33 32 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑋 } ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) }
34 iba ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) )
35 34 bicomd ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐵 ) )
36 35 anbi1d ⊢ ( 𝑋 ∈ 𝐵 → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ) )
37 36 abbidv ⊢ ( 𝑋 ∈ 𝐵 → { 𝑥 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) } )
38 33 37 syl5eq ⊢ ( 𝑋 ∈ 𝐵 → { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑋 } ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) } )
39 38 adantl ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → { 𝑥 ∣ ∃ 𝑦 ∈ { 𝑋 } ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) } )
40 12 14 39 3eqtrd ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → [ 𝑋 ] { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) } )
41 10 40 syl5eq ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → [ 𝑋 ] ◡ ∼ = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) } )
42 df-rab ⊢ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) }
43 42 a1i ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → { 𝑥 ∈ 𝐵 ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) } )
44 2 rabeqi ⊢ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } = { 𝑥 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) }
45 rabdif ⊢ ( { 𝑥 ∈ ( Base ‘ 𝑉 ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } ∖ { ( 0g ‘ 𝑉 ) } ) = { 𝑥 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) }
46 45 a1i ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → ( { 𝑥 ∈ ( Base ‘ 𝑉 ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } ∖ { ( 0g ‘ 𝑉 ) } ) = { 𝑥 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } )
47 44 46 eqtr4id ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → { 𝑥 ∈ 𝐵 ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } = ( { 𝑥 ∈ ( Base ‘ 𝑉 ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } ∖ { ( 0g ‘ 𝑉 ) } ) )
48 41 43 47 3eqtr2d ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → [ 𝑋 ] ◡ ∼ = ( { 𝑥 ∈ ( Base ‘ 𝑉 ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } ∖ { ( 0g ‘ 𝑉 ) } ) )
49 1 2 3 4 5 prjsper ⊢ ( 𝑉 ∈ LVec → ∼ Er 𝐵 )
50 49 adantr ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → ∼ Er 𝐵 )
51 ercnv ⊢ ( ∼ Er 𝐵 → ◡ ∼ = ∼ )
52 51 eqcomd ⊢ ( ∼ Er 𝐵 → ∼ = ◡ ∼ )
53 50 52 syl ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → ∼ = ◡ ∼ )
54 53 eceq2d ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → [ 𝑋 ] ∼ = [ 𝑋 ] ◡ ∼ )
55 lveclmod ⊢ ( 𝑉 ∈ LVec → 𝑉 ∈ LMod )
56 difss ⊢ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) ⊆ ( Base ‘ 𝑉 )
57 2 56 eqsstri ⊢ 𝐵 ⊆ ( Base ‘ 𝑉 )
58 57 sseli ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝑉 ) )
59 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
60 3 5 59 4 6 lspsn ⊢ ( ( 𝑉 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑉 ) ) → ( 𝑁 ‘ { 𝑋 } ) = { 𝑥 ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } )
61 55 58 60 syl2an ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ { 𝑋 } ) = { 𝑥 ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } )
62 simpr ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑙 ∈ 𝐾 ) ∧ 𝑥 = ( 𝑙 · 𝑋 ) ) → 𝑥 = ( 𝑙 · 𝑋 ) )
63 55 adantr ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → 𝑉 ∈ LMod )
64 63 adantr ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑙 ∈ 𝐾 ) → 𝑉 ∈ LMod )
65 simpr ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑙 ∈ 𝐾 ) → 𝑙 ∈ 𝐾 )
66 58 ad2antlr ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑙 ∈ 𝐾 ) → 𝑋 ∈ ( Base ‘ 𝑉 ) )
67 59 3 4 5 lmodvscl ⊢ ( ( 𝑉 ∈ LMod ∧ 𝑙 ∈ 𝐾 ∧ 𝑋 ∈ ( Base ‘ 𝑉 ) ) → ( 𝑙 · 𝑋 ) ∈ ( Base ‘ 𝑉 ) )
68 64 65 66 67 syl3anc ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑙 ∈ 𝐾 ) → ( 𝑙 · 𝑋 ) ∈ ( Base ‘ 𝑉 ) )
69 68 adantr ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑙 ∈ 𝐾 ) ∧ 𝑥 = ( 𝑙 · 𝑋 ) ) → ( 𝑙 · 𝑋 ) ∈ ( Base ‘ 𝑉 ) )
70 62 69 eqeltrd ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑙 ∈ 𝐾 ) ∧ 𝑥 = ( 𝑙 · 𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑉 ) )
71 70 rexlimdva2 ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) → 𝑥 ∈ ( Base ‘ 𝑉 ) ) )
72 71 pm4.71rd ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑉 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) ) )
73 72 abbidv ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → { 𝑥 ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } = { 𝑥 ∣ ( 𝑥 ∈ ( Base ‘ 𝑉 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) } )
74 df-rab ⊢ { 𝑥 ∈ ( Base ‘ 𝑉 ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } = { 𝑥 ∣ ( 𝑥 ∈ ( Base ‘ 𝑉 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) ) }
75 73 74 eqtr4di ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → { 𝑥 ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } = { 𝑥 ∈ ( Base ‘ 𝑉 ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } )
76 61 75 eqtrd ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ { 𝑋 } ) = { 𝑥 ∈ ( Base ‘ 𝑉 ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } )
77 76 difeq1d ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ { 𝑋 } ) ∖ { ( 0g ‘ 𝑉 ) } ) = ( { 𝑥 ∈ ( Base ‘ 𝑉 ) ∣ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑋 ) } ∖ { ( 0g ‘ 𝑉 ) } ) )
78 48 54 77 3eqtr4d ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ) → [ 𝑋 ] ∼ = ( ( 𝑁 ‘ { 𝑋 } ) ∖ { ( 0g ‘ 𝑉 ) } ) )