Metamath Proof Explorer

Theorem prjspner1

Description: Two vectors whose zeroth coordinate is nonzero are equivalent if and only if they have the same representative in the (n-1)-dimensional affine subspace { x_0 = 1 } . For example, vectors in 3D space whose x coordinate is nonzero are equivalent iff they intersect at the plane x = 1 at the same point (also see section header). (Contributed by SN, 13-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 prjspner01.e 
 |-  .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
2 prjspner01.f 
 |-  F = ( b e. B |-> if ( ( b ` 0 ) = .0. , b , ( ( I ` ( b ` 0 ) ) .x. b ) ) )
3 prjspner01.b 
 |-  B = ( ( Base ` W ) \ { ( 0g ` W ) } )
4 prjspner01.w 
 |-  W = ( K freeLMod ( 0 ... N ) )
5 prjspner01.t 
 |-  .x. = ( .s ` W )
6 prjspner01.s 
 |-  S = ( Base ` K )
7 prjspner01.0 
 |-  .0. = ( 0g ` K )
8 prjspner01.i 
 |-  I = ( invr ` K )
9 prjspner01.k 
 |-  ( ph -> K e. DivRing )
10 prjspner01.n 
 |-  ( ph -> N e. NN0 )
11 prjspner01.x 
 |-  ( ph -> X e. B )
12 prjspner1.y 
 |-  ( ph -> Y e. B )
13 prjspner1.1 
 |-  ( ph -> ( X ` 0 ) =/= .0. )
14 prjspner1.2 
 |-  ( ph -> ( Y ` 0 ) =/= .0. )
15 1 prjsprel 
 |-  ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) )
16 fveq1 
 |-  ( X = ( 0g ` W ) -> ( X ` 0 ) = ( ( 0g ` W ) ` 0 ) )
17 9 drngringd 
 |-  ( ph -> K e. Ring )
18 ovexd 
 |-  ( ph -> ( 0 ... N ) e. _V )
19 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
20 10 19 syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
21 4 7 17 18 20 frlm0vald 
 |-  ( ph -> ( ( 0g ` W ) ` 0 ) = .0. )
22 16 21 sylan9eqr 
 |-  ( ( ph /\ X = ( 0g ` W ) ) -> ( X ` 0 ) = .0. )
23 13 22 mteqand 
 |-  ( ph -> X =/= ( 0g ` W ) )
24 4 frlmsca 
 |-  ( ( K e. DivRing /\ ( 0 ... N ) e. _V ) -> K = ( Scalar ` W ) )
25 9 18 24 syl2anc 
 |-  ( ph -> K = ( Scalar ` W ) )
26 25 fveq2d 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` ( Scalar ` W ) ) )
27 7 26 eqtrid 
 |-  ( ph -> .0. = ( 0g ` ( Scalar ` W ) ) )
28 27 oveq1d 
 |-  ( ph -> ( .0. .x. Y ) = ( ( 0g ` ( Scalar ` W ) ) .x. Y ) )
29 4 frlmlvec 
 |-  ( ( K e. DivRing /\ ( 0 ... N ) e. _V ) -> W e. LVec )
30 9 18 29 syl2anc 
 |-  ( ph -> W e. LVec )
31 30 lveclmodd 
 |-  ( ph -> W e. LMod )
32 12 3 eleqtrdi 
 |-  ( ph -> Y e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
33 32 eldifad 
 |-  ( ph -> Y e. ( Base ` W ) )
34 eqid 
 |-  ( Base ` W ) = ( Base ` W )
35 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
36 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
37 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
38 34 35 5 36 37 lmod0vs 
 |-  ( ( W e. LMod /\ Y e. ( Base ` W ) ) -> ( ( 0g ` ( Scalar ` W ) ) .x. Y ) = ( 0g ` W ) )
39 31 33 38 syl2anc 
 |-  ( ph -> ( ( 0g ` ( Scalar ` W ) ) .x. Y ) = ( 0g ` W ) )
40 28 39 eqtrd 
 |-  ( ph -> ( .0. .x. Y ) = ( 0g ` W ) )
41 23 40 neeqtrrd 
 |-  ( ph -> X =/= ( .0. .x. Y ) )
42 41 ad2antrr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) -> X =/= ( .0. .x. Y ) )
43 oveq1 
 |-  ( m = .0. -> ( m .x. Y ) = ( .0. .x. Y ) )
44 43 neeq2d 
 |-  ( m = .0. -> ( X =/= ( m .x. Y ) <-> X =/= ( .0. .x. Y ) ) )
45 42 44 syl5ibrcom 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) -> ( m = .0. -> X =/= ( m .x. Y ) ) )
46 45 necon2d 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) -> ( X = ( m .x. Y ) -> m =/= .0. ) )
47 46 ancrd 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) -> ( X = ( m .x. Y ) -> ( m =/= .0. /\ X = ( m .x. Y ) ) ) )
48 ovexd 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( 0 ... N ) e. _V )
49 simplr 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> m e. S )
50 33 ad3antrrr 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> Y e. ( Base ` W ) )
51 20 ad3antrrr 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> 0 e. ( 0 ... N ) )
52 eqid 
 |-  ( .r ` K ) = ( .r ` K )
53 4 34 6 48 49 50 51 5 52 frlmvscaval 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( m .x. Y ) ` 0 ) = ( m ( .r ` K ) ( Y ` 0 ) ) )
54 53 fveq2d 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( I ` ( ( m .x. Y ) ` 0 ) ) = ( I ` ( m ( .r ` K ) ( Y ` 0 ) ) ) )
55 9 ad3antrrr 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> K e. DivRing )
56 4 6 34 frlmbasf 
 |-  ( ( ( 0 ... N ) e. _V /\ Y e. ( Base ` W ) ) -> Y : ( 0 ... N ) --> S )
57 18 33 56 syl2anc 
 |-  ( ph -> Y : ( 0 ... N ) --> S )
58 57 20 ffvelcdmd 
 |-  ( ph -> ( Y ` 0 ) e. S )
59 58 ad3antrrr 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( Y ` 0 ) e. S )
60 simpr 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> m =/= .0. )
61 14 ad3antrrr 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( Y ` 0 ) =/= .0. )
62 6 7 52 8 55 49 59 60 61 drnginvmuld 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( I ` ( m ( .r ` K ) ( Y ` 0 ) ) ) = ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) )
63 54 62 eqtrd 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( I ` ( ( m .x. Y ) ` 0 ) ) = ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) )
64 63 oveq1d 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( I ` ( ( m .x. Y ) ` 0 ) ) .x. ( m .x. Y ) ) = ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) .x. ( m .x. Y ) ) )
65 31 ad3antrrr 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> W e. LMod )
66 17 ad3antrrr 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> K e. Ring )
67 6 7 8 55 59 61 drnginvrcld 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( I ` ( Y ` 0 ) ) e. S )
68 6 7 8 55 49 60 drnginvrcld 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( I ` m ) e. S )
69 6 52 66 67 68 ringcld 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) e. S )
70 25 fveq2d 
 |-  ( ph -> ( Base ` K ) = ( Base ` ( Scalar ` W ) ) )
71 6 70 eqtrid 
 |-  ( ph -> S = ( Base ` ( Scalar ` W ) ) )
72 71 ad3antrrr 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> S = ( Base ` ( Scalar ` W ) ) )
73 69 72 eleqtrd 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) e. ( Base ` ( Scalar ` W ) ) )
74 49 72 eleqtrd 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> m e. ( Base ` ( Scalar ` W ) ) )
75 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
76 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
77 34 35 5 75 76 lmodvsass 
 |-  ( ( W e. LMod /\ ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) e. ( Base ` ( Scalar ` W ) ) /\ m e. ( Base ` ( Scalar ` W ) ) /\ Y e. ( Base ` W ) ) ) -> ( ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) ( .r ` ( Scalar ` W ) ) m ) .x. Y ) = ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) .x. ( m .x. Y ) ) )
