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