Metamath Proof Explorer

Theorem prjspval

Description: Value of the projective space function, which is also known as the projectivization of V . (Contributed by Steven Nguyen, 29-Apr-2023)

Ref Expression
Hypotheses prjspval.b ⊢ B = Base V ∖ 0 V
prjspval.x ⊢ · ˙ = ⋅ V
prjspval.s ⊢ S = Scalar ⁡ V
prjspval.k ⊢ K = Base S
Assertion prjspval ⊢ V ∈ LVec → ℙ𝕣𝕠𝕛 ⁡ V = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y

Proof

Step Hyp Ref Expression
1 prjspval.b ⊢ B = Base V ∖ 0 V
2 prjspval.x ⊢ · ˙ = ⋅ V
3 prjspval.s ⊢ S = Scalar ⁡ V
4 prjspval.k ⊢ K = Base S
5 fvex ⊢ Base v ∈ V
6 5 difexi ⊢ Base v ∖ 0 v ∈ V
7 6 a1i ⊢ v = V → Base v ∖ 0 v ∈ V
8 fveq2 ⊢ v = V → Base v = Base V
9 fveq2 ⊢ v = V → 0 v = 0 V
10 9 sneqd ⊢ v = V → 0 v = 0 V
11 8 10 difeq12d ⊢ v = V → Base v ∖ 0 v = Base V ∖ 0 V
12 11 1 eqtr4di ⊢ v = V → Base v ∖ 0 v = B
13 12 eqeq2d ⊢ v = V → b = Base v ∖ 0 v ↔ b = B
14 13 biimpd ⊢ v = V → b = Base v ∖ 0 v → b = B
15 14 imp ⊢ v = V ∧ b = Base v ∖ 0 v → b = B
16 14 imdistani ⊢ v = V ∧ b = Base v ∖ 0 v → v = V ∧ b = B
17 eleq2 ⊢ b = B → x ∈ b ↔ x ∈ B
18 eleq2 ⊢ b = B → y ∈ b ↔ y ∈ B
19 17 18 anbi12d ⊢ b = B → x ∈ b ∧ y ∈ b ↔ x ∈ B ∧ y ∈ B
20 fveq2 ⊢ v = V → Scalar ⁡ v = Scalar ⁡ V
21 20 3 eqtr4di ⊢ v = V → Scalar ⁡ v = S
22 21 fveq2d ⊢ v = V → Base Scalar ⁡ v = Base S
23 22 4 eqtr4di ⊢ v = V → Base Scalar ⁡ v = K
24 fveq2 ⊢ v = V → ⋅ v = ⋅ V
25 24 2 eqtr4di ⊢ v = V → ⋅ v = · ˙
26 25 oveqd ⊢ v = V → l ⋅ v y = l · ˙ y
27 26 eqeq2d ⊢ v = V → x = l ⋅ v y ↔ x = l · ˙ y
28 23 27 rexeqbidv ⊢ v = V → ∃ l ∈ Base Scalar ⁡ v x = l ⋅ v y ↔ ∃ l ∈ K x = l · ˙ y
29 19 28 bi2anan9r ⊢ v = V ∧ b = B → x ∈ b ∧ y ∈ b ∧ ∃ l ∈ Base Scalar ⁡ v x = l ⋅ v y ↔ x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y
30 16 29 syl ⊢ v = V ∧ b = Base v ∖ 0 v → x ∈ b ∧ y ∈ b ∧ ∃ l ∈ Base Scalar ⁡ v x = l ⋅ v y ↔ x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y
31 30 opabbidv ⊢ v = V ∧ b = Base v ∖ 0 v → x y | x ∈ b ∧ y ∈ b ∧ ∃ l ∈ Base Scalar ⁡ v x = l ⋅ v y = x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y
32 15 31 qseq12d ⊢ v = V ∧ b = Base v ∖ 0 v → b / x y | x ∈ b ∧ y ∈ b ∧ ∃ l ∈ Base Scalar ⁡ v x = l ⋅ v y = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y
33 7 32 csbied ⊢ v = V → ⦋ Base v ∖ 0 v / b⦌ b / x y | x ∈ b ∧ y ∈ b ∧ ∃ l ∈ Base Scalar ⁡ v x = l ⋅ v y = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y
34 df-prjsp ⊢ ℙ𝕣𝕠𝕛 = v ∈ LVec ⟼ ⦋ Base v ∖ 0 v / b⦌ b / x y | x ∈ b ∧ y ∈ b ∧ ∃ l ∈ Base Scalar ⁡ v x = l ⋅ v y
35 fvex ⊢ Base V ∈ V
36 35 difexi ⊢ Base V ∖ 0 V ∈ V
37 1 36 eqeltri ⊢ B ∈ V
38 37 qsex ⊢ B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y ∈ V
39 33 34 38 fvmpt ⊢ V ∈ LVec → ℙ𝕣𝕠𝕛 ⁡ V = B / x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y