This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspsneq

Description: Equal spans of singletons must have proportional vectors. See lspsnss2 for comparable span version. TODO: can proof be shortened? (Contributed by NM, 21-Mar-2015)

Ref Expression
Hypotheses lspsneq.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsneq.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
lspsneq.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
lspsneq.o ⊢ 0 = ( 0g ‘ 𝑆 )
lspsneq.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lspsneq.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsneq.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lspsneq.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspsneq.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion lspsneq ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑘 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑘 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lspsneq.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsneq.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
3 lspsneq.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
4 lspsneq.o ⊢ 0 = ( 0g ‘ 𝑆 )
5 lspsneq.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 lspsneq.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
7 lspsneq.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
8 lspsneq.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 lspsneq.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11 7 10 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
12 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑆 ∈ Ring )
13 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
14 3 13 ringidcl ⊢ ( 𝑆 ∈ Ring → ( 1r ‘ 𝑆 ) ∈ 𝐾 )
15 11 12 14 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ 𝐾 )
16 2 lvecdrng ⊢ ( 𝑊 ∈ LVec → 𝑆 ∈ DivRing )
17 4 13 drngunz ⊢ ( 𝑆 ∈ DivRing → ( 1r ‘ 𝑆 ) ≠ 0 )
18 7 16 17 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ≠ 0 )
19 eldifsn ⊢ ( ( 1r ‘ 𝑆 ) ∈ ( 𝐾 ∖ { 0 } ) ↔ ( ( 1r ‘ 𝑆 ) ∈ 𝐾 ∧ ( 1r ‘ 𝑆 ) ≠ 0 ) )
20 15 18 19 sylanbrc ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( 𝐾 ∖ { 0 } ) )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 = ( 0g ‘ 𝑊 ) ) → ( 1r ‘ 𝑆 ) ∈ ( 𝐾 ∖ { 0 } ) )
22 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
23 1 22 lmod0vcl ⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
24 1 2 5 13 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ) → ( ( 1r ‘ 𝑆 ) · ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
25 11 23 24 syl2anc2 ⊢ ( 𝜑 → ( ( 1r ‘ 𝑆 ) · ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 = ( 0g ‘ 𝑊 ) ) → ( ( 1r ‘ 𝑆 ) · ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
27 oveq2 ⊢ ( 𝑌 = ( 0g ‘ 𝑊 ) → ( ( 1r ‘ 𝑆 ) · 𝑌 ) = ( ( 1r ‘ 𝑆 ) · ( 0g ‘ 𝑊 ) ) )
28 27 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 = ( 0g ‘ 𝑊 ) ) → ( ( 1r ‘ 𝑆 ) · 𝑌 ) = ( ( 1r ‘ 𝑆 ) · ( 0g ‘ 𝑊 ) ) )
29 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → 𝑊 ∈ LMod )
30 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ∈ 𝑉 )
31 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → 𝑌 ∈ 𝑉 )
32 simpr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
33 1 22 6 29 30 31 32 lspsneq0b ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑋 = ( 0g ‘ 𝑊 ) ↔ 𝑌 = ( 0g ‘ 𝑊 ) ) )
34 33 biimpar ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 = ( 0g ‘ 𝑊 ) ) → 𝑋 = ( 0g ‘ 𝑊 ) )
35 26 28 34 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 = ( 0g ‘ 𝑊 ) ) → 𝑋 = ( ( 1r ‘ 𝑆 ) · 𝑌 ) )
36 oveq1 ⊢ ( 𝑗 = ( 1r ‘ 𝑆 ) → ( 𝑗 · 𝑌 ) = ( ( 1r ‘ 𝑆 ) · 𝑌 ) )
37 36 rspceeqv ⊢ ( ( ( 1r ‘ 𝑆 ) ∈ ( 𝐾 ∖ { 0 } ) ∧ 𝑋 = ( ( 1r ‘ 𝑆 ) · 𝑌 ) ) → ∃ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑗 · 𝑌 ) )
38 21 35 37 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 = ( 0g ‘ 𝑊 ) ) → ∃ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑗 · 𝑌 ) )
39 eqimss ⊢ ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) )
40 39 adantl ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) )
41 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
42 1 41 6 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
43 11 9 42 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
45 1 41 6 29 44 30 ellspsn5b ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) )
46 40 45 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
47 2 3 1 5 6 ellspsn ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑗 ∈ 𝐾 𝑋 = ( 𝑗 · 𝑌 ) ) )
48 29 31 47 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑗 ∈ 𝐾 𝑋 = ( 𝑗 · 𝑌 ) ) )
49 46 48 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ∃ 𝑗 ∈ 𝐾 𝑋 = ( 𝑗 · 𝑌 ) )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) → ∃ 𝑗 ∈ 𝐾 𝑋 = ( 𝑗 · 𝑌 ) )
51 simprl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) ) → 𝑗 ∈ 𝐾 )
52 simpr ⊢ ( ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) → 𝑋 = ( 𝑗 · 𝑌 ) )
53 52 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) ) → 𝑋 = ( 𝑗 · 𝑌 ) )
54 33 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑋 = ( 0g ‘ 𝑊 ) → 𝑌 = ( 0g ‘ 𝑊 ) ) )
55 54 necon3d ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑌 ≠ ( 0g ‘ 𝑊 ) → 𝑋 ≠ ( 0g ‘ 𝑊 ) ) )
56 55 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) → 𝑋 ≠ ( 0g ‘ 𝑊 ) )
57 56 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) ) → 𝑋 ≠ ( 0g ‘ 𝑊 ) )
58 53 57 eqnetrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) ) → ( 𝑗 · 𝑌 ) ≠ ( 0g ‘ 𝑊 ) )
59 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → 𝑊 ∈ LVec )
60 59 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) ) → 𝑊 ∈ LVec )
61 31 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) ) → 𝑌 ∈ 𝑉 )
62 1 5 2 3 4 22 60 51 61 lvecvsn0 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) ) → ( ( 𝑗 · 𝑌 ) ≠ ( 0g ‘ 𝑊 ) ↔ ( 𝑗 ≠ 0 ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ) )
63 58 62 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) ) → ( 𝑗 ≠ 0 ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) )
64 63 simpld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) ) → 𝑗 ≠ 0 )
65 eldifsn ⊢ ( 𝑗 ∈ ( 𝐾 ∖ { 0 } ) ↔ ( 𝑗 ∈ 𝐾 ∧ 𝑗 ≠ 0 ) )
66 51 64 65 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑋 = ( 𝑗 · 𝑌 ) ) ) → 𝑗 ∈ ( 𝐾 ∖ { 0 } ) )
67 50 66 53 reximssdv ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) → ∃ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑗 · 𝑌 ) )
68 38 67 pm2.61dane ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ∃ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑗 · 𝑌 ) )
69 68 ex ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ∃ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑗 · 𝑌 ) ) )
70 7 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑊 ∈ LVec )
71 eldifi ⊢ ( 𝑗 ∈ ( 𝐾 ∖ { 0 } ) → 𝑗 ∈ 𝐾 )
72 71 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑗 ∈ 𝐾 )
73 eldifsni ⊢ ( 𝑗 ∈ ( 𝐾 ∖ { 0 } ) → 𝑗 ≠ 0 )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑗 ≠ 0 )
75 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑌 ∈ 𝑉 )
76 1 2 5 3 4 6 lspsnvs ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑗 ≠ 0 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑗 · 𝑌 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )
77 70 72 74 75 76 syl121anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 ‘ { ( 𝑗 · 𝑌 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )
78 77 ex ⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝐾 ∖ { 0 } ) → ( 𝑁 ‘ { ( 𝑗 · 𝑌 ) } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
79 sneq ⊢ ( 𝑋 = ( 𝑗 · 𝑌 ) → { 𝑋 } = { ( 𝑗 · 𝑌 ) } )
80 79 fveqeq2d ⊢ ( 𝑋 = ( 𝑗 · 𝑌 ) → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { ( 𝑗 · 𝑌 ) } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
81 80 biimprcd ⊢ ( ( 𝑁 ‘ { ( 𝑗 · 𝑌 ) } ) = ( 𝑁 ‘ { 𝑌 } ) → ( 𝑋 = ( 𝑗 · 𝑌 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
82 78 81 syl6 ⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝐾 ∖ { 0 } ) → ( 𝑋 = ( 𝑗 · 𝑌 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ) )
83 82 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑗 · 𝑌 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
84 69 83 impbid ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑗 · 𝑌 ) ) )
85 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 · 𝑌 ) = ( 𝑘 · 𝑌 ) )
86 85 eqeq2d ⊢ ( 𝑗 = 𝑘 → ( 𝑋 = ( 𝑗 · 𝑌 ) ↔ 𝑋 = ( 𝑘 · 𝑌 ) ) )
87 86 cbvrexvw ⊢ ( ∃ 𝑗 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑗 · 𝑌 ) ↔ ∃ 𝑘 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑘 · 𝑌 ) )
88 84 87 bitrdi ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑘 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑘 · 𝑌 ) ) )