Metamath Proof Explorer

Theorem angmndaddeu4

Description: There exists a unique point s satisfying the conditions of angle addition. Case where both angles are zero angles. (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 )
angmndaddeu4.1 
|- ( ph -> X ( ( hlG ` G ) ` Y ) Z )
angmndaddeu4.2 
|- ( ph -> U ( ( hlG ` G ) ` V ) W )
Assertion angmndaddeu4 
|- ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )

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 angmndaddeu4.1 
 |-  ( ph -> X ( ( hlG ` G ) ` Y ) Z )
19 angmndaddeu4.2 
 |-  ( ph -> U ( ( hlG ` G ) ` V ) W )
20 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
21 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
22 14 necomd 
 |-  ( ph -> V =/= U )
23 1 20 21 12 9 8 7 11 4 16 22 hlcgreu 
 |-  ( ph -> E! s e. P ( s ( ( hlG ` G ) ` Y ) X /\ ( Y .- s ) = ( V .- U ) ) )
24 7 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> G e. TarskiG )
25 13 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> Z e. P )
26 11 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> X e. P )
27 simpllr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. P )
28 12 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> Y e. P )
29 1 3 21 11 13 12 7 18 hlcomd 
 |-  ( ph -> Z ( ( hlG ` G ) ` Y ) X )
30 29 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> Z ( ( hlG ` G ) ` Y ) X )
31 simplr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> s ( ( hlG ` G ) ` Y ) X )
32 1 3 21 27 26 28 24 31 hlcomd 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> X ( ( hlG ` G ) ` Y ) s )
33 1 3 21 25 26 27 24 28 30 32 hltr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> Z ( ( hlG ` G ) ` Y ) s )
34 19 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> U ( ( hlG ` G ) ` V ) W )
35 9 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> V e. P )
36 1 5 21 24 33 34 28 35 zerocgra 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> <" Z Y s "> .~ <" U V W "> )
37 simpr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> ( Y .- s ) = ( V .- U ) )
38 36 37 jca 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) X ) /\ ( Y .- s ) = ( V .- U ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )
39 38 anasss 
 |-  ( ( ( ph /\ s e. P ) /\ ( s ( ( hlG ` G ) ` Y ) X /\ ( Y .- s ) = ( V .- U ) ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )
40 11 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> X e. P )
41 simpllr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. P )
42 12 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> Y e. P )
43 7 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> G e. TarskiG )
44 13 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> Z e. P )
45 18 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> X ( ( hlG ` G ) ` Y ) Z )
46 8 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> U e. P )
47 9 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> V e. P )
48 10 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> W e. P )
49 5 a1i 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> .~ = ( cgrA ` G ) )
50 simplr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> <" Z Y s "> .~ <" U V W "> )
51 49 50 breqdi 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> <" Z Y s "> ( cgrA ` G ) <" U V W "> )
52 1 3 43 21 44 42 41 46 47 48 51 cgracom 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> <" U V W "> ( cgrA ` G ) <" Z Y s "> )
53 19 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> U ( ( hlG ` G ) ` V ) W )
54 1 3 4 43 46 47 48 44 42 41 52 21 53 cgrahl 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> Z ( ( hlG ` G ) ` Y ) s )
55 1 3 21 40 44 41 43 42 45 54 hltr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> X ( ( hlG ` G ) ` Y ) s )
56 1 3 21 40 41 42 43 55 hlcomd 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> s ( ( hlG ` G ) ` Y ) X )
57 simpr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> ( Y .- s ) = ( V .- U ) )
58 56 57 jca 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> ( s ( ( hlG ` G ) ` Y ) X /\ ( Y .- s ) = ( V .- U ) ) )
59 58 anasss 
 |-  ( ( ( ph /\ s e. P ) /\ ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) ) -> ( s ( ( hlG ` G ) ` Y ) X /\ ( Y .- s ) = ( V .- U ) ) )
60 39 59 impbida 
 |-  ( ( ph /\ s e. P ) -> ( ( s ( ( hlG ` G ) ` Y ) X /\ ( Y .- s ) = ( V .- U ) ) <-> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) ) )
61 60 reubidva 
 |-  ( ph -> ( E! s e. P ( s ( ( hlG ` G ) ` Y ) X /\ ( Y .- s ) = ( V .- U ) ) <-> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) ) )
62 23 61 mpbid 
 |-  ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )