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

Definition df-cgra 27167
Description: Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 27168 for a more human readable version. (Contributed by Thierry Arnoux, 30-Jul-2020.)
Assertion
Ref Expression
df-cgra cgrA = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))})
Distinct variable group:   𝑎,𝑏,𝑔,𝑘,𝑝,𝑥,𝑦

Detailed syntax breakdown of Definition df-cgra
StepHypRef Expression
1 ccgra 27166 . 2 class cgrA
2 vg . . 3 setvar 𝑔
3 cvv 3431 . . 3 class V
4 va . . . . . . . . . 10 setvar 𝑎
54cv 1541 . . . . . . . . 9 class 𝑎
6 vp . . . . . . . . . . 11 setvar 𝑝
76cv 1541 . . . . . . . . . 10 class 𝑝
8 cc0 10872 . . . . . . . . . . 11 class 0
9 c3 12029 . . . . . . . . . . 11 class 3
10 cfzo 13381 . . . . . . . . . . 11 class ..^
118, 9, 10co 7271 . . . . . . . . . 10 class (0..^3)
12 cmap 8598 . . . . . . . . . 10 class m
137, 11, 12co 7271 . . . . . . . . 9 class (𝑝m (0..^3))
145, 13wcel 2110 . . . . . . . 8 wff 𝑎 ∈ (𝑝m (0..^3))
15 vb . . . . . . . . . 10 setvar 𝑏
1615cv 1541 . . . . . . . . 9 class 𝑏
1716, 13wcel 2110 . . . . . . . 8 wff 𝑏 ∈ (𝑝m (0..^3))
1814, 17wa 396 . . . . . . 7 wff (𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3)))
19 vx . . . . . . . . . . . . 13 setvar 𝑥
2019cv 1541 . . . . . . . . . . . 12 class 𝑥
21 c1 10873 . . . . . . . . . . . . 13 class 1
2221, 16cfv 6432 . . . . . . . . . . . 12 class (𝑏‘1)
23 vy . . . . . . . . . . . . 13 setvar 𝑦
2423cv 1541 . . . . . . . . . . . 12 class 𝑦
2520, 22, 24cs3 14553 . . . . . . . . . . 11 class ⟨“𝑥(𝑏‘1)𝑦”⟩
262cv 1541 . . . . . . . . . . . 12 class 𝑔
27 ccgrg 26869 . . . . . . . . . . . 12 class cgrG
2826, 27cfv 6432 . . . . . . . . . . 11 class (cgrG‘𝑔)
295, 25, 28wbr 5079 . . . . . . . . . 10 wff 𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩
308, 16cfv 6432 . . . . . . . . . . 11 class (𝑏‘0)
31 vk . . . . . . . . . . . . 13 setvar 𝑘
3231cv 1541 . . . . . . . . . . . 12 class 𝑘
3322, 32cfv 6432 . . . . . . . . . . 11 class (𝑘‘(𝑏‘1))
3420, 30, 33wbr 5079 . . . . . . . . . 10 wff 𝑥(𝑘‘(𝑏‘1))(𝑏‘0)
35 c2 12028 . . . . . . . . . . . 12 class 2
3635, 16cfv 6432 . . . . . . . . . . 11 class (𝑏‘2)
3724, 36, 33wbr 5079 . . . . . . . . . 10 wff 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)
3829, 34, 37w3a 1086 . . . . . . . . 9 wff (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
3938, 23, 7wrex 3067 . . . . . . . 8 wff 𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
4039, 19, 7wrex 3067 . . . . . . 7 wff 𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
4118, 40wa 396 . . . . . 6 wff ((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
42 chlg 26959 . . . . . . 7 class hlG
4326, 42cfv 6432 . . . . . 6 class (hlG‘𝑔)
4441, 31, 43wsbc 3720 . . . . 5 wff [(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
45 cbs 16910 . . . . . 6 class Base
4626, 45cfv 6432 . . . . 5 class (Base‘𝑔)
4744, 6, 46wsbc 3720 . . . 4 wff [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
4847, 4, 15copab 5141 . . 3 class {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}
492, 3, 48cmpt 5162 . 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))})
501, 49wceq 1542 1 wff cgrA = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))})
Colors of variables: wff setvar class
This definition is referenced by:  iscgra  27168
  Copyright terms: Public domain W3C validator