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 \in V ⟼ \{w \in Word {Base}_{g} \| (\|w\| = 3 \land w (0) dist (g) w (2) = w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2)))\})$

Step	Hyp	Ref	Expression
0		crag	$class ∟_{𝒢}$
1		vg	$setvar g$
2		cvv	$class V$
3		vw	$setvar w$
4		cbs	$class Base$
5	1	cv	$setvar g$
6	5 4	cfv	$class {Base}_{g}$
7	6	cword	$class Word {Base}_{g}$
8		chash	$class \|.\|$
9	3	cv	$setvar w$
10	9 8	cfv	$class \|w\|$
11		c3	$class 3$
12	10 11	wceq	$wff \|w\| = 3$
13		cc0	$class 0$
14	13 9	cfv	$class w (0)$
15		cds	$class dist$
16	5 15	cfv	$class dist (g)$
17		c2	$class 2$
18	17 9	cfv	$class w (2)$
19	14 18 16	co	$class (w (0) dist (g) w (2))$
20		cmir	$class {pInv}_{𝒢}$
21	5 20	cfv	$class {pInv}_{𝒢} (g)$
22		c1	$class 1$
23	22 9	cfv	$class w (1)$
24	23 21	cfv	$class {pInv}_{𝒢} (g) (w (1))$
25	18 24	cfv	$class {pInv}_{𝒢} (g) (w (1)) (w (2))$
26	14 25 16	co	$class (w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2)))$
27	19 26	wceq	$wff w (0) dist (g) w (2) = w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2))$
28	12 27	wa	$wff (\|w\| = 3 \land w (0) dist (g) w (2) = w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2)))$
29	28 3 7	crab	$class \{w \in Word {Base}_{g} \| (\|w\| = 3 \land w (0) dist (g) w (2) = w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2)))\}$
30	1 2 29	cmpt	$class (g \in V ⟼ \{w \in Word {Base}_{g} \| (\|w\| = 3 \land w (0) dist (g) w (2) = w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2)))\})$
31	0 30	wceq	$wff ∟_{𝒢} = (g \in V ⟼ \{w \in Word {Base}_{g} \| (\|w\| = 3 \land w (0) dist (g) w (2) = w (0) dist (g) {pInv}_{𝒢} (g) (w (1)) (w (2)))\})$

Metamath Proof Explorer