Metamath Proof Explorer

Theorem angmndaddov2

Description: Value of the addition operation in the angle addition monoid, in case the first angle is zero or flat. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses angmndadd.p 
|- P = ( Base ` G )
angmndadd.a 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
angmndadd.i 
|- I = ( Itv ` G )
angmndadd.d 
|- .- = ( dist ` G )
angmndadd.c 
|- .~ = ( cgrA ` G )
angmndadd.l 
|- L = ( LineG ` G )
angmndadd.g 
|- ( ph -> G e. TarskiG )
angmndaddov.u 
|- ( ph -> U e. P )
angmndaddov.v 
|- ( ph -> V e. P )
angmndaddov.w 
|- ( ph -> W e. P )
angmndaddov.x 
|- ( ph -> X e. P )
angmndaddov.y 
|- ( ph -> Y e. P )
angmndaddov.z 
|- ( ph -> Z e. P )
angmndaddeu.1 
|- ( ph -> U =/= V )
angmndaddeu.2 
|- ( ph -> V =/= W )
angmndaddeu.3 
|- ( ph -> X =/= Y )
angmndaddeu.4 
|- ( ph -> Y =/= Z )
angmndaddov.o 
|- .+ = ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) )
angmndaddov2.x 
|- ( ph -> X e. ( Y L Z ) )
angmndaddov2.s 
|- ( ph -> S e. P )
angmndaddov2.1 
|- ( ph -> <" W V S "> .~ <" X Y Z "> )
angmndaddov2.2 
|- ( ph -> ( V .- S ) = ( Y .- X ) )
Assertion angmndaddov2 
|- ( ph -> ( <" X Y Z "> .+ <" U V W "> ) = <" U V S "> )

Proof

Step Hyp Ref Expression
1 angmndadd.p 
 |-  P = ( Base ` G )
2 angmndadd.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 angmndadd.i 
 |-  I = ( Itv ` G )
4 angmndadd.d 
 |-  .- = ( dist ` G )
5 angmndadd.c 
 |-  .~ = ( cgrA ` G )
6 angmndadd.l 
 |-  L = ( LineG ` G )
7 angmndadd.g 
 |-  ( ph -> G e. TarskiG )
8 angmndaddov.u 
 |-  ( ph -> U e. P )
9 angmndaddov.v 
 |-  ( ph -> V e. P )
10 angmndaddov.w 
 |-  ( ph -> W e. P )
11 angmndaddov.x 
 |-  ( ph -> X e. P )
12 angmndaddov.y 
 |-  ( ph -> Y e. P )
13 angmndaddov.z 
 |-  ( ph -> Z e. P )
14 angmndaddeu.1 
 |-  ( ph -> U =/= V )
15 angmndaddeu.2 
 |-  ( ph -> V =/= W )
16 angmndaddeu.3 
 |-  ( ph -> X =/= Y )
17 angmndaddeu.4 
 |-  ( ph -> Y =/= Z )
18 angmndaddov.o 
 |-  .+ = ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) )
19 angmndaddov2.x 
 |-  ( ph -> X e. ( Y L Z ) )
20 angmndaddov2.s 
 |-  ( ph -> S e. P )
21 angmndaddov2.1 
 |-  ( ph -> <" W V S "> .~ <" X Y Z "> )
22 angmndaddov2.2 
 |-  ( ph -> ( V .- S ) = ( Y .- X ) )
23 18 a1i 
 |-  ( ph -> .+ = ( e e. A , f e. A |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) )
24 19 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> X e. ( Y L Z ) )
25 simplr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> e = <" X Y Z "> )
26 25 fveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 0 ) = ( <" X Y Z "> ` 0 ) )
27 s3fv0 
 |-  ( X e. P -> ( <" X Y Z "> ` 0 ) = X )
28 11 27 syl 
 |-  ( ph -> ( <" X Y Z "> ` 0 ) = X )
29 28 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" X Y Z "> ` 0 ) = X )
30 26 29 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 0 ) = X )
31 25 fveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 1 ) = ( <" X Y Z "> ` 1 ) )
32 s3fv1 
 |-  ( Y e. P -> ( <" X Y Z "> ` 1 ) = Y )
33 12 32 syl 
 |-  ( ph -> ( <" X Y Z "> ` 1 ) = Y )
34 33 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" X Y Z "> ` 1 ) = Y )
35 31 34 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 1 ) = Y )
36 25 fveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 2 ) = ( <" X Y Z "> ` 2 ) )
37 s3fv2 
 |-  ( Z e. P -> ( <" X Y Z "> ` 2 ) = Z )
38 13 37 syl 
 |-  ( ph -> ( <" X Y Z "> ` 2 ) = Z )
39 38 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" X Y Z "> ` 2 ) = Z )
40 36 39 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 2 ) = Z )
41 35 40 oveq12d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( e ` 1 ) L ( e ` 2 ) ) = ( Y L Z ) )
42 24 30 41 3eltr4d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) )
43 42 iftrued 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) = <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> )
44 simpr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> f = <" U V W "> )
45 44 fveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( f ` 0 ) = ( <" U V W "> ` 0 ) )
46 s3fv0 
 |-  ( U e. P -> ( <" U V W "> ` 0 ) = U )
47 8 46 syl 
 |-  ( ph -> ( <" U V W "> ` 0 ) = U )
48 47 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" U V W "> ` 0 ) = U )
49 45 48 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( f ` 0 ) = U )
50 44 fveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( f ` 1 ) = ( <" U V W "> ` 1 ) )
51 s3fv1 
 |-  ( V e. P -> ( <" U V W "> ` 1 ) = V )
52 9 51 syl 
 |-  ( ph -> ( <" U V W "> ` 1 ) = V )
53 52 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" U V W "> ` 1 ) = V )
54 50 53 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( f ` 1 ) = V )
55 20 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> S e. P )
56 7 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> G e. TarskiG )
57 10 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> W e. P )
58 9 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> V e. P )
59 11 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> X e. P )
60 12 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> Y e. P )
61 13 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> Z e. P )
62 15 necomd 
 |-  ( ph -> W =/= V )
63 62 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> W =/= V )
64 15 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> V =/= W )
65 16 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> X =/= Y )
66 17 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> Y =/= Z )
67 1 2 3 4 5 6 56 57 58 57 59 60 61 63 64 65 66 24 angmndaddov2lem 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) )
68 44 fveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( f ` 2 ) = ( <" U V W "> ` 2 ) )
69 s3fv2 
 |-  ( W e. P -> ( <" U V W "> ` 2 ) = W )
70 10 69 syl 
 |-  ( ph -> ( <" U V W "> ` 2 ) = W )
71 70 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" U V W "> ` 2 ) = W )
72 68 71 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( f ` 2 ) = W )
73 eqidd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> s = s )
74 72 54 73 s3eqd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> <" ( f ` 2 ) ( f ` 1 ) s "> = <" W V s "> )
75 74 25 breq12d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e <-> <" W V s "> .~ <" X Y Z "> ) )
76 54 oveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( f ` 1 ) .- s ) = ( V .- s ) )
77 35 30 oveq12d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( e ` 1 ) .- ( e ` 0 ) ) = ( Y .- X ) )
78 76 77 eqeq12d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) <-> ( V .- s ) = ( Y .- X ) ) )
79 75 78 anbi12d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) <-> ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) ) )
80 79 bicomd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) <-> ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) )
81 80 reubidv 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( E! s e. P ( <" W V s "> .~ <" X Y Z "> /\ ( V .- s ) = ( Y .- X ) ) <-> E! s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) )
82 67 81 mpbid 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> E! s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) )
83 21 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> <" W V S "> .~ <" X Y Z "> )
84 eqidd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> S = S )
85 72 54 84 s3eqd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> <" ( f ` 2 ) ( f ` 1 ) S "> = <" W V S "> )
86 83 85 25 3brtr4d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> <" ( f ` 2 ) ( f ` 1 ) S "> .~ e )
87 22 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( V .- S ) = ( Y .- X ) )
88 54 oveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( f ` 1 ) .- S ) = ( V .- S ) )
89 87 88 77 3eqtr4d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( f ` 1 ) .- S ) = ( ( e ` 1 ) .- ( e ` 0 ) ) )
90 eqidd 
 |-  ( s = S -> ( f ` 2 ) = ( f ` 2 ) )
91 eqidd 
 |-  ( s = S -> ( f ` 1 ) = ( f ` 1 ) )
92 id 
 |-  ( s = S -> s = S )
93 90 91 92 s3eqd 
 |-  ( s = S -> <" ( f ` 2 ) ( f ` 1 ) s "> = <" ( f ` 2 ) ( f ` 1 ) S "> )
94 93 breq1d 
 |-  ( s = S -> ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e <-> <" ( f ` 2 ) ( f ` 1 ) S "> .~ e ) )
95 oveq2 
 |-  ( s = S -> ( ( f ` 1 ) .- s ) = ( ( f ` 1 ) .- S ) )
96 95 eqeq1d 
 |-  ( s = S -> ( ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) <-> ( ( f ` 1 ) .- S ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) )
97 94 96 anbi12d 
 |-  ( s = S -> ( ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) <-> ( <" ( f ` 2 ) ( f ` 1 ) S "> .~ e /\ ( ( f ` 1 ) .- S ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) )
98 97 riota2 
 |-  ( ( S e. P /\ E! s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) -> ( ( <" ( f ` 2 ) ( f ` 1 ) S "> .~ e /\ ( ( f ` 1 ) .- S ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) <-> ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) = S ) )
99 98 biimpa 
 |-  ( ( ( S e. P /\ E! s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) /\ ( <" ( f ` 2 ) ( f ` 1 ) S "> .~ e /\ ( ( f ` 1 ) .- S ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) -> ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) = S )
100 55 82 86 89 99 syl22anc 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) = S )
101 49 54 100 s3eqd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> = <" U V S "> )
102 43 101 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) = <" U V S "> )
103 102 anasss 
 |-  ( ( ph /\ ( e = <" X Y Z "> /\ f = <" U V W "> ) ) -> if ( ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ s e. P ( <" ( f ` 2 ) ( f ` 1 ) s "> .~ e /\ ( ( f ` 1 ) .- s ) = ( ( e ` 1 ) .- ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) ) "> ) = <" U V S "> )
104 1 fvexi 
 |-  P e. _V
105 104 a1i 
 |-  ( ph -> P e. _V )
106 2 105 11 12 13 16 17 elcgrabasrd 
 |-  ( ph -> <" X Y Z "> e. A )
107 2 105 8 9 10 14 15 elcgrabasrd 
 |-  ( ph -> <" U V W "> e. A )
108 22 eqcomd 
 |-  ( ph -> ( Y .- X ) = ( V .- S ) )
109 16 necomd 
 |-  ( ph -> Y =/= X )
110 1 4 3 7 12 11 9 20 108 109 tgcgrneq 
 |-  ( ph -> V =/= S )
111 2 105 8 9 20 14 110 elcgrabasrd 
 |-  ( ph -> <" U V S "> e. A )
112 23 103 106 107 111 ovmpod 
 |-  ( ph -> ( <" X Y Z "> .+ <" U V W "> ) = <" U V S "> )