Metamath Proof Explorer

Theorem angmndaddov1

Description: Value of the addition operation in the angle addition monoid, in case the first angle is neither zero nor 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 ) ) ) =/= (/) ) ) "> ) )
angmndaddov1.x 
|- ( ph -> -. X e. ( Y L Z ) )
angmndaddov1.s 
|- ( ph -> S e. P )
angmndaddov1.1 
|- ( ph -> <" Z Y S "> .~ <" U V W "> )
angmndaddov1.2 
|- ( ph -> ( Y .- S ) = ( V .- U ) )
angmndaddov1.3 
|- ( ph -> ( ( Y L Z ) i^i ( S I X ) ) =/= (/) )
Assertion angmndaddov1 
|- ( ph -> ( <" X Y Z "> .+ <" U V W "> ) = <" X Y 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 angmndaddov1.x 
 |-  ( ph -> -. X e. ( Y L Z ) )
20 angmndaddov1.s 
 |-  ( ph -> S e. P )
21 angmndaddov1.1 
 |-  ( ph -> <" Z Y S "> .~ <" U V W "> )
22 angmndaddov1.2 
 |-  ( ph -> ( Y .- S ) = ( V .- U ) )
23 angmndaddov1.3 
 |-  ( ph -> ( ( Y L Z ) i^i ( S I X ) ) =/= (/) )
24 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 ) ) ) =/= (/) ) ) "> ) ) )
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 19 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> -. X e. ( Y L Z ) )
32 25 fveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 1 ) = ( <" X Y Z "> ` 1 ) )
33 s3fv1 
 |-  ( Y e. P -> ( <" X Y Z "> ` 1 ) = Y )
34 12 33 syl 
 |-  ( ph -> ( <" X Y Z "> ` 1 ) = Y )
35 34 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" X Y Z "> ` 1 ) = Y )
36 32 35 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 1 ) = Y )
37 25 fveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 2 ) = ( <" X Y Z "> ` 2 ) )
38 s3fv2 
 |-  ( Z e. P -> ( <" X Y Z "> ` 2 ) = Z )
39 13 38 syl 
 |-  ( ph -> ( <" X Y Z "> ` 2 ) = Z )
40 39 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" X Y Z "> ` 2 ) = Z )
41 37 40 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 2 ) = Z )
42 36 41 oveq12d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( e ` 1 ) L ( e ` 2 ) ) = ( Y L Z ) )
43 31 42 neleqtrrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> -. X e. ( ( e ` 1 ) L ( e ` 2 ) ) )
44 30 43 eqneltrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> -. ( e ` 0 ) e. ( ( e ` 1 ) L ( e ` 2 ) ) )
45 44 iffalsed 
 |-  ( ( ( 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 ) ) ) =/= (/) ) ) "> ) = <" ( 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 ) ) ) =/= (/) ) ) "> )
46 20 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> S e. P )
47 7 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> G e. TarskiG )
48 8 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> U e. P )
49 9 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> V e. P )
50 10 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> W e. P )
51 11 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> X e. P )
52 12 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> Y e. P )
53 36 52 eqeltrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 1 ) e. P )
54 13 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> Z e. P )
55 41 54 eqeltrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 2 ) e. P )
56 14 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> U =/= V )
57 15 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> V =/= W )
58 16 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> X =/= Y )
59 58 36 neeqtrrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> X =/= ( e ` 1 ) )
60 17 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> Y =/= Z )
61 36 60 eqnetrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 1 ) =/= Z )
62 61 41 neeqtrrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( e ` 1 ) =/= ( e ` 2 ) )
63 1 2 3 4 5 6 47 48 49 50 51 53 55 56 57 59 62 43 angmndaddov1lem 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> E! s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ <" U V W "> /\ ( ( e ` 1 ) .- s ) = ( V .- U ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I X ) ) =/= (/) ) )
64 simpr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> f = <" U V W "> )
65 64 breq2d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f <-> <" ( e ` 2 ) ( e ` 1 ) s "> .~ <" U V W "> ) )
66 64 fveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( f ` 1 ) = ( <" U V W "> ` 1 ) )
67 s3fv1 
 |-  ( V e. P -> ( <" U V W "> ` 1 ) = V )
68 9 67 syl 
 |-  ( ph -> ( <" U V W "> ` 1 ) = V )
69 68 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" U V W "> ` 1 ) = V )
70 66 69 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( f ` 1 ) = V )
71 64 fveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( f ` 0 ) = ( <" U V W "> ` 0 ) )
72 s3fv0 
 |-  ( U e. P -> ( <" U V W "> ` 0 ) = U )
