Metamath Proof Explorer

Theorem prjspval2

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

Ref Expression
Hypotheses prjspval2.0 
|- .0. = ( 0g ` V )
prjspval2.b 
|- B = ( ( Base ` V ) \ { .0. } )
prjspval2.n 
|- N = ( LSpan ` V )
Assertion prjspval2 
|- ( V e. LVec -> ( PrjSp ` V ) = U_ z e. B { ( ( N ` { z } ) \ { .0. } ) } )

Proof

Step Hyp Ref Expression
1 prjspval2.0 
 |-  .0. = ( 0g ` V )
2 prjspval2.b 
 |-  B = ( ( Base ` V ) \ { .0. } )
3 prjspval2.n 
 |-  N = ( LSpan ` V )
4 1 sneqi 
 |-  { .0. } = { ( 0g ` V ) }
5 4 difeq2i 
 |-  ( ( Base ` V ) \ { .0. } ) = ( ( Base ` V ) \ { ( 0g ` V ) } )
6 2 5 eqtri 
 |-  B = ( ( Base ` V ) \ { ( 0g ` V ) } )
7 eqid 
 |-  ( .s ` V ) = ( .s ` V )
8 eqid 
 |-  ( Scalar ` V ) = ( Scalar ` V )
9 eqid 
 |-  ( Base ` ( Scalar ` V ) ) = ( Base ` ( Scalar ` V ) )
10 6 7 8 9 prjspval 
 |-  ( V e. LVec -> ( PrjSp ` V ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) } ) )
11 dfqs3 
 |-  ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) } ) = U_ z e. B { [ z ] { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) } }
12 11 a1i 
 |-  ( V e. LVec -> ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) } ) = U_ z e. B { [ z ] { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) } } )
13 eqid 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) }
14 13 6 8 7 9 3 prjspeclsp 
 |-  ( ( V e. LVec /\ z e. B ) -> [ z ] { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) } = ( ( N ` { z } ) \ { ( 0g ` V ) } ) )
15 4 difeq2i 
 |-  ( ( N ` { z } ) \ { .0. } ) = ( ( N ` { z } ) \ { ( 0g ` V ) } )
16 14 15 eqtr4di 
 |-  ( ( V e. LVec /\ z e. B ) -> [ z ] { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) } = ( ( N ` { z } ) \ { .0. } ) )
17 16 sneqd 
 |-  ( ( V e. LVec /\ z e. B ) -> { [ z ] { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) } } = { ( ( N ` { z } ) \ { .0. } ) } )
18 17 iuneq2dv 
 |-  ( V e. LVec -> U_ z e. B { [ z ] { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` V ) ) x = ( l ( .s ` V ) y ) ) } } = U_ z e. B { ( ( N ` { z } ) \ { .0. } ) } )
19 10 12 18 3eqtrd 
 |-  ( V e. LVec -> ( PrjSp ` V ) = U_ z e. B { ( ( N ` { z } ) \ { .0. } ) } )