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

Definition df-cgra 26605
 Description: Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 26606 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 26604 . 2 class cgrA
2 vg . . 3 setvar 𝑔
3 cvv 3480 . . 3 class V
4 va . . . . . . . . . 10 setvar 𝑎
54cv 1537 . . . . . . . . 9 class 𝑎
6 vp . . . . . . . . . . 11 setvar 𝑝
76cv 1537 . . . . . . . . . 10 class 𝑝
8 cc0 10535 . . . . . . . . . . 11 class 0
9 c3 11690 . . . . . . . . . . 11 class 3
10 cfzo 13037 . . . . . . . . . . 11 class ..^
118, 9, 10co 7149 . . . . . . . . . 10 class (0..^3)
12 cmap 8402 . . . . . . . . . 10 class m
137, 11, 12co 7149 . . . . . . . . 9 class (𝑝m (0..^3))
145, 13wcel 2115 . . . . . . . 8 wff 𝑎 ∈ (𝑝m (0..^3))
15 vb . . . . . . . . . 10 setvar 𝑏
1615cv 1537 . . . . . . . . 9 class 𝑏
1716, 13wcel 2115 . . . . . . . 8 wff 𝑏 ∈ (𝑝m (0..^3))
1814, 17wa 399 . . . . . . 7 wff (𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3)))
19 vx . . . . . . . . . . . . 13 setvar 𝑥
2019cv 1537 . . . . . . . . . . . 12 class 𝑥
21 c1 10536 . . . . . . . . . . . . 13 class 1
2221, 16cfv 6343 . . . . . . . . . . . 12 class (𝑏‘1)
23 vy . . . . . . . . . . . . 13 setvar 𝑦
2423cv 1537 . . . . . . . . . . . 12 class 𝑦
2520, 22, 24cs3 14204 . . . . . . . . . . 11 class ⟨“𝑥(𝑏‘1)𝑦”⟩
262cv 1537 . . . . . . . . . . . 12 class 𝑔
27 ccgrg 26307 . . . . . . . . . . . 12 class cgrG
2826, 27cfv 6343 . . . . . . . . . . 11 class (cgrG‘𝑔)
295, 25, 28wbr 5052 . . . . . . . . . 10 wff 𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩
308, 16cfv 6343 . . . . . . . . . . 11 class (𝑏‘0)
31 vk . . . . . . . . . . . . 13 setvar 𝑘
3231cv 1537 . . . . . . . . . . . 12 class 𝑘
3322, 32cfv 6343 . . . . . . . . . . 11 class (𝑘‘(𝑏‘1))
3420, 30, 33wbr 5052 . . . . . . . . . 10 wff 𝑥(𝑘‘(𝑏‘1))(𝑏‘0)
35 c2 11689 . . . . . . . . . . . 12 class 2
3635, 16cfv 6343 . . . . . . . . . . 11 class (𝑏‘2)
3724, 36, 33wbr 5052 . . . . . . . . . 10 wff 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)
3829, 34, 37w3a 1084 . . . . . . . . 9 wff (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
3938, 23, 7wrex 3134 . . . . . . . 8 wff 𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
4039, 19, 7wrex 3134 . . . . . . 7 wff 𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
4118, 40wa 399 . . . . . 6 wff ((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
42 chlg 26397 . . . . . . 7 class hlG
4326, 42cfv 6343 . . . . . 6 class (hlG‘𝑔)
4441, 31, 43wsbc 3758 . . . . 5 wff [(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
45 cbs 16483 . . . . . 6 class Base
4626, 45cfv 6343 . . . . 5 class (Base‘𝑔)
4744, 6, 46wsbc 3758 . . . 4 wff [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
4847, 4, 15copab 5114 . . 3 class {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}
492, 3, 48cmpt 5132 . 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝m (0..^3)) ∧ 𝑏 ∈ (𝑝m (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))})
501, 49wceq 1538 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  26606
 Copyright terms: Public domain W3C validator