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 ˙