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 ˙ = x y | x B y B l S x = l · ˙ y
prjspnval2.w W = K freeLMod 0 N
prjspnval2.b B = Base W 0 W
prjspnval2.s S = Base K
prjspnval2.x · ˙ = W
Assertion prjspnval2 N 0 K DivRing N ℙ𝕣𝕠𝕛 n K = B / ˙

Proof

Step Hyp Ref Expression
1 prjspnval2.e ˙ = x y | x B y B l S x = l · ˙ y
2 prjspnval2.w W = K freeLMod 0 N
3 prjspnval2.b B = Base W 0 W
4 prjspnval2.s S = Base K
5 prjspnval2.x · ˙ = W
6 prjspnval N 0 K DivRing N ℙ𝕣𝕠𝕛 n K = ℙ𝕣𝕠𝕛 K freeLMod 0 N
7 2 fveq2i ℙ𝕣𝕠𝕛 W = ℙ𝕣𝕠𝕛 K freeLMod 0 N
8 ovex 0 N V
9 2 frlmlvec K DivRing 0 N V W LVec
10 8 9 mpan2 K DivRing W LVec
11 eqid Scalar W = Scalar W
12 eqid Base Scalar W = Base Scalar W
13 3 5 11 12 prjspval W LVec ℙ𝕣𝕠𝕛 W = B / x y | x B y B l Base Scalar W x = l · ˙ y
14 10 13 syl K DivRing ℙ𝕣𝕠𝕛 W = B / x y | x B y B l Base Scalar W x = l · ˙ y
15 1 2 3 4 5 prjspnerlem K DivRing ˙ = x y | x B y B l Base Scalar W x = l · ˙ y
16 15 qseq2d K DivRing B / ˙ = B / x y | x B y B l Base Scalar W x = l · ˙ y
17 14 16 eqtr4d K DivRing ℙ𝕣𝕠𝕛 W = B / ˙
18 7 17 eqtr3id K DivRing ℙ𝕣𝕠𝕛 K freeLMod 0 N = B / ˙
19 18 adantl N 0 K DivRing ℙ𝕣𝕠𝕛 K freeLMod 0 N = B / ˙
20 6 19 eqtrd N 0 K DivRing N ℙ𝕣𝕠𝕛 n K = B / ˙