Metamath Proof Explorer

Theorem ragcgra

Description: Right angles are congruent with each other. Theorem 11.16 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses ragcgra.p 
|- P = ( Base ` G )
ragcgra.g 
|- ( ph -> G e. TarskiG )
ragcgra.x 
|- ( ph -> X e. P )
ragcgra.y 
|- ( ph -> Y e. P )
ragcgra.z 
|- ( ph -> Z e. P )
ragcgra.a 
|- ( ph -> A e. P )
ragcgra.b 
|- ( ph -> B e. P )
ragcgra.c 
|- ( ph -> C e. P )
ragcgra.1 
|- ( ph -> <" X Y Z "> e. ( raG ` G ) )
ragcgra.2 
|- ( ph -> <" A B C "> e. ( raG ` G ) )
ragcgra.3 
|- ( ph -> A =/= B )
ragcgra.4 
|- ( ph -> B =/= C )
ragcgra.5 
|- ( ph -> X =/= Y )
ragcgra.6 
|- ( ph -> Y =/= Z )
Assertion ragcgra 
|- ( ph -> <" X Y Z "> ( cgrA ` G ) <" A B C "> )

Proof

Step Hyp Ref Expression
1 ragcgra.p 
 |-  P = ( Base ` G )
2 ragcgra.g 
 |-  ( ph -> G e. TarskiG )
3 ragcgra.x 
 |-  ( ph -> X e. P )
4 ragcgra.y 
 |-  ( ph -> Y e. P )
5 ragcgra.z 
 |-  ( ph -> Z e. P )
6 ragcgra.a 
 |-  ( ph -> A e. P )
7 ragcgra.b 
 |-  ( ph -> B e. P )
8 ragcgra.c 
 |-  ( ph -> C e. P )
9 ragcgra.1 
 |-  ( ph -> <" X Y Z "> e. ( raG ` G ) )
10 ragcgra.2 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
11 ragcgra.3 
 |-  ( ph -> A =/= B )
12 ragcgra.4 
 |-  ( ph -> B =/= C )
13 ragcgra.5 
 |-  ( ph -> X =/= Y )
14 ragcgra.6 
 |-  ( ph -> Y =/= Z )
15 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
16 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
17 2 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> G e. TarskiG )
18 3 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> X e. P )
19 4 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> Y e. P )
20 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> Z e. P )
21 6 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> A e. P )
22 7 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> B e. P )
23 8 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> C e. P )
24 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> a e. P )
25 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> c e. P )
26 eqid 
 |-  ( dist ` G ) = ( dist ` G )
27 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
28 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) )
29 28 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> ( Y ( dist ` G ) X ) = ( B ( dist ` G ) a ) )
30 1 26 15 17 19 18 22 24 29 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> ( X ( dist ` G ) Y ) = ( a ( dist ` G ) B ) )
31 simpr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) )
32 31 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> ( Y ( dist ` G ) Z ) = ( B ( dist ` G ) c ) )
33 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
34 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
35 12 necomd 
 |-  ( ph -> C =/= B )
36 1 26 15 33 34 2 6 7 8 10 11 35 ragncol 
 |-  ( ph -> -. ( C e. ( A ( LineG ` G ) B ) \/ A = B ) )
37 1 33 15 2 6 7 8 36 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
38 37 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> G TarskiGDim>= 2 )
39 9 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> <" X Y Z "> e. ( raG ` G ) )
40 10 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> <" A B C "> e. ( raG ` G ) )
41 1 26 15 33 34 17 21 22 23 40 ragcom 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> <" C B A "> e. ( raG ` G ) )
42 35 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> C =/= B )
43 14 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> Y =/= Z )
44 1 26 15 17 19 20 22 25 32 43 tgcgrneq 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> B =/= c )
45 simplr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> c ( ( hlG ` G ) ` B ) C )
46 1 15 16 25 23 22 17 33 45 hlln 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> c e. ( C ( LineG ` G ) B ) )
47 1 15 33 17 22 25 23 44 46 42 lnrot1 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> C e. ( B ( LineG ` G ) c ) )
48 47 orcd 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> ( C e. ( B ( LineG ` G ) c ) \/ B = c ) )
49 1 26 15 33 34 17 23 22 21 25 41 42 48 ragcol 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> <" c B A "> e. ( raG ` G ) )
50 1 26 15 33 34 17 25 22 21 49 ragcom 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> <" A B c "> e. ( raG ` G ) )
51 11 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> A =/= B )
52 13 necomd 
 |-  ( ph -> Y =/= X )
53 52 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> Y =/= X )
54 1 26 15 17 19 18 22 24 29 53 tgcgrneq 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> B =/= a )
55 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> a ( ( hlG ` G ) ` B ) A )
56 1 15 16 24 21 22 17 33 55 hlln 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> a e. ( A ( LineG ` G ) B ) )
57 1 15 33 17 22 24 21 54 56 51 lnrot1 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> A e. ( B ( LineG ` G ) a ) )
58 57 orcd 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> ( A e. ( B ( LineG ` G ) a ) \/ B = a ) )
59 1 26 15 33 34 17 21 22 25 24 50 51 58 ragcol 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> <" a B c "> e. ( raG ` G ) )
60 1 26 15 17 38 18 19 20 24 22 25 39 59 30 32 hypcgr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> ( X ( dist ` G ) Z ) = ( a ( dist ` G ) c ) )
61 1 26 15 17 18 20 24 25 60 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> ( Z ( dist ` G ) X ) = ( c ( dist ` G ) a ) )
62 1 26 27 17 18 19 20 24 22 25 30 32 61 trgcgr 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> <" X Y Z "> ( cgrG ` G ) <" a B c "> )
63 1 15 16 17 18 19 20 21 22 23 24 25 62 55 45 iscgrad 
 |-  ( ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ c ( ( hlG ` G ) ` B ) C ) /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) -> <" X Y Z "> ( cgrA ` G ) <" A B C "> )
64 63 anasss 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) /\ c e. P ) /\ ( c ( ( hlG ` G ) ` B ) C /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) ) -> <" X Y Z "> ( cgrA ` G ) <" A B C "> )
65 1 15 16 7 4 5 2 8 26 35 14 hlcgrex 
 |-  ( ph -> E. c e. P ( c ( ( hlG ` G ) ` B ) C /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) )
66 65 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) -> E. c e. P ( c ( ( hlG ` G ) ` B ) C /\ ( B ( dist ` G ) c ) = ( Y ( dist ` G ) Z ) ) )
67 64 66 r19.29a 
 |-  ( ( ( ( ph /\ a e. P ) /\ a ( ( hlG ` G ) ` B ) A ) /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) -> <" X Y Z "> ( cgrA ` G ) <" A B C "> )
68 67 anasss 
 |-  ( ( ( ph /\ a e. P ) /\ ( a ( ( hlG ` G ) ` B ) A /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) ) -> <" X Y Z "> ( cgrA ` G ) <" A B C "> )
69 1 15 16 7 4 3 2 6 26 11 52 hlcgrex 
 |-  ( ph -> E. a e. P ( a ( ( hlG ` G ) ` B ) A /\ ( B ( dist ` G ) a ) = ( Y ( dist ` G ) X ) ) )
70 68 69 r19.29a 
 |-  ( ph -> <" X Y Z "> ( cgrA ` G ) <" A B C "> )