Theorem prjspnval2

Description: Value of the n-dimensional projective space function, expanded. (Contributed by Steven Nguyen, 15-Jul-2023)

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

Proof

Step	Hyp	Ref	Expression
1		prjspnval2.e	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
2		prjspnval2.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
3		prjspnval2.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
4		prjspnval2.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
5		prjspnval2.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		prjspnval	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing ) → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
7	2	fveq2i	⊢ ( ℙ𝕣𝕠𝕛 ‘ 𝑊 ) = ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) )
8		ovex	⊢ ( 0 ... 𝑁 ) ∈ V
9	2	frlmlvec	⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝑊 ∈ LVec )
10	8 9	mpan2	⊢ ( 𝐾 ∈ DivRing → 𝑊 ∈ LVec )
11		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
13	3 5 11 12	prjspval	⊢ ( 𝑊 ∈ LVec → ( ℙ𝕣𝕠𝕛 ‘ 𝑊 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } ) )
14	10 13	syl	⊢ ( 𝐾 ∈ DivRing → ( ℙ𝕣𝕠𝕛 ‘ 𝑊 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } ) )
15	1 2 3 4 5	prjspnerlem	⊢ ( 𝐾 ∈ DivRing → ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } )
16	15	qseq2d	⊢ ( 𝐾 ∈ DivRing → ( 𝐵 / ∼ ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } ) )
17	14 16	eqtr4d	⊢ ( 𝐾 ∈ DivRing → ( ℙ𝕣𝕠𝕛 ‘ 𝑊 ) = ( 𝐵 / ∼ ) )
18	7 17	eqtr3id	⊢ ( 𝐾 ∈ DivRing → ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) = ( 𝐵 / ∼ ) )
19	18	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing ) → ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) = ( 𝐵 / ∼ ) )
20	6 19	eqtrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing ) → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ( 𝐵 / ∼ ) )