Metamath Proof Explorer


Theorem prjspval2

Description: Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023)

Ref Expression
Hypotheses prjspval2.0 0 ˙ = 0 V
prjspval2.b B = Base V 0 ˙
prjspval2.n N = LSpan V
Assertion prjspval2 V LVec ℙ𝕣𝕠𝕛 V = z B N z 0 ˙

Proof

Step Hyp Ref Expression
1 prjspval2.0 0 ˙ = 0 V
2 prjspval2.b B = Base V 0 ˙
3 prjspval2.n N = LSpan V
4 1 sneqi 0 ˙ = 0 V
5 4 difeq2i Base V 0 ˙ = Base V 0 V
6 2 5 eqtri B = Base V 0 V
7 eqid V = V
8 eqid Scalar V = Scalar V
9 eqid Base Scalar V = Base Scalar V
10 6 7 8 9 prjspval V LVec ℙ𝕣𝕠𝕛 V = B / x y | x B y B l Base Scalar V x = l V y
11 dfqs3 B / x y | x B y B l Base Scalar V x = l V y = z B z x y | x B y B l Base Scalar V x = l V y
12 11 a1i V LVec B / x y | x B y B l Base Scalar V x = l V y = z B z x y | x B y B l Base Scalar V x = l V y
13 eqid x y | x B y B l Base Scalar V x = l V y = x y | x B y B l Base Scalar V x = l V y
14 13 6 8 7 9 3 prjspeclsp V LVec z B z x y | x B y B l Base Scalar V x = l V y = N z 0 V
15 4 difeq2i N z 0 ˙ = N z 0 V
16 14 15 eqtr4di V LVec z B z x y | x B y B l Base Scalar V x = l V y = N z 0 ˙
17 16 sneqd V LVec z B z x y | x B y B l Base Scalar V x = l V y = N z 0 ˙
18 17 iuneq2dv V LVec z B z x y | x B y B l Base Scalar V x = l V y = z B N z 0 ˙
19 10 12 18 3eqtrd V LVec ℙ𝕣𝕠𝕛 V = z B N z 0 ˙