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

Definition df-rag 26592
 Description: Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 26595. (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 26591 . 2 class ∟G
2 vg . . 3 setvar 𝑔
3 cvv 3409 . . 3 class V
4 vw . . . . . . . 8 setvar 𝑤
54cv 1537 . . . . . . 7 class 𝑤
6 chash 13745 . . . . . . 7 class
75, 6cfv 6339 . . . . . 6 class (♯‘𝑤)
8 c3 11735 . . . . . 6 class 3
97, 8wceq 1538 . . . . 5 wff (♯‘𝑤) = 3
10 cc0 10580 . . . . . . . 8 class 0
1110, 5cfv 6339 . . . . . . 7 class (𝑤‘0)
12 c2 11734 . . . . . . . 8 class 2
1312, 5cfv 6339 . . . . . . 7 class (𝑤‘2)
142cv 1537 . . . . . . . 8 class 𝑔
15 cds 16637 . . . . . . . 8 class dist
1614, 15cfv 6339 . . . . . . 7 class (dist‘𝑔)
1711, 13, 16co 7155 . . . . . 6 class ((𝑤‘0)(dist‘𝑔)(𝑤‘2))
18 c1 10581 . . . . . . . . . 10 class 1
1918, 5cfv 6339 . . . . . . . . 9 class (𝑤‘1)
20 cmir 26550 . . . . . . . . . 10 class pInvG
2114, 20cfv 6339 . . . . . . . . 9 class (pInvG‘𝑔)
2219, 21cfv 6339 . . . . . . . 8 class ((pInvG‘𝑔)‘(𝑤‘1))
2313, 22cfv 6339 . . . . . . 7 class (((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))
2411, 23, 16co 7155 . . . . . 6 class ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))
2517, 24wceq 1538 . . . . 5 wff ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))
269, 25wa 399 . . . 4 wff ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))
27 cbs 16546 . . . . . 6 class Base
2814, 27cfv 6339 . . . . 5 class (Base‘𝑔)
2928cword 13918 . . . 4 class Word (Base‘𝑔)
3026, 4, 29crab 3074 . . 3 class {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))}
312, 3, 30cmpt 5115 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((♯‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})
321, 31wceq 1538 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  26595
 Copyright terms: Public domain W3C validator