Metamath Proof Explorer

Theorem angmgmaddeu2

Description: Existence of a unique point for building angle addition. Case where the second angle is a zero angle. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses angmgmadd.p 
|- P = ( Base ` G )
angmgmadd.a 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
angmgmadd.i 
|- I = ( Itv ` G )
angmgmadd.d 
|- .- = ( dist ` G )
angmgmadd.c 
|- .~ = ( cgrA ` G )
angmgmadd.l 
|- L = ( LineG ` G )
angmgmadd.g 
|- ( ph -> G e. TarskiG )
angmgmaddov.u 
|- ( ph -> U e. P )
angmgmaddov.v 
|- ( ph -> V e. P )
angmgmaddov.w 
|- ( ph -> W e. P )
angmgmaddov.x 
|- ( ph -> X e. P )
angmgmaddov.y 
|- ( ph -> Y e. P )
angmgmaddov.z 
|- ( ph -> Z e. P )
angmgmaddeu.1 
|- ( ph -> U =/= V )
angmgmaddeu.2 
|- ( ph -> V =/= W )
angmgmaddeu.3 
|- ( ph -> X =/= Y )
angmgmaddeu.4 
|- ( ph -> Y =/= Z )
angmgmaddeu2.1 
|- ( ph -> -. X e. ( Y L Z ) )
angmgmaddeu2.2 
|- ( ph -> U ( ( hlG ` G ) ` V ) W )
Assertion angmgmaddeu2 
|- ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 angmgmadd.p 
 |-  P = ( Base ` G )
2 angmgmadd.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 angmgmadd.i 
 |-  I = ( Itv ` G )
4 angmgmadd.d 
 |-  .- = ( dist ` G )
5 angmgmadd.c 
 |-  .~ = ( cgrA ` G )
6 angmgmadd.l 
 |-  L = ( LineG ` G )
7 angmgmadd.g 
 |-  ( ph -> G e. TarskiG )
8 angmgmaddov.u 
 |-  ( ph -> U e. P )
9 angmgmaddov.v 
 |-  ( ph -> V e. P )
10 angmgmaddov.w 
 |-  ( ph -> W e. P )
11 angmgmaddov.x 
 |-  ( ph -> X e. P )
12 angmgmaddov.y 
 |-  ( ph -> Y e. P )
13 angmgmaddov.z 
 |-  ( ph -> Z e. P )
14 angmgmaddeu.1 
 |-  ( ph -> U =/= V )
15 angmgmaddeu.2 
 |-  ( ph -> V =/= W )
16 angmgmaddeu.3 
 |-  ( ph -> X =/= Y )
17 angmgmaddeu.4 
 |-  ( ph -> Y =/= Z )
18 angmgmaddeu2.1 
 |-  ( ph -> -. X e. ( Y L Z ) )
19 angmgmaddeu2.2 
 |-  ( ph -> U ( ( hlG ` G ) ` V ) W )
20 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
21 17 necomd 
 |-  ( ph -> Z =/= Y )
22 14 necomd 
 |-  ( ph -> V =/= U )
23 1 3 20 12 9 8 7 13 4 21 22 hlcgreu 
 |-  ( ph -> E! s e. P ( s ( ( hlG ` G ) ` Y ) Z /\ ( Y .- s ) = ( V .- U ) ) )
24 7 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> G e. TarskiG )
25 simpllr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. P )
26 13 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> Z e. P )
27 12 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> Y e. P )
28 simplr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> s ( ( hlG ` G ) ` Y ) Z )
29 1 3 20 25 26 27 24 28 hlcomd 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> Z ( ( hlG ` G ) ` Y ) s )
30 19 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> U ( ( hlG ` G ) ` V ) W )
31 9 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> V e. P )
32 1 5 20 24 29 30 27 31 zerocgra 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> <" Z Y s "> .~ <" U V W "> )
33 simpr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> ( Y .- s ) = ( V .- U ) )
34 17 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> Y =/= Z )
35 1 3 20 26 25 27 24 6 29 hlln 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> Z e. ( s L Y ) )
36 8 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> U e. P )
37 33 eqcomd 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> ( V .- U ) = ( Y .- s ) )
38 22 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> V =/= U )
39 1 4 3 24 31 36 27 25 37 38 tgcgrneq 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> Y =/= s )
40 39 necomd 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> s =/= Y )
41 1 3 6 24 27 26 25 34 35 40 lnrot1 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. ( Y L Z ) )
42 11 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> X e. P )
43 1 4 3 24 25 42 tgbtwntriv1 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. ( s I X ) )
44 41 43 elind 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. ( ( Y L Z ) i^i ( s I X ) ) )
45 44 ne0d 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> ( ( Y L Z ) i^i ( s I X ) ) =/= (/) )
46 32 33 45 3jca 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
47 46 anasss 
 |-  ( ( ( ph /\ s e. P ) /\ ( s ( ( hlG ` G ) ` Y ) Z /\ ( Y .- s ) = ( V .- U ) ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
48 13 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> Z e. P )
49 simp-4r 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> s e. P )
50 12 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> Y e. P )
51 7 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> G e. TarskiG )
52 8 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> U e. P )
53 9 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> V e. P )
54 10 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> W e. P )
55 5 a1i 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> .~ = ( cgrA ` G ) )
56 simpllr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" Z Y s "> .~ <" U V W "> )
57 55 56 breqdi 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" Z Y s "> ( cgrA ` G ) <" U V W "> )
58 1 3 51 20 48 50 49 52 53 54 57 cgracom 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" U V W "> ( cgrA ` G ) <" Z Y s "> )
59 19 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> U ( ( hlG ` G ) ` V ) W )
60 1 3 4 51 52 53 54 48 50 49 58 20 59 cgrahl 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> Z ( ( hlG ` G ) ` Y ) s )
61 1 3 20 48 49 50 51 60 hlcomd 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> s ( ( hlG ` G ) ` Y ) Z )
62 simplr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( Y .- s ) = ( V .- U ) )
63 61 62 jca 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( s ( ( hlG ` G ) ` Y ) Z /\ ( Y .- s ) = ( V .- U ) ) )
64 63 3anasss 
 |-  ( ( ( ph /\ s e. P ) /\ ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) ) -> ( s ( ( hlG ` G ) ` Y ) Z /\ ( Y .- s ) = ( V .- U ) ) )
65 47 64 impbida 
 |-  ( ( ph /\ s e. P ) -> ( ( s ( ( hlG ` G ) ` Y ) Z /\ ( Y .- s ) = ( V .- U ) ) <-> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) ) )
66 65 reubidva 
 |-  ( ph -> ( E! s e. P ( s ( ( hlG ` G ) ` Y ) Z /\ ( Y .- s ) = ( V .- U ) ) <-> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) ) )
67 23 66 mpbid 
 |-  ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )