Metamath Proof Explorer

Theorem prjspnnorm

Description: In a free module, two nonzero vectors are equivalent iff they have the same normalized representative. (Contributed by SN, 24-Sep-2026)

Ref Expression
Hypotheses prjspnnorm.e 
|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
prjspnnorm.j 
|- J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
prjspnnorm.f 
|- F = ( v e. B |-> ( ( I ` ( v ` ( J ` v ) ) ) .x. v ) )
prjspnnorm.w 
|- W = ( K freeLMod ( 0 ... N ) )
prjspnnorm.b 
|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
prjspnnorm.s 
|- S = ( Base ` K )
prjspnnorm.i 
|- I = ( invr ` K )
prjspnnorm.t 
|- .x. = ( .s ` W )
prjspnnorm.k 
|- ( ph -> K e. DivRing )
prjspnnorm.n 
|- ( ph -> N e. NN0 )
prjspnnorm.x 
|- ( ph -> X e. B )
prjspnnorm.y 
|- ( ph -> Y e. B )
Assertion prjspnnorm 
|- ( ph -> ( X .~ Y <-> ( F ` X ) = ( F ` Y ) ) )

Proof

Step Hyp Ref Expression
1 prjspnnorm.e 
 |-  .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
2 prjspnnorm.j 
 |-  J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
3 prjspnnorm.f 
 |-  F = ( v e. B |-> ( ( I ` ( v ` ( J ` v ) ) ) .x. v ) )
4 prjspnnorm.w 
 |-  W = ( K freeLMod ( 0 ... N ) )
5 prjspnnorm.b 
 |-  B = ( ( Base ` W ) \ { ( 0g ` W ) } )
6 prjspnnorm.s 
 |-  S = ( Base ` K )
7 prjspnnorm.i 
 |-  I = ( invr ` K )
8 prjspnnorm.t 
 |-  .x. = ( .s ` W )
9 prjspnnorm.k 
 |-  ( ph -> K e. DivRing )
10 prjspnnorm.n 
 |-  ( ph -> N e. NN0 )
11 prjspnnorm.x 
 |-  ( ph -> X e. B )
12 prjspnnorm.y 
 |-  ( ph -> Y e. B )
13 ovexd 
 |-  ( ph -> ( 0 ... N ) e. _V )
14 4 frlmsca 
 |-  ( ( K e. DivRing /\ ( 0 ... N ) e. _V ) -> K = ( Scalar ` W ) )
15 9 13 14 syl2anc 
 |-  ( ph -> K = ( Scalar ` W ) )
16 15 fveq2d 
 |-  ( ph -> ( Base ` K ) = ( Base ` ( Scalar ` W ) ) )
17 6 16 eqtrid 
 |-  ( ph -> S = ( Base ` ( Scalar ` W ) ) )
18 17 rexeqdv 
 |-  ( ph -> ( E. l e. S x = ( l .x. y ) <-> E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) )
19 18 anbi2d 
 |-  ( ph -> ( ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) <-> ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) ) )
20 19 opabbidv 
 |-  ( ph -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } )
21 1 20 eqtrid 
 |-  ( ph -> .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } )
22 21 breqd 
 |-  ( ph -> ( X .~ Y <-> X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } Y ) )
23 4 frlmlvec 
 |-  ( ( K e. DivRing /\ ( 0 ... N ) e. _V ) -> W e. LVec )
24 9 13 23 syl2anc 
 |-  ( ph -> W e. LVec )
25 eqid 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) }
26 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
27 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
28 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
29 25 5 26 8 27 28 prjspreln0 
 |-  ( W e. LVec -> ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) X = ( m .x. Y ) ) ) )
30 24 29 syl 
 |-  ( ph -> ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. ( Base ` ( Scalar ` W ) ) x = ( l .x. y ) ) } Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) X = ( m .x. Y ) ) ) )
31 22 30 bitrd 
 |-  ( ph -> ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) X = ( m .x. Y ) ) ) )
32 31 simplbda 
 |-  ( ( ph /\ X .~ Y ) -> E. m e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) X = ( m .x. Y ) )
33 eldifsn 
 |-  ( m e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) <-> ( m e. ( Base ` ( Scalar ` W ) ) /\ m =/= ( 0g ` ( Scalar ` W ) ) ) )
34 17 eqcomd 
 |-  ( ph -> ( Base ` ( Scalar ` W ) ) = S )
35 34 eleq2d 
 |-  ( ph -> ( m e. ( Base ` ( Scalar ` W ) ) <-> m e. S ) )
36 15 eqcomd 
 |-  ( ph -> ( Scalar ` W ) = K )
37 36 fveq2d 
 |-  ( ph -> ( 0g ` ( Scalar ` W ) ) = ( 0g ` K ) )
38 37 neeq2d 
 |-  ( ph -> ( m =/= ( 0g ` ( Scalar ` W ) ) <-> m =/= ( 0g ` K ) ) )
39 35 38 anbi12d 
 |-  ( ph -> ( ( m e. ( Base ` ( Scalar ` W ) ) /\ m =/= ( 0g ` ( Scalar ` W ) ) ) <-> ( m e. S /\ m =/= ( 0g ` K ) ) ) )
40 33 39 bitrid 
 |-  ( ph -> ( m e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) <-> ( m e. S /\ m =/= ( 0g ` K ) ) ) )
41 eqid 
 |-  ( Base ` W ) = ( Base ` W )
42 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
43 24 lveclmodd 
 |-  ( ph -> W e. LMod )
44 43 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> W e. LMod )
45 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
46 9 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> K e. DivRing )
47 9 drngringd 
 |-  ( ph -> K e. Ring )
48 47 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> K e. Ring )
49 10 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> N e. NN0 )
50 simprl 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> m e. S )
51 difss 
 |-  ( ( Base ` W ) \ { ( 0g ` W ) } ) C_ ( Base ` W )
52 5 51 eqsstri 
 |-  B C_ ( Base ` W )
53 52 12 sselid 
 |-  ( ph -> Y e. ( Base ` W ) )
54 53 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> Y e. ( Base ` W ) )
55 4 41 6 8 48 50 54 frlmvscl 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( m .x. Y ) e. ( Base ` W ) )
56 simprr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> m =/= ( 0g ` K ) )
57 15 fveq2d 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` ( Scalar ` W ) ) )
58 57 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( 0g ` K ) = ( 0g ` ( Scalar ` W ) ) )
59 56 58 neeqtrd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> m =/= ( 0g ` ( Scalar ` W ) ) )
60 12 5 eleqtrdi 
 |-  ( ph -> Y e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
61 60 eldifsnbd 
 |-  ( ph -> Y =/= ( 0g ` W ) )
62 61 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> Y =/= ( 0g ` W ) )
63 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
64 24 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> W e. LVec )
65 17 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> S = ( Base ` ( Scalar ` W ) ) )
66 50 65 eleqtrd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> m e. ( Base ` ( Scalar ` W ) ) )
67 41 8 26 27 28 63 64 66 54 lvecvsn0 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( m .x. Y ) =/= ( 0g ` W ) <-> ( m =/= ( 0g ` ( Scalar ` W ) ) /\ Y =/= ( 0g ` W ) ) ) )
68 59 62 67 mpbir2and 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( m .x. Y ) =/= ( 0g ` W ) )
69 55 68 eldifsnd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( m .x. Y ) e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
70 69 5 eleqtrrdi 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( m .x. Y ) e. B )
71 2 4 5 48 49 70 6 frlmnzcoordcl2 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) e. S )
72 2 4 5 48 49 70 frlmnzcoordn0 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) =/= ( 0g ` K ) )
73 6 45 7 46 71 72 drnginvrcld 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) e. S )
74 73 65 eleqtrd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) e. ( Base ` ( Scalar ` W ) ) )
75 41 26 8 27 42 44 74 66 54 lmodvsassd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) ( .r ` ( Scalar ` W ) ) m ) .x. Y ) = ( ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) .x. ( m .x. Y ) ) )
76 36 fveq2d 
 |-  ( ph -> ( .r ` ( Scalar ` W ) ) = ( .r ` K ) )
77 76 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( .r ` ( Scalar ` W ) ) = ( .r ` K ) )
78 12 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> Y e. B )
79 2 4 5 8 45 6 46 49 78 50 56 frlmnzcoordsca 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( J ` ( m .x. Y ) ) = ( J ` Y ) )
80 79 fveq2d 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) = ( ( m .x. Y ) ` ( J ` Y ) ) )
81 ovexd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( 0 ... N ) e. _V )
82 2 4 5 47 10 12 frlmnzcoordcl 
 |-  ( ph -> ( J ` Y ) e. ( 0 ... N ) )
83 82 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( J ` Y ) e. ( 0 ... N ) )
84 eqid 
 |-  ( .r ` K ) = ( .r ` K )
85 4 41 6 81 50 54 83 8 84 frlmvscaval 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( m .x. Y ) ` ( J ` Y ) ) = ( m ( .r ` K ) ( Y ` ( J ` Y ) ) ) )
86 80 85 eqtrd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) = ( m ( .r ` K ) ( Y ` ( J ` Y ) ) ) )
87 86 fveq2d 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) = ( I ` ( m ( .r ` K ) ( Y ` ( J ` Y ) ) ) ) )
88 2 4 5 47 10 12 6 frlmnzcoordcl2 
 |-  ( ph -> ( Y ` ( J ` Y ) ) e. S )
89 88 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( Y ` ( J ` Y ) ) e. S )
90 2 4 5 47 10 12 frlmnzcoordn0 
 |-  ( ph -> ( Y ` ( J ` Y ) ) =/= ( 0g ` K ) )
91 90 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( Y ` ( J ` Y ) ) =/= ( 0g ` K ) )
92 6 45 84 7 46 50 89 56 91 drnginvmuld 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( I ` ( m ( .r ` K ) ( Y ` ( J ` Y ) ) ) ) = ( ( I ` ( Y ` ( J ` Y ) ) ) ( .r ` K ) ( I ` m ) ) )
93 87 92 eqtrd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) = ( ( I ` ( Y ` ( J ` Y ) ) ) ( .r ` K ) ( I ` m ) ) )
94 eqidd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> m = m )
95 77 93 94 oveq123d 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) ( .r ` ( Scalar ` W ) ) m ) = ( ( ( I ` ( Y ` ( J ` Y ) ) ) ( .r ` K ) ( I ` m ) ) ( .r ` K ) m ) )
96 6 45 7 9 88 90 drnginvrcld 
 |-  ( ph -> ( I ` ( Y ` ( J ` Y ) ) ) e. S )
97 96 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( I ` ( Y ` ( J ` Y ) ) ) e. S )
98 6 45 7 46 50 56 drnginvrcld 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( I ` m ) e. S )
99 6 84 48 97 98 50 ringassd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( ( I ` ( Y ` ( J ` Y ) ) ) ( .r ` K ) ( I ` m ) ) ( .r ` K ) m ) = ( ( I ` ( Y ` ( J ` Y ) ) ) ( .r ` K ) ( ( I ` m ) ( .r ` K ) m ) ) )
100 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
101 6 45 84 100 7 46 50 56 drnginvrld 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( I ` m ) ( .r ` K ) m ) = ( 1r ` K ) )
102 101 oveq2d 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( I ` ( Y ` ( J ` Y ) ) ) ( .r ` K ) ( ( I ` m ) ( .r ` K ) m ) ) = ( ( I ` ( Y ` ( J ` Y ) ) ) ( .r ` K ) ( 1r ` K ) ) )
103 6 84 100 48 97 ringridmd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( I ` ( Y ` ( J ` Y ) ) ) ( .r ` K ) ( 1r ` K ) ) = ( I ` ( Y ` ( J ` Y ) ) ) )
104 102 103 eqtrd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( I ` ( Y ` ( J ` Y ) ) ) ( .r ` K ) ( ( I ` m ) ( .r ` K ) m ) ) = ( I ` ( Y ` ( J ` Y ) ) ) )
105 95 99 104 3eqtrd 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) ( .r ` ( Scalar ` W ) ) m ) = ( I ` ( Y ` ( J ` Y ) ) ) )
106 105 oveq1d 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) ( .r ` ( Scalar ` W ) ) m ) .x. Y ) = ( ( I ` ( Y ` ( J ` Y ) ) ) .x. Y ) )
107 75 106 eqtr3d 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) .x. ( m .x. Y ) ) = ( ( I ` ( Y ` ( J ` Y ) ) ) .x. Y ) )
108 3 70 prjspnnormval 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( F ` ( m .x. Y ) ) = ( ( I ` ( ( m .x. Y ) ` ( J ` ( m .x. Y ) ) ) ) .x. ( m .x. Y ) ) )
109 3 12 prjspnnormval 
 |-  ( ph -> ( F ` Y ) = ( ( I ` ( Y ` ( J ` Y ) ) ) .x. Y ) )
