Theorem prjspersym

Description: The relation in PrjSp is symmetric. (Contributed by Steven Nguyen, 1-May-2023)

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

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		simpllr	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑋 ∼ 𝑌 )
7	1	prjsprel	⊢ ( 𝑋 ∼ 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) )
8		pm3.22	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
9	8	adantr	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) → ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
10	7 9	sylbi	⊢ ( 𝑋 ∼ 𝑌 → ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
11	6 10	syl	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
12		oveq1	⊢ ( 𝑛 = ( ( invr ‘ 𝑆 ) ‘ 𝑚 ) → ( 𝑛 · 𝑋 ) = ( ( ( invr ‘ 𝑆 ) ‘ 𝑚 ) · 𝑋 ) )
13	12	eqeq2d	⊢ ( 𝑛 = ( ( invr ‘ 𝑆 ) ‘ 𝑚 ) → ( 𝑌 = ( 𝑛 · 𝑋 ) ↔ 𝑌 = ( ( ( invr ‘ 𝑆 ) ‘ 𝑚 ) · 𝑋 ) ) )
14		simplll	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑉 ∈ LVec )
15	3	lvecdrng	⊢ ( 𝑉 ∈ LVec → 𝑆 ∈ DivRing )
16	14 15	syl	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑆 ∈ DivRing )
17		simplr	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑚 ∈ 𝐾 )
18		simpll	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑋 ∈ 𝐵 )
19	7 18	sylbi	⊢ ( 𝑋 ∼ 𝑌 → 𝑋 ∈ 𝐵 )
20		eldifsni	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
21	20 2	eleq2s	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
22	6 19 21	3syl	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
23		simplr	⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ∧ 𝑚 = ( 0g ‘ 𝑆 ) ) → 𝑋 = ( 𝑚 · 𝑌 ) )
24		simpr	⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ∧ 𝑚 = ( 0g ‘ 𝑆 ) ) → 𝑚 = ( 0g ‘ 𝑆 ) )
25	24	oveq1d	⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ∧ 𝑚 = ( 0g ‘ 𝑆 ) ) → ( 𝑚 · 𝑌 ) = ( ( 0g ‘ 𝑆 ) · 𝑌 ) )
26		lveclmod	⊢ ( 𝑉 ∈ LVec → 𝑉 ∈ LMod )
27	26	ad4antr	⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ∧ 𝑚 = ( 0g ‘ 𝑆 ) ) → 𝑉 ∈ LMod )
28		simplr	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑌 ∈ 𝐵 )
29	7 28	sylbi	⊢ ( 𝑋 ∼ 𝑌 → 𝑌 ∈ 𝐵 )
30		eldifi	⊢ ( 𝑌 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑌 ∈ ( Base ‘ 𝑉 ) )
31	30 2	eleq2s	⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( Base ‘ 𝑉 ) )
32	6 29 31	3syl	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑌 ∈ ( Base ‘ 𝑉 ) )
33	32	adantr	⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ∧ 𝑚 = ( 0g ‘ 𝑆 ) ) → 𝑌 ∈ ( Base ‘ 𝑉 ) )
34		eqid	⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
35		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
36		eqid	⊢ ( 0g ‘ 𝑉 ) = ( 0g ‘ 𝑉 )
37	34 3 4 35 36	lmod0vs	⊢ ( ( 𝑉 ∈ LMod ∧ 𝑌 ∈ ( Base ‘ 𝑉 ) ) → ( ( 0g ‘ 𝑆 ) · 𝑌 ) = ( 0g ‘ 𝑉 ) )
38	27 33 37	syl2anc	⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ∧ 𝑚 = ( 0g ‘ 𝑆 ) ) → ( ( 0g ‘ 𝑆 ) · 𝑌 ) = ( 0g ‘ 𝑉 ) )
39	23 25 38	3eqtrd	⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ∧ 𝑚 = ( 0g ‘ 𝑆 ) ) → 𝑋 = ( 0g ‘ 𝑉 ) )
40	22 39	mteqand	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑚 ≠ ( 0g ‘ 𝑆 ) )
41		eqid	⊢ ( invr ‘ 𝑆 ) = ( invr ‘ 𝑆 )
42	5 35 41	drnginvrcl	⊢ ( ( 𝑆 ∈ DivRing ∧ 𝑚 ∈ 𝐾 ∧ 𝑚 ≠ ( 0g ‘ 𝑆 ) ) → ( ( invr ‘ 𝑆 ) ‘ 𝑚 ) ∈ 𝐾 )
43	16 17 40 42	syl3anc	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → ( ( invr ‘ 𝑆 ) ‘ 𝑚 ) ∈ 𝐾 )
44		simpr	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑋 = ( 𝑚 · 𝑌 ) )
45		nelsn	⊢ ( 𝑚 ≠ ( 0g ‘ 𝑆 ) → ¬ 𝑚 ∈ { ( 0g ‘ 𝑆 ) } )
46	40 45	syl	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → ¬ 𝑚 ∈ { ( 0g ‘ 𝑆 ) } )
47	17 46	eldifd	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑚 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝑆 ) } ) )
48		eldifi	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑋 ∈ ( Base ‘ 𝑉 ) )
49	48 2	eleq2s	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝑉 ) )
50	6 19 49	3syl	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝑉 ) )
51	34 4 3 5 35 41 14 47 50 32	lvecinv	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → ( 𝑋 = ( 𝑚 · 𝑌 ) ↔ 𝑌 = ( ( ( invr ‘ 𝑆 ) ‘ 𝑚 ) · 𝑋 ) ) )
52	44 51	mpbid	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑌 = ( ( ( invr ‘ 𝑆 ) ‘ 𝑚 ) · 𝑋 ) )
53	13 43 52	rspcedvdw	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → ∃ 𝑛 ∈ 𝐾 𝑌 = ( 𝑛 · 𝑋 ) )
54	1	prjsprel	⊢ ( 𝑌 ∼ 𝑋 ↔ ( ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑛 ∈ 𝐾 𝑌 = ( 𝑛 · 𝑋 ) ) )
55	11 53 54	sylanbrc	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) ∧ 𝑚 ∈ 𝐾 ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑌 ∼ 𝑋 )
56		simpr	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) → ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) )
57	7 56	sylbi	⊢ ( 𝑋 ∼ 𝑌 → ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) )
58	57	adantl	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) → ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) )
59	55 58	r19.29a	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌 ) → 𝑌 ∼ 𝑋 )