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

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

Detailed syntax breakdown of Definition df-cgra
StepHypRef Expression
1 ccgra 25744 . 2 class cgrA
2 vg . . 3 setvar 𝑔
3 cvv 3231 . . 3 class V
4 va . . . . . . . . . 10 setvar 𝑎
54cv 1522 . . . . . . . . 9 class 𝑎
6 vp . . . . . . . . . . 11 setvar 𝑝
76cv 1522 . . . . . . . . . 10 class 𝑝
8 cc0 9974 . . . . . . . . . . 11 class 0
9 c3 11109 . . . . . . . . . . 11 class 3
10 cfzo 12504 . . . . . . . . . . 11 class ..^
118, 9, 10co 6690 . . . . . . . . . 10 class (0..^3)
12 cmap 7899 . . . . . . . . . 10 class 𝑚
137, 11, 12co 6690 . . . . . . . . 9 class (𝑝𝑚 (0..^3))
145, 13wcel 2030 . . . . . . . 8 wff 𝑎 ∈ (𝑝𝑚 (0..^3))
15 vb . . . . . . . . . 10 setvar 𝑏
1615cv 1522 . . . . . . . . 9 class 𝑏
1716, 13wcel 2030 . . . . . . . 8 wff 𝑏 ∈ (𝑝𝑚 (0..^3))
1814, 17wa 383 . . . . . . 7 wff (𝑎 ∈ (𝑝𝑚 (0..^3)) ∧ 𝑏 ∈ (𝑝𝑚 (0..^3)))
19 vx . . . . . . . . . . . . 13 setvar 𝑥
2019cv 1522 . . . . . . . . . . . 12 class 𝑥
21 c1 9975 . . . . . . . . . . . . 13 class 1
2221, 16cfv 5926 . . . . . . . . . . . 12 class (𝑏‘1)
23 vy . . . . . . . . . . . . 13 setvar 𝑦
2423cv 1522 . . . . . . . . . . . 12 class 𝑦
2520, 22, 24cs3 13633 . . . . . . . . . . 11 class ⟨“𝑥(𝑏‘1)𝑦”⟩
262cv 1522 . . . . . . . . . . . 12 class 𝑔
27 ccgrg 25450 . . . . . . . . . . . 12 class cgrG
2826, 27cfv 5926 . . . . . . . . . . 11 class (cgrG‘𝑔)
295, 25, 28wbr 4685 . . . . . . . . . 10 wff 𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩
308, 16cfv 5926 . . . . . . . . . . 11 class (𝑏‘0)
31 vk . . . . . . . . . . . . 13 setvar 𝑘
3231cv 1522 . . . . . . . . . . . 12 class 𝑘
3322, 32cfv 5926 . . . . . . . . . . 11 class (𝑘‘(𝑏‘1))
3420, 30, 33wbr 4685 . . . . . . . . . 10 wff 𝑥(𝑘‘(𝑏‘1))(𝑏‘0)
35 c2 11108 . . . . . . . . . . . 12 class 2
3635, 16cfv 5926 . . . . . . . . . . 11 class (𝑏‘2)
3724, 36, 33wbr 4685 . . . . . . . . . 10 wff 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)
3829, 34, 37w3a 1054 . . . . . . . . 9 wff (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
3938, 23, 7wrex 2942 . . . . . . . 8 wff 𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
4039, 19, 7wrex 2942 . . . . . . 7 wff 𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
4118, 40wa 383 . . . . . 6 wff ((𝑎 ∈ (𝑝𝑚 (0..^3)) ∧ 𝑏 ∈ (𝑝𝑚 (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
42 chlg 25540 . . . . . . 7 class hlG
4326, 42cfv 5926 . . . . . 6 class (hlG‘𝑔)
4441, 31, 43wsbc 3468 . . . . 5 wff [(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝𝑚 (0..^3)) ∧ 𝑏 ∈ (𝑝𝑚 (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
45 cbs 15904 . . . . . 6 class Base
4626, 45cfv 5926 . . . . 5 class (Base‘𝑔)
4744, 6, 46wsbc 3468 . . . 4 wff [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝𝑚 (0..^3)) ∧ 𝑏 ∈ (𝑝𝑚 (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
4847, 4, 15copab 4745 . . 3 class {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝𝑚 (0..^3)) ∧ 𝑏 ∈ (𝑝𝑚 (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}
492, 3, 48cmpt 4762 . 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝𝑚 (0..^3)) ∧ 𝑏 ∈ (𝑝𝑚 (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))})
501, 49wceq 1523 1 wff cgrA = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝𝑚 (0..^3)) ∧ 𝑏 ∈ (𝑝𝑚 (0..^3))) ∧ ∃𝑥𝑝𝑦𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))})
 Colors of variables: wff setvar class This definition is referenced by:  iscgra  25746
 Copyright terms: Public domain W3C validator