Definition df-rag 25389

Description: Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 25392. (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 25388	. 2 class ∟G
2		vg	. . 3 setvar 𝑔
3		cvv 3173	. . 3 class V
4		vw	. . . . . . . 8 setvar 𝑤
5	4	cv 1474	. . . . . . 7 class 𝑤
6		chash 12979	. . . . . . 7 class #
7	5, 6	cfv 5804	. . . . . 6 class (#‘𝑤)
8		c3 10948	. . . . . 6 class 3
9	7, 8	wceq 1475	. . . . 5 wff (#‘𝑤) = 3
10		cc0 9815	. . . . . . . 8 class 0
11	10, 5	cfv 5804	. . . . . . 7 class (𝑤‘0)
12		c2 10947	. . . . . . . 8 class 2
13	12, 5	cfv 5804	. . . . . . 7 class (𝑤‘2)
14	2	cv 1474	. . . . . . . 8 class 𝑔
15		cds 15777	. . . . . . . 8 class dist
16	14, 15	cfv 5804	. . . . . . 7 class (dist‘𝑔)
17	11, 13, 16	co 6549	. . . . . 6 class ((𝑤‘0)(dist‘𝑔)(𝑤‘2))
18		c1 9816	. . . . . . . . . 10 class 1
19	18, 5	cfv 5804	. . . . . . . . 9 class (𝑤‘1)
20		cmir 25347	. . . . . . . . . 10 class pInvG
21	14, 20	cfv 5804	. . . . . . . . 9 class (pInvG‘𝑔)
22	19, 21	cfv 5804	. . . . . . . 8 class ((pInvG‘𝑔)‘(𝑤‘1))
23	13, 22	cfv 5804	. . . . . . 7 class (((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))
24	11, 23, 16	co 6549	. . . . . 6 class ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))
25	17, 24	wceq 1475	. . . . 5 wff ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))
26	9, 25	wa 383	. . . 4 wff ((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))
27		cbs 15695	. . . . . 6 class Base
28	14, 27	cfv 5804	. . . . 5 class (Base‘𝑔)
29	28	cword 13146	. . . 4 class Word (Base‘𝑔)
30	26, 4, 29	crab 2900	. . 3 class {𝑤 ∈ Word (Base‘𝑔) ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))}
31	2, 3, 30	cmpt 4643	. 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})
32	1, 31	wceq 1475	1 wff ∟G = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})

This definition is referenced by:  israg  25392