Definition df-rag 28378

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

Assertion

Ref	Expression
df-rag	⊢ ∟G = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})

Distinct variable group:   𝑤,𝑔

Detailed syntax breakdown of Definition df-rag

Step	Hyp	Ref	Expression
1		crag 28377	. 2 class ∟G
2		vg	. . 3 setvar 𝑔
3		cvv 3473	. . 3 class V
4		vw	. . . . . . . 8 setvar 𝑤
5	4	cv 1539	. . . . . . 7 class 𝑤
6		chash 14297	. . . . . . 7 class ♯
7	5, 6	cfv 6543	. . . . . 6 class (♯‘𝑤)
8		c3 12275	. . . . . 6 class 3
9	7, 8	wceq 1540	. . . . 5 wff (♯‘𝑤) = 3
10		cc0 11116	. . . . . . . 8 class 0
11	10, 5	cfv 6543	. . . . . . 7 class (𝑤‘0)
12		c2 12274	. . . . . . . 8 class 2
13	12, 5	cfv 6543	. . . . . . 7 class (𝑤‘2)
14	2	cv 1539	. . . . . . . 8 class 𝑔
15		cds 17213	. . . . . . . 8 class dist
16	14, 15	cfv 6543	. . . . . . 7 class (dist‘𝑔)
17	11, 13, 16	co 7412	. . . . . 6 class ((𝑤‘0)(dist‘𝑔)(𝑤‘2))
18		c1 11117	. . . . . . . . . 10 class 1
19	18, 5	cfv 6543	. . . . . . . . 9 class (𝑤‘1)
20		cmir 28336	. . . . . . . . . 10 class pInvG
21	14, 20	cfv 6543	. . . . . . . . 9 class (pInvG‘𝑔)
22	19, 21	cfv 6543	. . . . . . . 8 class ((pInvG‘𝑔)‘(𝑤‘1))
23	13, 22	cfv 6543	. . . . . . 7 class (((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))
24	11, 23, 16	co 7412	. . . . . 6 class ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))
25	17, 24	wceq 1540	. . . . 5 wff ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))
26	9, 25	wa 395	. . . 4 wff ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))
27		cbs 17151	. . . . . 6 class Base
28	14, 27	cfv 6543	. . . . 5 class (Base‘𝑔)
29	28	cword 14471	. . . 4 class Word (Base‘𝑔)
30	26, 4, 29	crab 3431	. . 3 class {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))}
31	2, 3, 30	cmpt 5231	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})
32	1, 31	wceq 1540	1 wff ∟G = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})

This definition is referenced by:  israg  28381