Definition df-rag

Description: Define the class of right angles. Definition 8.1 of Schwabhauser p. 57. See israg . (Contributed by Thierry Arnoux, 25-Aug-2019)

	Ref	Expression
Assertion	df-rag	|- raG = ( g e. _V |-> { w e. Word ( Base ` g ) | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crag	|- raG
1		vg	|- g
2		cvv	|- _V
3		vw	|- w
4		cbs	|- Base
5	1	cv	|- g
6	5 4	cfv	|- ( Base ` g )
7	6	cword	|- Word ( Base ` g )
8		chash	|- #
9	3	cv	|- w
10	9 8	cfv	|- ( # ` w )
11		c3	|- 3
12	10 11	wceq	|- ( # ` w ) = 3
13		cc0	|- 0
14	13 9	cfv	|- ( w ` 0 )
15		cds	|- dist
16	5 15	cfv	|- ( dist ` g )
17		c2	|- 2
18	17 9	cfv	|- ( w ` 2 )
19	14 18 16	co	|- ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) )
20		cmir	|- pInvG
21	5 20	cfv	|- ( pInvG ` g )
22		c1	|- 1
23	22 9	cfv	|- ( w ` 1 )
24	23 21	cfv	|- ( ( pInvG ` g ) ` ( w ` 1 ) )
25	18 24	cfv	|- ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) )
26	14 25 16	co	|- ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) )
27	19 26	wceq	|- ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) )
28	12 27	wa	|- ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) )
29	28 3 7	crab	|- { w e. Word ( Base ` g ) | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) }
30	1 2 29	cmpt	|- ( g e. _V |-> { w e. Word ( Base ` g ) | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } )
31	0 30	wceq	|- raG = ( g e. _V |-> { w e. Word ( Base ` g ) | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } )