Theorem prjsprel

Description: Utility theorem regarding the relation used in PrjSp . (Contributed by Steven Nguyen, 29-Apr-2023)

	Ref	Expression
Hypothesis	prjsprel.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
Assertion	prjsprel	⊢ ( 𝑋 ∼ 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prjsprel.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
2		simpll	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ∧ 𝑙 = 𝑚 ) → 𝑥 = 𝑋 )
3		simpr	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ∧ 𝑙 = 𝑚 ) → 𝑙 = 𝑚 )
4		simplr	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ∧ 𝑙 = 𝑚 ) → 𝑦 = 𝑌 )
5	3 4	oveq12d	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ∧ 𝑙 = 𝑚 ) → ( 𝑙 · 𝑦 ) = ( 𝑚 · 𝑌 ) )
6	2 5	eqeq12d	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ∧ 𝑙 = 𝑚 ) → ( 𝑥 = ( 𝑙 · 𝑦 ) ↔ 𝑋 = ( 𝑚 · 𝑌 ) ) )
7	6	cbvrexdva	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ↔ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) )
8	7 1	brab2a	⊢ ( 𝑋 ∼ 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) )