78 65 73 74 50 77 syl13anc 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) ( .r ` ( Scalar ` W ) ) m ) .x. Y ) = ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) .x. ( m .x. Y ) ) )
79 6 52 66 67 68 49 ringassd 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) ( .r ` K ) m ) = ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( ( I ` m ) ( .r ` K ) m ) ) )
80 55 48 24 syl2anc 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> K = ( Scalar ` W ) )
81 80 fveq2d 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( .r ` K ) = ( .r ` ( Scalar ` W ) ) )
82 81 oveqd 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) ( .r ` K ) m ) = ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) ( .r ` ( Scalar ` W ) ) m ) )
83 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
84 6 7 52 83 8 55 49 60 drnginvrld 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( I ` m ) ( .r ` K ) m ) = ( 1r ` K ) )
85 84 oveq2d 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( ( I ` m ) ( .r ` K ) m ) ) = ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( 1r ` K ) ) )
86 6 52 83 66 67 ringridmd 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( 1r ` K ) ) = ( I ` ( Y ` 0 ) ) )
87 85 86 eqtrd 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( ( I ` m ) ( .r ` K ) m ) ) = ( I ` ( Y ` 0 ) ) )
88 79 82 87 3eqtr3d 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) ( .r ` ( Scalar ` W ) ) m ) = ( I ` ( Y ` 0 ) ) )
89 88 oveq1d 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( ( ( I ` ( Y ` 0 ) ) ( .r ` K ) ( I ` m ) ) ( .r ` ( Scalar ` W ) ) m ) .x. Y ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) )
90 64 78 89 3eqtr2d 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( ( I ` ( ( m .x. Y ) ` 0 ) ) .x. ( m .x. Y ) ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) )
91 fveq1 
 |-  ( X = ( m .x. Y ) -> ( X ` 0 ) = ( ( m .x. Y ) ` 0 ) )
92 91 fveq2d 
 |-  ( X = ( m .x. Y ) -> ( I ` ( X ` 0 ) ) = ( I ` ( ( m .x. Y ) ` 0 ) ) )
93 id 
 |-  ( X = ( m .x. Y ) -> X = ( m .x. Y ) )
94 92 93 oveq12d 
 |-  ( X = ( m .x. Y ) -> ( ( I ` ( X ` 0 ) ) .x. X ) = ( ( I ` ( ( m .x. Y ) ` 0 ) ) .x. ( m .x. Y ) ) )
95 94 eqeq1d 
 |-  ( X = ( m .x. Y ) -> ( ( ( I ` ( X ` 0 ) ) .x. X ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) <-> ( ( I ` ( ( m .x. Y ) ` 0 ) ) .x. ( m .x. Y ) ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) ) )
96 90 95 syl5ibrcom 
 |-  ( ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) /\ m =/= .0. ) -> ( X = ( m .x. Y ) -> ( ( I ` ( X ` 0 ) ) .x. X ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) ) )
97 96 expimpd 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) -> ( ( m =/= .0. /\ X = ( m .x. Y ) ) -> ( ( I ` ( X ` 0 ) ) .x. X ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) ) )
98 47 97 syld 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ m e. S ) -> ( X = ( m .x. Y ) -> ( ( I ` ( X ` 0 ) ) .x. X ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) ) )
99 98 rexlimdva 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( E. m e. S X = ( m .x. Y ) -> ( ( I ` ( X ` 0 ) ) .x. X ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) ) )
100 99 impr 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> ( ( I ` ( X ` 0 ) ) .x. X ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) )
101 13 neneqd 
 |-  ( ph -> -. ( X ` 0 ) = .0. )
102 101 iffalsed 
 |-  ( ph -> if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) = ( ( I ` ( X ` 0 ) ) .x. X ) )
103 102 adantr 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) = ( ( I ` ( X ` 0 ) ) .x. X ) )
104 14 neneqd 
 |-  ( ph -> -. ( Y ` 0 ) = .0. )
105 104 iffalsed 
 |-  ( ph -> if ( ( Y ` 0 ) = .0. , Y , ( ( I ` ( Y ` 0 ) ) .x. Y ) ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) )
106 105 adantr 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> if ( ( Y ` 0 ) = .0. , Y , ( ( I ` ( Y ` 0 ) ) .x. Y ) ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) )
107 100 103 106 3eqtr4d 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) = if ( ( Y ` 0 ) = .0. , Y , ( ( I ` ( Y ` 0 ) ) .x. Y ) ) )
108 fveq1 
 |-  ( b = X -> ( b ` 0 ) = ( X ` 0 ) )
109 108 eqeq1d 
 |-  ( b = X -> ( ( b ` 0 ) = .0. <-> ( X ` 0 ) = .0. ) )
110 id 
 |-  ( b = X -> b = X )
111 108 fveq2d 
 |-  ( b = X -> ( I ` ( b ` 0 ) ) = ( I ` ( X ` 0 ) ) )
112 111 110 oveq12d 
 |-  ( b = X -> ( ( I ` ( b ` 0 ) ) .x. b ) = ( ( I ` ( X ` 0 ) ) .x. X ) )
113 109 110 112 ifbieq12d 
 |-  ( b = X -> if ( ( b ` 0 ) = .0. , b , ( ( I ` ( b ` 0 ) ) .x. b ) ) = if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) )
114 simprll 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> X e. B )
115 ovexd 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> ( ( I ` ( X ` 0 ) ) .x. X ) e. _V )
116 114 115 ifexd 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) e. _V )
117 2 113 114 116 fvmptd3 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> ( F ` X ) = if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) )
118 fveq1 
 |-  ( b = Y -> ( b ` 0 ) = ( Y ` 0 ) )
119 118 eqeq1d 
 |-  ( b = Y -> ( ( b ` 0 ) = .0. <-> ( Y ` 0 ) = .0. ) )
120 id 
 |-  ( b = Y -> b = Y )
121 118 fveq2d 
 |-  ( b = Y -> ( I ` ( b ` 0 ) ) = ( I ` ( Y ` 0 ) ) )
122 121 120 oveq12d 
 |-  ( b = Y -> ( ( I ` ( b ` 0 ) ) .x. b ) = ( ( I ` ( Y ` 0 ) ) .x. Y ) )
123 119 120 122 ifbieq12d 
 |-  ( b = Y -> if ( ( b ` 0 ) = .0. , b , ( ( I ` ( b ` 0 ) ) .x. b ) ) = if ( ( Y ` 0 ) = .0. , Y , ( ( I ` ( Y ` 0 ) ) .x. Y ) ) )
124 simprlr 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> Y e. B )
125 ovexd 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> ( ( I ` ( Y ` 0 ) ) .x. Y ) e. _V )
126 124 125 ifexd 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> if ( ( Y ` 0 ) = .0. , Y , ( ( I ` ( Y ` 0 ) ) .x. Y ) ) e. _V )
127 2 123 124 126 fvmptd3 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> ( F ` Y ) = if ( ( Y ` 0 ) = .0. , Y , ( ( I ` ( Y ` 0 ) ) .x. Y ) ) )
128 107 117 127 3eqtr4d 
 |-  ( ( ph /\ ( ( X e. B /\ Y e. B ) /\ E. m e. S X = ( m .x. Y ) ) ) -> ( F ` X ) = ( F ` Y ) )
129 15 128 sylan2b 
 |-  ( ( ph /\ X .~ Y ) -> ( F ` X ) = ( F ` Y ) )
130 1 4 3 6 5 9 prjspner 
 |-  ( ph -> .~ Er B )
131 130 adantr 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> .~ Er B )
132 1 2 3 4 5 6 7 8 9 10 11 prjspner01 
 |-  ( ph -> X .~ ( F ` X ) )
133 132 adantr 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> X .~ ( F ` X ) )
134 130 132 ercl2 
 |-  ( ph -> ( F ` X ) e. B )
135 134 adantr 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> ( F ` X ) e. B )
136 131 135 erref 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> ( F ` X ) .~ ( F ` X ) )
137 breq2 
 |-  ( ( F ` X ) = ( F ` Y ) -> ( ( F ` X ) .~ ( F ` X ) <-> ( F ` X ) .~ ( F ` Y ) ) )
138 137 adantl 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> ( ( F ` X ) .~ ( F ` X ) <-> ( F ` X ) .~ ( F ` Y ) ) )
139 136 138 mpbid 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> ( F ` X ) .~ ( F ` Y ) )
140 1 2 3 4 5 6 7 8 9 10 12 prjspner01 
 |-  ( ph -> Y .~ ( F ` Y ) )
141 140 adantr 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> Y .~ ( F ` Y ) )
142 131 139 141 ertr4d 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> ( F ` X ) .~ Y )
143 131 133 142 ertrd 
 |-  ( ( ph /\ ( F ` X ) = ( F ` Y ) ) -> X .~ Y )
144 129 143 impbida 
 |-  ( ph -> ( X .~ Y <-> ( F ` X ) = ( F ` Y ) ) )