73 8 72 syl 
 |-  ( ph -> ( <" U V W "> ` 0 ) = U )
74 73 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( <" U V W "> ` 0 ) = U )
75 71 74 eqtrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( f ` 0 ) = U )
76 70 75 oveq12d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( f ` 1 ) .- ( f ` 0 ) ) = ( V .- U ) )
77 76 eqeq2d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) <-> ( ( e ` 1 ) .- s ) = ( V .- U ) ) )
78 30 oveq2d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( s I ( e ` 0 ) ) = ( s I X ) )
79 78 ineq2d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) = ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I X ) ) )
80 79 neeq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) <-> ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I X ) ) =/= (/) ) )
81 65 77 80 3anbi123d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) <-> ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ <" U V W "> /\ ( ( e ` 1 ) .- s ) = ( V .- U ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I X ) ) =/= (/) ) ) )
82 81 reubidv 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( E! 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 ) ) ) =/= (/) ) <-> E! s e. P ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ <" U V W "> /\ ( ( e ` 1 ) .- s ) = ( V .- U ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I X ) ) =/= (/) ) ) )
83 63 82 mpbird 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> E! 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 ) ) ) =/= (/) ) )
84 21 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> <" Z Y S "> .~ <" U V W "> )
85 eqidd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> S = S )
86 41 36 85 s3eqd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> <" ( e ` 2 ) ( e ` 1 ) S "> = <" Z Y S "> )
87 84 86 64 3brtr4d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> <" ( e ` 2 ) ( e ` 1 ) S "> .~ f )
88 22 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( Y .- S ) = ( V .- U ) )
89 36 oveq1d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( e ` 1 ) .- S ) = ( Y .- S ) )
90 88 89 76 3eqtr4d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( e ` 1 ) .- S ) = ( ( f ` 1 ) .- ( f ` 0 ) ) )
91 30 oveq2d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( S I ( e ` 0 ) ) = ( S I X ) )
92 42 91 ineq12d 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( S I ( e ` 0 ) ) ) = ( ( Y L Z ) i^i ( S I X ) ) )
93 23 ad2antrr 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( Y L Z ) i^i ( S I X ) ) =/= (/) )
94 92 93 eqnetrd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( S I ( e ` 0 ) ) ) =/= (/) )
95 eqidd 
 |-  ( s = S -> ( e ` 2 ) = ( e ` 2 ) )
96 eqidd 
 |-  ( s = S -> ( e ` 1 ) = ( e ` 1 ) )
97 id 
 |-  ( s = S -> s = S )
98 95 96 97 s3eqd 
 |-  ( s = S -> <" ( e ` 2 ) ( e ` 1 ) s "> = <" ( e ` 2 ) ( e ` 1 ) S "> )
99 98 breq1d 
 |-  ( s = S -> ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f <-> <" ( e ` 2 ) ( e ` 1 ) S "> .~ f ) )
100 oveq2 
 |-  ( s = S -> ( ( e ` 1 ) .- s ) = ( ( e ` 1 ) .- S ) )
101 100 eqeq1d 
 |-  ( s = S -> ( ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) <-> ( ( e ` 1 ) .- S ) = ( ( f ` 1 ) .- ( f ` 0 ) ) ) )
102 oveq1 
 |-  ( s = S -> ( s I ( e ` 0 ) ) = ( S I ( e ` 0 ) ) )
103 102 ineq2d 
 |-  ( s = S -> ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) = ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( S I ( e ` 0 ) ) ) )
104 103 neeq1d 
 |-  ( s = S -> ( ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) <-> ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( S I ( e ` 0 ) ) ) =/= (/) ) )
105 99 101 104 3anbi123d 
 |-  ( s = S -> ( ( <" ( e ` 2 ) ( e ` 1 ) s "> .~ f /\ ( ( e ` 1 ) .- s ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( s I ( e ` 0 ) ) ) =/= (/) ) <-> ( <" ( e ` 2 ) ( e ` 1 ) S "> .~ f /\ ( ( e ` 1 ) .- S ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( S I ( e ` 0 ) ) ) =/= (/) ) ) )
106 105 riota2 
 |-  ( ( S e. P /\ E! 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 ) ) ) =/= (/) ) ) -> ( ( <" ( e ` 2 ) ( e ` 1 ) S "> .~ f /\ ( ( e ` 1 ) .- S ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( S I ( e ` 0 ) ) ) =/= (/) ) <-> ( 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 ) ) ) =/= (/) ) ) = S ) )
107 106 biimpa 
 |-  ( ( ( S e. P /\ E! 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 ) ) ) =/= (/) ) ) /\ ( <" ( e ` 2 ) ( e ` 1 ) S "> .~ f /\ ( ( e ` 1 ) .- S ) = ( ( f ` 1 ) .- ( f ` 0 ) ) /\ ( ( ( e ` 1 ) L ( e ` 2 ) ) i^i ( S I ( e ` 0 ) ) ) =/= (/) ) ) -> ( 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 ) ) ) =/= (/) ) ) = S )
108 46 83 87 90 94 107 syl23anc 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> ( 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 ) ) ) =/= (/) ) ) = S )
109 30 36 108 s3eqd 
 |-  ( ( ( ph /\ e = <" X Y Z "> ) /\ f = <" U V W "> ) -> <" ( 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 ) ) ) =/= (/) ) ) "> = <" X Y S "> )
110 45 109 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 ) ) ) =/= (/) ) ) "> ) = <" X Y S "> )
111 110 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 ) ) ) =/= (/) ) ) "> ) = <" X Y S "> )
112 1 fvexi 
 |-  P e. _V
113 112 a1i 
 |-  ( ph -> P e. _V )
114 2 113 11 12 13 16 17 elcgrabasrd 
 |-  ( ph -> <" X Y Z "> e. A )
115 2 113 8 9 10 14 15 elcgrabasrd 
 |-  ( ph -> <" U V W "> e. A )
116 22 eqcomd 
 |-  ( ph -> ( V .- U ) = ( Y .- S ) )
117 14 necomd 
 |-  ( ph -> V =/= U )
118 1 4 3 7 9 8 12 20 116 117 tgcgrneq 
 |-  ( ph -> Y =/= S )
119 2 113 11 12 20 16 118 elcgrabasrd 
 |-  ( ph -> <" X Y S "> e. A )
120 24 111 114 115 119 ovmpod 
 |-  ( ph -> ( <" X Y Z "> .+ <" U V W "> ) = <" X Y S "> )