Metamath Proof Explorer

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 𝐾 ) = ( 𝐵 / ∼ ) )