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 25307
Description: Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 25310. (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 25306 . 2 class ∟G
2 vg . . 3 setvar 𝑔
3 cvv 3172 . . 3 class V
4 vw . . . . . . . 8 setvar 𝑤
54cv 1473 . . . . . . 7 class 𝑤
6 chash 12934 . . . . . . 7 class #
75, 6cfv 5790 . . . . . 6 class (#‘𝑤)
8 c3 10918 . . . . . 6 class 3
97, 8wceq 1474 . . . . 5 wff (#‘𝑤) = 3
10 cc0 9792 . . . . . . . 8 class 0
1110, 5cfv 5790 . . . . . . 7 class (𝑤‘0)
12 c2 10917 . . . . . . . 8 class 2
1312, 5cfv 5790 . . . . . . 7 class (𝑤‘2)
142cv 1473 . . . . . . . 8 class 𝑔
15 cds 15723 . . . . . . . 8 class dist
1614, 15cfv 5790 . . . . . . 7 class (dist‘𝑔)
1711, 13, 16co 6527 . . . . . 6 class ((𝑤‘0)(dist‘𝑔)(𝑤‘2))
18 c1 9793 . . . . . . . . . 10 class 1
1918, 5cfv 5790 . . . . . . . . 9 class (𝑤‘1)
20 cmir 25265 . . . . . . . . . 10 class pInvG
2114, 20cfv 5790 . . . . . . . . 9 class (pInvG‘𝑔)
2219, 21cfv 5790 . . . . . . . 8 class ((pInvG‘𝑔)‘(𝑤‘1))
2313, 22cfv 5790 . . . . . . 7 class (((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))
2411, 23, 16co 6527 . . . . . 6 class ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))
2517, 24wceq 1474 . . . . 5 wff ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2)))
269, 25wa 382 . . . 4 wff ((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))
27 cbs 15641 . . . . . 6 class Base
2814, 27cfv 5790 . . . . 5 class (Base‘𝑔)
2928cword 13092 . . . 4 class Word (Base‘𝑔)
3026, 4, 29crab 2899 . . 3 class {𝑤 ∈ Word (Base‘𝑔) ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))}
312, 3, 30cmpt 4637 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Base‘𝑔) ∣ ((#‘𝑤) = 3 ∧ ((𝑤‘0)(dist‘𝑔)(𝑤‘2)) = ((𝑤‘0)(dist‘𝑔)(((pInvG‘𝑔)‘(𝑤‘1))‘(𝑤‘2))))})
321, 31wceq 1474 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  25310
  Copyright terms: Public domain W3C validator