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	⊢ ∟G = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Base ‘ 𝑔 ) ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crag	⊢ ∟G
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		cbs	⊢ Base
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Base ‘ 𝑔 )
7	6	cword	⊢ Word ( Base ‘ 𝑔 )
8		chash	⊢ ♯
9	3	cv	⊢ 𝑤
10	9 8	cfv	⊢ ( ♯ ‘ 𝑤 )
11		c3	⊢ 3
12	10 11	wceq	⊢ ( ♯ ‘ 𝑤 ) = 3
13		cc0	⊢ 0
14	13 9	cfv	⊢ ( 𝑤 ‘ 0 )
15		cds	⊢ dist
16	5 15	cfv	⊢ ( dist ‘ 𝑔 )
17		c2	⊢ 2
18	17 9	cfv	⊢ ( 𝑤 ‘ 2 )
19	14 18 16	co	⊢ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) )
20		cmir	⊢ pInvG
21	5 20	cfv	⊢ ( pInvG ‘ 𝑔 )
22		c1	⊢ 1
23	22 9	cfv	⊢ ( 𝑤 ‘ 1 )
24	23 21	cfv	⊢ ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) )
25	18 24	cfv	⊢ ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) )
26	14 25 16	co	⊢ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) )
27	19 26	wceq	⊢ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) )
28	12 27	wa	⊢ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) )
29	28 3 7	crab	⊢ { 𝑤 ∈ Word ( Base ‘ 𝑔 ) ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) }
30	1 2 29	cmpt	⊢ ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Base ‘ 𝑔 ) ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } )
31	0 30	wceq	⊢ ∟G = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Base ‘ 𝑔 ) ∣ ( ( ♯ ‘ 𝑤 ) = 3 ∧ ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( 𝑤 ‘ 2 ) ) = ( ( 𝑤 ‘ 0 ) ( dist ‘ 𝑔 ) ( ( ( pInvG ‘ 𝑔 ) ‘ ( 𝑤 ‘ 1 ) ) ‘ ( 𝑤 ‘ 2 ) ) ) ) } )