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