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 ) \ { ( 0g ` V ) } )
prjspval.x 
|- .x. = ( .s ` V )
prjspval.s 
|- S = ( Scalar ` V )
prjspval.k 
|- K = ( Base ` S )
Assertion prjspval 
|- ( V e. LVec -> ( PrjSp ` V ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } ) )

Proof

Step Hyp Ref Expression
1 prjspval.b 
 |-  B = ( ( Base ` V ) \ { ( 0g ` V ) } )
2 prjspval.x 
 |-  .x. = ( .s ` V )
3 prjspval.s 
 |-  S = ( Scalar ` V )
4 prjspval.k 
 |-  K = ( Base ` S )
5 fvex 
 |-  ( Base ` v ) e. _V
6 5 difexi 
 |-  ( ( Base ` v ) \ { ( 0g ` v ) } ) e. _V
7 6 a1i 
 |-  ( v = V -> ( ( Base ` v ) \ { ( 0g ` v ) } ) e. _V )
8 fveq2 
 |-  ( v = V -> ( Base ` v ) = ( Base ` V ) )
9 fveq2 
 |-  ( v = V -> ( 0g ` v ) = ( 0g ` V ) )
10 9 sneqd 
 |-  ( v = V -> { ( 0g ` v ) } = { ( 0g ` V ) } )
11 8 10 difeq12d 
 |-  ( v = V -> ( ( Base ` v ) \ { ( 0g ` v ) } ) = ( ( Base ` V ) \ { ( 0g ` V ) } ) )
12 11 1 eqtr4di 
 |-  ( v = V -> ( ( Base ` v ) \ { ( 0g ` v ) } ) = B )
13 12 eqeq2d 
 |-  ( v = V -> ( b = ( ( Base ` v ) \ { ( 0g ` v ) } ) <-> b = B ) )
14 13 biimpd 
 |-  ( v = V -> ( b = ( ( Base ` v ) \ { ( 0g ` v ) } ) -> b = B ) )
15 14 imp 
 |-  ( ( v = V /\ b = ( ( Base ` v ) \ { ( 0g ` v ) } ) ) -> b = B )
16 14 imdistani 
 |-  ( ( v = V /\ b = ( ( Base ` v ) \ { ( 0g ` v ) } ) ) -> ( v = V /\ b = B ) )
17 eleq2 
 |-  ( b = B -> ( x e. b <-> x e. B ) )
18 eleq2 
 |-  ( b = B -> ( y e. b <-> y e. B ) )
19 17 18 anbi12d 
 |-  ( b = B -> ( ( x e. b /\ y e. b ) <-> ( x e. B /\ y e. 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 -> ( .s ` v ) = ( .s ` V ) )
25 24 2 eqtr4di 
 |-  ( v = V -> ( .s ` v ) = .x. )
26 25 oveqd 
 |-  ( v = V -> ( l ( .s ` v ) y ) = ( l .x. y ) )
27 26 eqeq2d 
 |-  ( v = V -> ( x = ( l ( .s ` v ) y ) <-> x = ( l .x. y ) ) )
28 23 27 rexeqbidv 
 |-  ( v = V -> ( E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) <-> E. l e. K x = ( l .x. y ) ) )
29 19 28 bi2anan9r 
 |-  ( ( v = V /\ b = B ) -> ( ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) <-> ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) ) )
30 16 29 syl 
 |-  ( ( v = V /\ b = ( ( Base ` v ) \ { ( 0g ` v ) } ) ) -> ( ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) <-> ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) ) )
31 30 opabbidv 
 |-  ( ( v = V /\ b = ( ( Base ` v ) \ { ( 0g ` v ) } ) ) -> { <. 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. K x = ( l .x. y ) ) } )
32 15 31 qseq12d 
 |-  ( ( v = V /\ b = ( ( Base ` v ) \ { ( 0g ` v ) } ) ) -> ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } ) )
33 7 32 csbied 
 |-  ( v = V -> [_ ( ( Base ` v ) \ { ( 0g ` v ) } ) / b ]_ ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } ) )
34 df-prjsp 
 |-  PrjSp = ( v e. LVec |-> [_ ( ( Base ` v ) \ { ( 0g ` v ) } ) / b ]_ ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) )
35 fvex 
 |-  ( Base ` V ) e. _V
36 35 difexi 
 |-  ( ( Base ` V ) \ { ( 0g ` V ) } ) e. _V
37 1 36 eqeltri 
 |-  B e. _V
38 37 qsex 
 |-  ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } ) e. _V
39 33 34 38 fvmpt 
 |-  ( V e. LVec -> ( PrjSp ` V ) = ( B /. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } ) )