Theorem prjspnerlem

Description: A lemma showing that the equivalence relation used in prjspnval2 and the equivalence relation used in prjspval are equal, but only with the antecedent K e. DivRing . (Contributed by SN, 15-Jul-2023)

	Ref	Expression
Hypotheses	prjspnerlem.e	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
	prjspnerlem.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
	prjspnerlem.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
	prjspnerlem.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
	prjspnerlem.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion	prjspnerlem	⊢ ( 𝐾 ∈ DivRing → ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		prjspnerlem.e	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
2		prjspnerlem.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
3		prjspnerlem.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
4		prjspnerlem.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
5		prjspnerlem.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		ovex	⊢ ( 0 ... 𝑁 ) ∈ V
7	2	frlmsca	⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝐾 = ( Scalar ‘ 𝑊 ) )
8	6 7	mpan2	⊢ ( 𝐾 ∈ DivRing → 𝐾 = ( Scalar ‘ 𝑊 ) )
9	8	fveq2d	⊢ ( 𝐾 ∈ DivRing → ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
10	4 9	syl5eq	⊢ ( 𝐾 ∈ DivRing → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
11	10	rexeqdv	⊢ ( 𝐾 ∈ DivRing → ( ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ↔ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) )
12	11	anbi2d	⊢ ( 𝐾 ∈ DivRing → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) ) )
13	12	opabbidv	⊢ ( 𝐾 ∈ DivRing → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } )
14	1 13	syl5eq	⊢ ( 𝐾 ∈ DivRing → ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } )