Metamath Proof Explorer

Theorem angmndaddeu6

Description: There exists a unique point s satisfying the conditions of angle addition. Case where the first angle is a zero angle, and the second angle is a straight angle. (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 )
angmndaddeu6.1 
|- ( ph -> Y e. ( X I Z ) )
angmndaddeu6.2 
|- ( ph -> U ( ( hlG ` G ) ` V ) W )
Assertion angmndaddeu6 
|- ( 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 angmndaddeu6.1 
 |-  ( ph -> Y e. ( X I Z ) )
19 angmndaddeu6.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 32 33 jca 
 |-  ( ( ( ( ph /\ s e. P ) /\ s ( ( hlG ` G ) ` Y ) Z ) /\ ( Y .- s ) = ( V .- U ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )
35 34 anasss 
 |-  ( ( ( ph /\ s e. P ) /\ ( s ( ( hlG ` G ) ` Y ) Z /\ ( Y .- s ) = ( V .- U ) ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )
36 13 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> Z e. P )
37 simpllr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. P )
38 12 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> Y e. P )
39 7 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> G e. TarskiG )
40 8 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> U e. P )
41 9 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> V e. P )
42 10 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> W e. P )
43 5 a1i 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> .~ = ( cgrA ` G ) )
44 simplr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> <" Z Y s "> .~ <" U V W "> )
45 43 44 breqdi 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> <" Z Y s "> ( cgrA ` G ) <" U V W "> )
46 1 3 39 20 36 38 37 40 41 42 45 cgracom 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> <" U V W "> ( cgrA ` G ) <" Z Y s "> )
47 19 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> U ( ( hlG ` G ) ` V ) W )
48 1 3 4 39 40 41 42 36 38 37 46 20 47 cgrahl 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> Z ( ( hlG ` G ) ` Y ) s )
49 1 3 20 36 37 38 39 48 hlcomd 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> s ( ( hlG ` G ) ` Y ) Z )
50 simpr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> ( Y .- s ) = ( V .- U ) )
51 49 50 jca 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> ( s ( ( hlG ` G ) ` Y ) Z /\ ( Y .- s ) = ( V .- U ) ) )
52 51 anasss 
 |-  ( ( ( ph /\ s e. P ) /\ ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) ) -> ( s ( ( hlG ` G ) ` Y ) Z /\ ( Y .- s ) = ( V .- U ) ) )
53 35 52 impbida 
 |-  ( ( ph /\ s e. P ) -> ( ( s ( ( hlG ` G ) ` Y ) Z /\ ( Y .- s ) = ( V .- U ) ) <-> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) ) )
54 53 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 ) ) ) )
55 23 54 mpbid 
 |-  ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )