Metamath Proof Explorer

Theorem ragsupplcgra

Description: An angle <" X Y Z "> is a right angle exactly when it is congruent to its supplementary angle <" X Y W "> . Theorem 11.18 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses ragsupplcgra.p 
|- P = ( Base ` G )
ragsupplcgra.i 
|- I = ( Itv ` G )
ragsupplcgra.g 
|- ( ph -> G e. TarskiG )
ragsupplcgra.7 
|- ( ph -> X e. ( P \ { Y } ) )
ragsupplcgra.x 
|- ( ph -> Y e. P )
ragsupplcgra.z 
|- ( ph -> Z e. ( P \ { Y } ) )
ragsupplcgra.w 
|- ( ph -> W e. ( P \ { Y } ) )
ragsupplcgra.y 
|- ( ph -> Y e. ( Z I W ) )
Assertion ragsupplcgra 
|- ( ph -> ( <" X Y Z "> e. ( raG ` G ) <-> <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) )

Proof

Step Hyp Ref Expression
1 ragsupplcgra.p 
 |-  P = ( Base ` G )
2 ragsupplcgra.i 
 |-  I = ( Itv ` G )
3 ragsupplcgra.g 
 |-  ( ph -> G e. TarskiG )
4 ragsupplcgra.7 
 |-  ( ph -> X e. ( P \ { Y } ) )
5 ragsupplcgra.x 
 |-  ( ph -> Y e. P )
6 ragsupplcgra.z 
 |-  ( ph -> Z e. ( P \ { Y } ) )
7 ragsupplcgra.w 
 |-  ( ph -> W e. ( P \ { Y } ) )
8 ragsupplcgra.y 
 |-  ( ph -> Y e. ( Z I W ) )
9 3 adantr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> G e. TarskiG )
10 4 eldifad 
 |-  ( ph -> X e. P )
11 10 adantr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> X e. P )
12 5 adantr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> Y e. P )
13 6 eldifad 
 |-  ( ph -> Z e. P )
14 13 adantr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> Z e. P )
15 7 eldifad 
 |-  ( ph -> W e. P )
16 15 adantr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> W e. P )
17 simpr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> <" X Y Z "> e. ( raG ` G ) )
18 eqid 
 |-  ( dist ` G ) = ( dist ` G )
19 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
20 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
21 1 18 2 19 20 9 11 12 14 17 ragcom 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> <" Z Y X "> e. ( raG ` G ) )
22 6 eldifsnbd 
 |-  ( ph -> Z =/= Y )
23 22 adantr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> Z =/= Y )
24 8 adantr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> Y e. ( Z I W ) )
25 1 19 2 9 12 16 14 24 btwncolg2 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> ( Z e. ( Y ( LineG ` G ) W ) \/ Y = W ) )
26 1 18 2 19 20 9 14 12 11 16 21 23 25 ragcol 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> <" W Y X "> e. ( raG ` G ) )
27 1 18 2 19 20 9 16 12 11 26 ragcom 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> <" X Y W "> e. ( raG ` G ) )
28 4 eldifsnbd 
 |-  ( ph -> X =/= Y )
29 28 adantr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> X =/= Y )
30 7 eldifsnbd 
 |-  ( ph -> W =/= Y )
31 30 necomd 
 |-  ( ph -> Y =/= W )
32 31 adantr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> Y =/= W )
33 22 necomd 
 |-  ( ph -> Y =/= Z )
34 33 adantr 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> Y =/= Z )
35 1 9 11 12 14 11 12 16 17 27 29 32 29 34 ragcgra 
 |-  ( ( ph /\ <" X Y Z "> e. ( raG ` G ) ) -> <" X Y Z "> ( cgrA ` G ) <" X Y W "> )
36 3 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> G e. TarskiG )
37 13 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> Z e. P )
38 10 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> X e. P )
39 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> z e. P )
40 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> x e. P )
41 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
42 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> Y e. P )
43 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> <" X Y Z "> ( cgrG ` G ) <" x Y z "> )
44 1 18 2 41 36 38 42 37 40 42 39 43 cgr3simp3 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( Z ( dist ` G ) X ) = ( z ( dist ` G ) x ) )
45 1 18 2 36 37 38 39 40 44 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( X ( dist ` G ) Z ) = ( x ( dist ` G ) z ) )
46 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
47 28 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> X =/= Y )
48 47 necomd 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> Y =/= X )
49 1 2 46 38 38 42 36 47 hlid 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> X ( ( hlG ` G ) ` Y ) X )
50 simplr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> x ( ( hlG ` G ) ` Y ) X )
51 eqidd 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( Y ( dist ` G ) X ) = ( Y ( dist ` G ) X ) )
52 1 18 2 41 36 38 42 37 40 42 39 43 cgr3simp1 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( X ( dist ` G ) Y ) = ( x ( dist ` G ) Y ) )
53 52 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( x ( dist ` G ) Y ) = ( X ( dist ` G ) Y ) )
54 1 18 2 36 40 42 38 42 53 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( Y ( dist ` G ) x ) = ( Y ( dist ` G ) X ) )
55 1 18 46 42 42 38 36 38 47 48 49 50 51 54 hlcgreq 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> X = x )
56 eqid 
 |-  ( ( pInvG ` G ) ` Y ) = ( ( pInvG ` G ) ` Y )
57 1 18 2 19 20 36 42 56 37 mircl 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( ( ( pInvG ` G ) ` Y ) ` Z ) e. P )
58 22 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> Z =/= Y )
59 1 18 2 19 20 36 42 56 37 mirbtwn 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> Y e. ( ( ( ( pInvG ` G ) ` Y ) ` Z ) I Z ) )
60 1 18 2 36 57 42 37 59 tgbtwncom 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> Y e. ( Z I ( ( ( pInvG ` G ) ` Y ) ` Z ) ) )
61 15 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> W e. P )
62 simpr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> z ( ( hlG ` G ) ` Y ) W )
63 1 2 46 39 61 42 36 62 hlcomd 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> W ( ( hlG ` G ) ` Y ) z )
64 1 18 2 3 13 5 15 8 tgbtwncom 
 |-  ( ph -> Y e. ( W I Z ) )
65 64 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> Y e. ( W I Z ) )
66 1 2 46 61 39 37 36 42 63 65 btwnhl 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> Y e. ( z I Z ) )
67 1 18 2 36 39 42 37 66 tgbtwncom 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> Y e. ( Z I z ) )
68 1 18 2 19 20 36 42 56 37 mircgr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( Y ( dist ` G ) ( ( ( pInvG ` G ) ` Y ) ` Z ) ) = ( Y ( dist ` G ) Z ) )
69 1 18 2 41 36 38 42 37 40 42 39 43 cgr3simp2 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( Y ( dist ` G ) Z ) = ( Y ( dist ` G ) z ) )
70 69 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( Y ( dist ` G ) z ) = ( Y ( dist ` G ) Z ) )
71 1 18 2 36 42 42 37 37 57 39 58 60 67 68 70 tgsegconeq 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( ( ( pInvG ` G ) ` Y ) ` Z ) = z )
72 55 71 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( X ( dist ` G ) ( ( ( pInvG ` G ) ` Y ) ` Z ) ) = ( x ( dist ` G ) z ) )
73 45 72 eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( X ( dist ` G ) Z ) = ( X ( dist ` G ) ( ( ( pInvG ` G ) ` Y ) ` Z ) ) )
74 1 18 2 19 20 3 10 5 13 israg 
 |-  ( ph -> ( <" X Y Z "> e. ( raG ` G ) <-> ( X ( dist ` G ) Z ) = ( X ( dist ` G ) ( ( ( pInvG ` G ) ` Y ) ` Z ) ) ) )
75 74 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> ( <" X Y Z "> e. ( raG ` G ) <-> ( X ( dist ` G ) Z ) = ( X ( dist ` G ) ( ( ( pInvG ` G ) ` Y ) ` Z ) ) ) )
76 73 75 mpbird 
 |-  ( ( ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ <" X Y Z "> ( cgrG ` G ) <" x Y z "> ) /\ x ( ( hlG ` G ) ` Y ) X ) /\ z ( ( hlG ` G ) ` Y ) W ) -> <" X Y Z "> e. ( raG ` G ) )
77 76 3anasss 
 |-  ( ( ( ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) /\ x e. P ) /\ z e. P ) /\ ( <" X Y Z "> ( cgrG ` G ) <" x Y z "> /\ x ( ( hlG ` G ) ` Y ) X /\ z ( ( hlG ` G ) ` Y ) W ) ) -> <" X Y Z "> e. ( raG ` G ) )
78 1 2 46 3 10 5 13 10 5 15 iscgra 
 |-  ( ph -> ( <" X Y Z "> ( cgrA ` G ) <" X Y W "> <-> E. x e. P E. z e. P ( <" X Y Z "> ( cgrG ` G ) <" x Y z "> /\ x ( ( hlG ` G ) ` Y ) X /\ z ( ( hlG ` G ) ` Y ) W ) ) )
79 78 biimpa 
 |-  ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) -> E. x e. P E. z e. P ( <" X Y Z "> ( cgrG ` G ) <" x Y z "> /\ x ( ( hlG ` G ) ` Y ) X /\ z ( ( hlG ` G ) ` Y ) W ) )
80 77 79 r19.29vva 
 |-  ( ( ph /\ <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) -> <" X Y Z "> e. ( raG ` G ) )
81 35 80 impbida 
 |-  ( ph -> ( <" X Y Z "> e. ( raG ` G ) <-> <" X Y Z "> ( cgrA ` G ) <" X Y W "> ) )