Theorem prjspval2

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

	Ref	Expression
Hypotheses	prjspval2.0	⊢ 0 = ( 0g ‘ 𝑉 )
	prjspval2.b	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { 0 } )
	prjspval2.n	⊢ 𝑁 = ( LSpan ‘ 𝑉 )
Assertion	prjspval2	⊢ ( 𝑉 ∈ LVec → ( ℙ𝕣𝕠𝕛 ‘ 𝑉 ) = ∪ 𝑧 ∈ 𝐵 { ( ( 𝑁 ‘ { 𝑧 } ) ∖ { 0 } ) } )

Proof

Step	Hyp	Ref	Expression
1		prjspval2.0	⊢ 0 = ( 0g ‘ 𝑉 )
2		prjspval2.b	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { 0 } )
3		prjspval2.n	⊢ 𝑁 = ( LSpan ‘ 𝑉 )
4	1	sneqi	⊢ { 0 } = { ( 0g ‘ 𝑉 ) }
5	4	difeq2i	⊢ ( ( Base ‘ 𝑉 ) ∖ { 0 } ) = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
6	2 5	eqtri	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
7		eqid	⊢ ( ·𝑠 ‘ 𝑉 ) = ( ·𝑠 ‘ 𝑉 )
8		eqid	⊢ ( Scalar ‘ 𝑉 ) = ( Scalar ‘ 𝑉 )
9		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑉 ) ) = ( Base ‘ ( Scalar ‘ 𝑉 ) )
10	6 7 8 9	prjspval	⊢ ( 𝑉 ∈ LVec → ( ℙ𝕣𝕠𝕛 ‘ 𝑉 ) = ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) } ) )
11		dfqs3	⊢ ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) } ) = ∪ 𝑧 ∈ 𝐵 { [ 𝑧 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) } }
12	11	a1i	⊢ ( 𝑉 ∈ LVec → ( 𝐵 / { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) } ) = ∪ 𝑧 ∈ 𝐵 { [ 𝑧 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) } } )
13		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) }
14	13 6 8 7 9 3	prjspeclsp	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑧 ∈ 𝐵 ) → [ 𝑧 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) } = ( ( 𝑁 ‘ { 𝑧 } ) ∖ { ( 0g ‘ 𝑉 ) } ) )
15	4	difeq2i	⊢ ( ( 𝑁 ‘ { 𝑧 } ) ∖ { 0 } ) = ( ( 𝑁 ‘ { 𝑧 } ) ∖ { ( 0g ‘ 𝑉 ) } )
16	14 15	eqtr4di	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑧 ∈ 𝐵 ) → [ 𝑧 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) } = ( ( 𝑁 ‘ { 𝑧 } ) ∖ { 0 } ) )
17	16	sneqd	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑧 ∈ 𝐵 ) → { [ 𝑧 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) } } = { ( ( 𝑁 ‘ { 𝑧 } ) ∖ { 0 } ) } )
18	17	iuneq2dv	⊢ ( 𝑉 ∈ LVec → ∪ 𝑧 ∈ 𝐵 { [ 𝑧 ] { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑉 ) 𝑦 ) ) } } = ∪ 𝑧 ∈ 𝐵 { ( ( 𝑁 ‘ { 𝑧 } ) ∖ { 0 } ) } )
19	10 12 18	3eqtrd	⊢ ( 𝑉 ∈ LVec → ( ℙ𝕣𝕠𝕛 ‘ 𝑉 ) = ∪ 𝑧 ∈ 𝐵 { ( ( 𝑁 ‘ { 𝑧 } ) ∖ { 0 } ) } )