110 109 adantr 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( F ` Y ) = ( ( I ` ( Y ` ( J ` Y ) ) ) .x. Y ) )
111 107 108 110 3eqtr4d 
 |-  ( ( ph /\ ( m e. S /\ m =/= ( 0g ` K ) ) ) -> ( F ` ( m .x. Y ) ) = ( F ` Y ) )
112 40 111 sylbida 
 |-  ( ( ph /\ m e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( F ` ( m .x. Y ) ) = ( F ` Y ) )
113 fveqeq2 
 |-  ( X = ( m .x. Y ) -> ( ( F ` X ) = ( F ` Y ) <-> ( F ` ( m .x. Y ) ) = ( F ` Y ) ) )
114 112 113 syl5ibrcom 
 |-  ( ( ph /\ m e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( X = ( m .x. Y ) -> ( F ` X ) = ( F ` Y ) ) )
115 114 impr 
 |-  ( ( ph /\ ( m e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) /\ X = ( m .x. Y ) ) ) -> ( F ` X ) = ( F ` Y ) )
116 115 adantlr 
 |-  ( ( ( ph /\ X .~ Y ) /\ ( m e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) /\ X = ( m .x. Y ) ) ) -> ( F ` X ) = ( F ` Y ) )
117 32 116 rexlimddv 
 |-  ( ( ph /\ X .~ Y ) -> ( F ` X ) = ( F ` Y ) )
118 1 4 5 6 8 9 prjspner 
 |-  ( ph -> .~ Er B )
119 118 adantr 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> .~ Er B )
120 1 2 3 4 5 6 7 8 9 10 11 prjspnequivnorm 
 |-  ( ph -> X .~ ( F ` X ) )
121 120 adantr 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> X .~ ( F ` X ) )
122 1 2 3 4 5 6 7 8 9 10 12 prjspnequivnorm 
 |-  ( ph -> Y .~ ( F ` Y ) )
123 122 adantr 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> Y .~ ( F ` Y ) )
124 simpr 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> ( F ` X ) = ( F ` Y ) )
125 123 124 breqtrrd 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> Y .~ ( F ` X ) )
126 119 121 125 ertr4d 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> X .~ Y )
127 117 126 impbida 
 |-  ( ph -> ( X .~ Y <-> ( F ` X ) = ( F ` Y ) ) )