Definition df-rag 23772

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

Assertion

Ref	Expression
df-rag	|- ∟G = ( 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 ) ) ) ) } )

Distinct variable group:   w, g

Detailed syntax breakdown of Definition df-rag

Step	Hyp	Ref	Expression
1		crag 23771	. 2 class ∟G
2		vg	. . 3 setvar g
3		cvv 3106	. . 3 class _V
4		vw	. . . . . . . 8 setvar w
5	4	cv 1373	. . . . . . 7 class w
6		chash 12360	. . . . . . 7 class #
7	5, 6	cfv 5579	. . . . . 6 class ( # ` w )
8		c3 10575	. . . . . 6 class 3
9	7, 8	wceq 1374	. . . . 5 wff ( # ` w ) = 3
10		cc0 9481	. . . . . . . 8 class 0
11	10, 5	cfv 5579	. . . . . . 7 class ( w ` 0 )
12		c2 10574	. . . . . . . 8 class 2
13	12, 5	cfv 5579	. . . . . . 7 class ( w ` 2 )
14	2	cv 1373	. . . . . . . 8 class g
15		cds 14553	. . . . . . . 8 class dist
16	14, 15	cfv 5579	. . . . . . 7 class ( dist ` g )
17	11, 13, 16	co 6275	. . . . . 6 class ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) )
18		c1 9482	. . . . . . . . . 10 class 1
19	18, 5	cfv 5579	. . . . . . . . 9 class ( w ` 1 )
20		cmir 23739	. . . . . . . . . 10 class pInvG
21	14, 20	cfv 5579	. . . . . . . . 9 class (pInvG ` g )
22	19, 21	cfv 5579	. . . . . . . 8 class ( (pInvG ` g ) ` ( w ` 1 ) )
23	13, 22	cfv 5579	. . . . . . 7 class ( ( (pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) )
24	11, 23, 16	co 6275	. . . . . 6 class ( ( w ` 0 ) ( dist ` g ) ( ( (pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) )
25	17, 24	wceq 1374	. . . . 5 wff ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( (pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) )
26	9, 25	wa 369	. . . 4 wff ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( (pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) )
27		cbs 14479	. . . . . 6 class Base
28	14, 27	cfv 5579	. . . . 5 class ( Base ` g )
29	28	cword 12487	. . . 4 class Word ( Base ` g )
30	26, 4, 29	crab 2811	. . 3 class { w e. Word ( Base ` g ) | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( (pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) }
31	2, 3, 30	cmpt 4498	. 2 class ( 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 ) ) ) ) } )
32	1, 31	wceq 1374	1 wff ∟G = ( 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 ) ) ) ) } )

This definition is referenced by:  israg  23775