Metamath Proof Explorer

Definition 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 ∈ V ⟼ w ∈ Word Base g | w = 3 ∧ w ⁡ 0 dist ⁡ g w ⁡ 2 = w ⁡ 0 dist ⁡ g pInv 𝒢 ⁡ g ⁡ w ⁡ 1 ⁡ w ⁡ 2

Detailed syntax breakdown

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 ∧ w ⁡ 0 dist ⁡ g w ⁡ 2 = w ⁡ 0 dist ⁡ g pInv 𝒢 ⁡ g ⁡ w ⁡ 1 ⁡ w ⁡ 2
29 28 3 7 crab class w ∈ Word Base g | w = 3 ∧ w ⁡ 0 dist ⁡ g w ⁡ 2 = w ⁡ 0 dist ⁡ g pInv 𝒢 ⁡ g ⁡ w ⁡ 1 ⁡ w ⁡ 2
30 1 2 29 cmpt class g ∈ V ⟼ w ∈ Word Base g | w = 3 ∧ w ⁡ 0 dist ⁡ g w ⁡ 2 = w ⁡ 0 dist ⁡ g pInv 𝒢 ⁡ g ⁡ w ⁡ 1 ⁡ w ⁡ 2
31 0 30 wceq wff ∟ 𝒢 = g ∈ V ⟼ w ∈ Word Base g | w = 3 ∧ w ⁡ 0 dist ⁡ g w ⁡ 2 = w ⁡ 0 dist ⁡ g pInv 𝒢 ⁡ g ⁡ w ⁡ 1 ⁡ w ⁡ 2