MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rag Structured version   Visualization version   GIF version

Definition df-rag 26407
Description: Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 26410. (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
StepHypRef Expression
1 crag 26406 . 2 class ∟G
2 vg . . 3 setvar 𝑔
3 cvv 3492 . . 3 class V
4 vw . . . . . . . 8 setvar 𝑤
54cv 1527 . . . . . . 7 class 𝑤
6 chash 13678 . . . . . . 7 class
75, 6cfv 6348 . . . . . 6 class (♯‘𝑤)
8 c3 11681 . . . . . 6 class 3
97, 8wceq 1528 . . . . 5 wff (♯‘𝑤) = 3
10 cc0 10525 . . . . . . . 8 class 0
1110, 5cfv 6348 . . . . . . 7 class (𝑤‘0)
12 c2 11680 . . . . . . . 8 class 2
1312, 5cfv 6348 . . . . . . 7 class (𝑤‘2)
142cv 1527 . . . . . . . 8 class 𝑔
15 cds 16562 . . . . . . . 8 class dist
1614, 15cfv 6348 . . . . . . 7 class (dist‘𝑔)
1711, 13, 16co 7145 . . . . . 6 class ((𝑤‘0)(dist‘𝑔)(𝑤‘2))
18 c1 10526 . . . . . . . . . 10 class 1
1918, 5cfv 6348 . . . . . . . . 9 class (𝑤‘1)
20 cmir 26365 . . . . . . . . . 10 class pInvG
2114, 20cfv 6348 . . . . . . . . 9 class (pInvG‘𝑔)
2219, 21cfv 6348 . . . . . . . 8 class ((pInvG‘𝑔)‘(𝑤‘1))
2313, 22cfv 6348 . . . . . . 7 class (((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))
2411, 23, 16co 7145 . . . . . 6 class ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))
2517, 24wceq 1528 . . . . 5 wff ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))
269, 25wa 396 . . . 4 wff ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))
27 cbs 16471 . . . . . 6 class Base
2814, 27cfv 6348 . . . . 5 class (Base‘𝑔)
2928cword 13849 . . . 4 class Word (Base‘𝑔)
3026, 4, 29crab 3139 . . 3 class {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))}
312, 3, 30cmpt 5137 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})
321, 31wceq 1528 1 wff ∟G = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})
Colors of variables: wff setvar class
This definition is referenced by:  israg  26410
  Copyright terms: Public domain W3C validator