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	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
	prjspval.x	⊢ · = ( ·𝑠 ‘ 𝑉 )
	prjspval.s	⊢ 𝑆 = ( Scalar ‘ 𝑉 )
	prjspval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
Assertion	prjspval	⊢ ( 𝑉 ∈ LVec → ( ℙ𝕣𝕠𝕛 ‘ 𝑉 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		prjspval.b	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
2		prjspval.x	⊢ · = ( ·𝑠 ‘ 𝑉 )
3		prjspval.s	⊢ 𝑆 = ( Scalar ‘ 𝑉 )
4		prjspval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
5		fvex	⊢ ( Base ‘ 𝑣 ) ∈ V
6	5	difexi	⊢ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) ∈ V
7	6	a1i	⊢ ( 𝑣 = 𝑉 → ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) ∈ V )
8		fveq2	⊢ ( 𝑣 = 𝑉 → ( Base ‘ 𝑣 ) = ( Base ‘ 𝑉 ) )
9		fveq2	⊢ ( 𝑣 = 𝑉 → ( 0g ‘ 𝑣 ) = ( 0g ‘ 𝑉 ) )
10	9	sneqd	⊢ ( 𝑣 = 𝑉 → { ( 0g ‘ 𝑣 ) } = { ( 0g ‘ 𝑉 ) } )
11	8 10	difeq12d	⊢ ( 𝑣 = 𝑉 → ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) )
12	11 1	eqtr4di	⊢ ( 𝑣 = 𝑉 → ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) = 𝐵 )
13	12	eqeq2d	⊢ ( 𝑣 = 𝑉 → ( 𝑏 = ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) ↔ 𝑏 = 𝐵 ) )
14	13	biimpd	⊢ ( 𝑣 = 𝑉 → ( 𝑏 = ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) → 𝑏 = 𝐵 ) )
15	14	imp	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑏 = ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) ) → 𝑏 = 𝐵 )
16	14	imdistani	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑏 = ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) ) → ( 𝑣 = 𝑉 ∧ 𝑏 = 𝐵 ) )
17		eleq2	⊢ ( 𝑏 = 𝐵 → ( 𝑥 ∈ 𝑏 ↔ 𝑥 ∈ 𝐵 ) )
18		eleq2	⊢ ( 𝑏 = 𝐵 → ( 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝐵 ) )
19	17 18	anbi12d	⊢ ( 𝑏 = 𝐵 → ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
20		fveq2	⊢ ( 𝑣 = 𝑉 → ( Scalar ‘ 𝑣 ) = ( Scalar ‘ 𝑉 ) )
21	20 3	eqtr4di	⊢ ( 𝑣 = 𝑉 → ( Scalar ‘ 𝑣 ) = 𝑆 )
22	21	fveq2d	⊢ ( 𝑣 = 𝑉 → ( Base ‘ ( Scalar ‘ 𝑣 ) ) = ( Base ‘ 𝑆 ) )
23	22 4	eqtr4di	⊢ ( 𝑣 = 𝑉 → ( Base ‘ ( Scalar ‘ 𝑣 ) ) = 𝐾 )
24		fveq2	⊢ ( 𝑣 = 𝑉 → ( ·𝑠 ‘ 𝑣 ) = ( ·𝑠 ‘ 𝑉 ) )
25	24 2	eqtr4di	⊢ ( 𝑣 = 𝑉 → ( ·𝑠 ‘ 𝑣 ) = · )
26	25	oveqd	⊢ ( 𝑣 = 𝑉 → ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) = ( 𝑙 · 𝑦 ) )
27	26	eqeq2d	⊢ ( 𝑣 = 𝑉 → ( 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ↔ 𝑥 = ( 𝑙 · 𝑦 ) ) )
28	23 27	rexeqbidv	⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ↔ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) )
29	19 28	bi2anan9r	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ) )
30	16 29	syl	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑏 = ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) ) → ( ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) ) )
31	30	opabbidv	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑏 = ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } )
32	15 31	qseq12d	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑏 = ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) ) → ( 𝑏 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } ) )
33	7 32	csbied	⊢ ( 𝑣 = 𝑉 → ⦋ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) / 𝑏 ⦌ ( 𝑏 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } ) )
34		df-prjsp	⊢ ℙ𝕣𝕠𝕛 = ( 𝑣 ∈ LVec ↦ ⦋ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) / 𝑏 ⦌ ( 𝑏 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } ) )
35		fvex	⊢ ( Base ‘ 𝑉 ) ∈ V
36	35	difexi	⊢ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) ∈ V
37	1 36	eqeltri	⊢ 𝐵 ∈ V
38	37	qsex	⊢ ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } ) ∈ V
39	33 34 38	fvmpt	⊢ ( 𝑉 ∈ LVec → ( ℙ𝕣𝕠𝕛 ‘ 𝑉 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) } ) )