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	lspsnel5	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) )
46	40 45	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
47	2 3 1 5 6	lspsnel	⊢ ( ( 𝑊 ∈ 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 } ) 𝑋 = ( 𝑘 · 𝑌 ) ) )