Metamath Proof Explorer

Theorem prjspnval2

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

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