Theorem prjsperref

Description: The relation in PrjSp is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023)

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

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		oveq1	⊢ ( 𝑚 = ( 1r ‘ 𝑆 ) → ( 𝑚 · 𝑋 ) = ( ( 1r ‘ 𝑆 ) · 𝑋 ) )
7	6	eqeq2d	⊢ ( 𝑚 = ( 1r ‘ 𝑆 ) → ( 𝑋 = ( 𝑚 · 𝑋 ) ↔ 𝑋 = ( ( 1r ‘ 𝑆 ) · 𝑋 ) ) )
8		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
9	3 5 8	lmod1cl	⊢ ( 𝑉 ∈ LMod → ( 1r ‘ 𝑆 ) ∈ 𝐾 )
10	9	adantr	⊢ ( ( 𝑉 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( 1r ‘ 𝑆 ) ∈ 𝐾 )
11		eldifi	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑋 ∈ ( Base ‘ 𝑉 ) )
12	11 2	eleq2s	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝑉 ) )
13		eqid	⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
14	13 3 4 8	lmodvs1	⊢ ( ( 𝑉 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑉 ) ) → ( ( 1r ‘ 𝑆 ) · 𝑋 ) = 𝑋 )
15	12 14	sylan2	⊢ ( ( 𝑉 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ( 1r ‘ 𝑆 ) · 𝑋 ) = 𝑋 )
16	15	eqcomd	⊢ ( ( 𝑉 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( ( 1r ‘ 𝑆 ) · 𝑋 ) )
17	7 10 16	rspcedvdw	⊢ ( ( 𝑉 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑋 ) )
18	17	ex	⊢ ( 𝑉 ∈ LMod → ( 𝑋 ∈ 𝐵 → ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑋 ) ) )
19	18	pm4.71d	⊢ ( 𝑉 ∈ LMod → ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑋 ) ) ) )
20		pm4.24	⊢ ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
21	20	anbi1i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑋 ) ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑋 ) ) )
22	1	prjsprel	⊢ ( 𝑋 ∼ 𝑋 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑋 ) ) )
23	21 22	bitr4i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑋 ) ) ↔ 𝑋 ∼ 𝑋 )
24	19 23	bitrdi	⊢ ( 𝑉 ∈ LMod → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∼ 𝑋 ) )