Metamath Proof Explorer

Theorem cgrarag

Description: Any angle <" A B C "> congruent with a right angle <" X Y Z "> is a right angle. Theorem 11.17 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 13-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 ) )
cgrarag.1 
|- ( ph -> <" X Y Z "> ( cgrA ` G ) <" A B C "> )
Assertion cgrarag 
|- ( ph -> <" A B C "> e. ( raG ` G ) )

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 cgrarag.1 
 |-  ( ph -> <" X Y Z "> ( cgrA ` G ) <" A B C "> )
11 eqid 
 |-  ( dist ` G ) = ( dist ` G )
12 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
13 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
14 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
15 2 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> G e. TarskiG )
16 simp-5r 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> a e. P )
17 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> B e. P )
18 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> C e. P )
19 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> A e. P )
20 simp-4r 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> c e. P )
21 3 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> X e. P )
22 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> Y e. P )
23 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> Z e. P )
24 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
25 9 ad5antr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> <" X Y Z "> e. ( raG ` G ) )
26 simpllr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> <" X Y Z "> ( cgrG ` G ) <" a B c "> )
27 1 11 12 13 14 15 21 22 23 24 16 17 20 25 26 ragcgr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> <" a B c "> e. ( raG ` G ) )
28 1 11 12 13 14 15 16 17 20 27 ragcom 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> <" c B a "> e. ( raG ` G ) )
29 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
30 simpr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> c ( ( hlG ` G ) ` B ) C )
31 1 12 29 20 18 17 15 30 hlne1 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> c =/= B )
32 1 12 29 20 18 17 15 30 hlcomd 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> C ( ( hlG ` G ) ` B ) c )
33 1 12 29 18 20 17 15 13 32 hlln 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> C e. ( c ( LineG ` G ) B ) )
34 33 orcd 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> ( C e. ( c ( LineG ` G ) B ) \/ c = B ) )
35 1 13 12 15 20 17 18 34 colrot1 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> ( c e. ( B ( LineG ` G ) C ) \/ B = C ) )
36 1 11 12 13 14 15 20 17 16 18 28 31 35 ragcol 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> <" C B a "> e. ( raG ` G ) )
37 1 11 12 13 14 15 18 17 16 36 ragcom 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> <" a B C "> e. ( raG ` G ) )
38 simplr 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> a ( ( hlG ` G ) ` B ) A )
39 1 12 29 16 19 17 15 38 hlne1 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> a =/= B )
40 1 12 29 16 19 17 15 38 hlcomd 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> A ( ( hlG ` G ) ` B ) a )
41 1 12 29 19 16 17 15 13 40 hlln 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> A e. ( a ( LineG ` G ) B ) )
42 41 orcd 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> ( A e. ( a ( LineG ` G ) B ) \/ a = B ) )
43 1 13 12 15 16 17 19 42 colrot1 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> ( a e. ( B ( LineG ` G ) A ) \/ B = A ) )
44 1 11 12 13 14 15 16 17 18 19 37 39 43 ragcol 
 |-  ( ( ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" a B c "> ) /\ a ( ( hlG ` G ) ` B ) A ) /\ c ( ( hlG ` G ) ` B ) C ) -> <" A B C "> e. ( raG ` G ) )
45 44 3anasss 
 |-  ( ( ( ( ph /\ a e. P ) /\ c e. P ) /\ ( <" X Y Z "> ( cgrG ` G ) <" a B c "> /\ a ( ( hlG ` G ) ` B ) A /\ c ( ( hlG ` G ) ` B ) C ) ) -> <" A B C "> e. ( raG ` G ) )
46 1 12 29 2 3 4 5 6 7 8 iscgra 
 |-  ( ph -> ( <" X Y Z "> ( cgrA ` G ) <" A B C "> <-> E. a e. P E. c e. P ( <" X Y Z "> ( cgrG ` G ) <" a B c "> /\ a ( ( hlG ` G ) ` B ) A /\ c ( ( hlG ` G ) ` B ) C ) ) )
47 10 46 mpbid 
 |-  ( ph -> E. a e. P E. c e. P ( <" X Y Z "> ( cgrG ` G ) <" a B c "> /\ a ( ( hlG ` G ) ` B ) A /\ c ( ( hlG ` G ) ` B ) C ) )
48 45 47 r19.29vva 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )