Metamath Proof Explorer

Theorem ragraghl

Description: Drawing two right angles at a point X on the same side of a line ( X L Y ) leads to points W and Z on the same ray from X . Theorem 11.19 of Schwabhauser p. 99. (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses ragraghl.p 
|- P = ( Base ` G )
ragraghl.l 
|- L = ( LineG ` G )
ragraghl.g 
|- ( ph -> G e. TarskiG )
ragraghl.x 
|- ( ph -> X e. P )
ragraghl.y 
|- ( ph -> Y e. P )
ragraghl.z 
|- ( ph -> Z e. P )
ragraghl.1 
|- ( ph -> W e. P )
ragraghl.2 
|- ( ph -> X =/= Y )
ragraghl.3 
|- ( ph -> <" Y X Z "> e. ( raG ` G ) )
ragraghl.4 
|- ( ph -> <" Y X W "> e. ( raG ` G ) )
ragraghl.5 
|- ( ph -> Z ( ( hpG ` G ) ` ( Y L X ) ) W )
Assertion ragraghl 
|- ( ph -> Z ( ( hlG ` G ) ` X ) W )

Proof

Step Hyp Ref Expression
1 ragraghl.p 
 |-  P = ( Base ` G )
2 ragraghl.l 
 |-  L = ( LineG ` G )
3 ragraghl.g 
 |-  ( ph -> G e. TarskiG )
4 ragraghl.x 
 |-  ( ph -> X e. P )
5 ragraghl.y 
 |-  ( ph -> Y e. P )
6 ragraghl.z 
 |-  ( ph -> Z e. P )
7 ragraghl.1 
 |-  ( ph -> W e. P )
8 ragraghl.2 
 |-  ( ph -> X =/= Y )
9 ragraghl.3 
 |-  ( ph -> <" Y X Z "> e. ( raG ` G ) )
10 ragraghl.4 
 |-  ( ph -> <" Y X W "> e. ( raG ` G ) )
11 ragraghl.5 
 |-  ( ph -> Z ( ( hpG ` G ) ` ( Y L X ) ) W )
12 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
13 eqid 
 |-  ( dist ` G ) = ( dist ` G )
14 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
15 8 necomd 
 |-  ( ph -> Y =/= X )
16 1 12 2 3 5 4 15 tglinerflx2 
 |-  ( ph -> X e. ( Y L X ) )
17 eleq1w 
 |-  ( a = c -> ( a e. ( P \ ( Y L X ) ) <-> c e. ( P \ ( Y L X ) ) ) )
18 eleq1w 
 |-  ( b = d -> ( b e. ( P \ ( Y L X ) ) <-> d e. ( P \ ( Y L X ) ) ) )
19 17 18 bi2anan9 
 |-  ( ( a = c /\ b = d ) -> ( ( a e. ( P \ ( Y L X ) ) /\ b e. ( P \ ( Y L X ) ) ) <-> ( c e. ( P \ ( Y L X ) ) /\ d e. ( P \ ( Y L X ) ) ) ) )
20 oveq12 
 |-  ( ( a = c /\ b = d ) -> ( a ( Itv ` G ) b ) = ( c ( Itv ` G ) d ) )
21 20 eleq2d 
 |-  ( ( a = c /\ b = d ) -> ( s e. ( a ( Itv ` G ) b ) <-> s e. ( c ( Itv ` G ) d ) ) )
22 21 rexbidv 
 |-  ( ( a = c /\ b = d ) -> ( E. s e. ( Y L X ) s e. ( a ( Itv ` G ) b ) <-> E. s e. ( Y L X ) s e. ( c ( Itv ` G ) d ) ) )
23 eleq1w 
 |-  ( s = t -> ( s e. ( c ( Itv ` G ) d ) <-> t e. ( c ( Itv ` G ) d ) ) )
24 23 cbvrexvw 
 |-  ( E. s e. ( Y L X ) s e. ( c ( Itv ` G ) d ) <-> E. t e. ( Y L X ) t e. ( c ( Itv ` G ) d ) )
25 22 24 bitrdi 
 |-  ( ( a = c /\ b = d ) -> ( E. s e. ( Y L X ) s e. ( a ( Itv ` G ) b ) <-> E. t e. ( Y L X ) t e. ( c ( Itv ` G ) d ) ) )
26 19 25 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( ( a e. ( P \ ( Y L X ) ) /\ b e. ( P \ ( Y L X ) ) ) /\ E. s e. ( Y L X ) s e. ( a ( Itv ` G ) b ) ) <-> ( ( c e. ( P \ ( Y L X ) ) /\ d e. ( P \ ( Y L X ) ) ) /\ E. t e. ( Y L X ) t e. ( c ( Itv ` G ) d ) ) ) )
27 26 cbvopabv 
 |-  { <. a , b >. | ( ( a e. ( P \ ( Y L X ) ) /\ b e. ( P \ ( Y L X ) ) ) /\ E. s e. ( Y L X ) s e. ( a ( Itv ` G ) b ) ) } = { <. c , d >. | ( ( c e. ( P \ ( Y L X ) ) /\ d e. ( P \ ( Y L X ) ) ) /\ E. t e. ( Y L X ) t e. ( c ( Itv ` G ) d ) ) }
28 1 12 2 3 5 4 15 tgelrnln 
 |-  ( ph -> ( Y L X ) e. ran L )
29 1 12 2 27 3 28 6 7 11 hpgne1 
 |-  ( ph -> -. Z e. ( Y L X ) )
30 nelne2 
 |-  ( ( X e. ( Y L X ) /\ -. Z e. ( Y L X ) ) -> X =/= Z )
31 16 29 30 syl2anc 
 |-  ( ph -> X =/= Z )
32 31 necomd 
 |-  ( ph -> Z =/= X )
33 1 13 12 2 14 3 5 4 6 9 15 32 ragncol 
 |-  ( ph -> -. ( Z e. ( Y L X ) \/ Y = X ) )
34 1 2 12 3 5 4 6 33 ncolrot1 
 |-  ( ph -> -. ( Y e. ( X L Z ) \/ X = Z ) )
35 1 12 2 27 3 28 6 7 11 hpgne2 
 |-  ( ph -> -. W e. ( Y L X ) )
36 nelne2 
 |-  ( ( X e. ( Y L X ) /\ -. W e. ( Y L X ) ) -> X =/= W )
37 16 35 36 syl2anc 
 |-  ( ph -> X =/= W )
38 37 necomd 
 |-  ( ph -> W =/= X )
39 1 13 12 2 14 3 5 4 7 10 15 38 ragncol 
 |-  ( ph -> -. ( W e. ( Y L X ) \/ Y = X ) )
40 1 2 12 3 5 4 7 39 ncolrot1 
 |-  ( ph -> -. ( Y e. ( X L W ) \/ X = W ) )
41 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
42 1 12 3 41 5 4 6 15 31 cgraid 
 |-  ( ph -> <" Y X Z "> ( cgrA ` G ) <" Y X Z "> )
43 1 3 5 4 6 5 4 7 9 10 15 37 15 31 ragcgra 
 |-  ( ph -> <" Y X Z "> ( cgrA ` G ) <" Y X W "> )
44 1 12 2 3 28 7 27 35 hpgid 
 |-  ( ph -> W ( ( hpG ` G ) ` ( Y L X ) ) W )
45 1 12 13 3 5 4 6 5 4 7 2 34 40 6 7 41 42 43 11 44 acopyeu 
 |-  ( ph -> Z ( ( hlG ` G ) ` X ) W )