Definition df-cgra 28817

Description: Define the congruence relation between angles. As for triangles we use "words of points". See iscgra 28818 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

Step	Hyp	Ref	Expression
1		ccgra 28816	. 2 class cgrA
2		vg	. . 3 setvar 𝑔
3		cvv 3479	. . 3 class V
4		va	. . . . . . . . . 10 setvar 𝑎
5	4	cv 1538	. . . . . . . . 9 class 𝑎
6		vp	. . . . . . . . . . 11 setvar 𝑝
7	6	cv 1538	. . . . . . . . . 10 class 𝑝
8		cc0 11156	. . . . . . . . . . 11 class 0
9		c3 12323	. . . . . . . . . . 11 class 3
10		cfzo 13695	. . . . . . . . . . 11 class ..^
11	8, 9, 10	co 7432	. . . . . . . . . 10 class (0..^3)
12		cmap 8867	. . . . . . . . . 10 class ↑m
13	7, 11, 12	co 7432	. . . . . . . . 9 class (𝑝 ↑m (0..^3))
14	5, 13	wcel 2107	. . . . . . . 8 wff 𝑎 ∈ (𝑝 ↑m (0..^3))
15		vb	. . . . . . . . . 10 setvar 𝑏
16	15	cv 1538	. . . . . . . . 9 class 𝑏
17	16, 13	wcel 2107	. . . . . . . 8 wff 𝑏 ∈ (𝑝 ↑m (0..^3))
18	14, 17	wa 395	. . . . . . 7 wff (𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3)))
19		vx	. . . . . . . . . . . . 13 setvar 𝑥
20	19	cv 1538	. . . . . . . . . . . 12 class 𝑥
21		c1 11157	. . . . . . . . . . . . 13 class 1
22	21, 16	cfv 6560	. . . . . . . . . . . 12 class (𝑏‘1)
23		vy	. . . . . . . . . . . . 13 setvar 𝑦
24	23	cv 1538	. . . . . . . . . . . 12 class 𝑦
25	20, 22, 24	cs3 14882	. . . . . . . . . . 11 class ⟨“𝑥(𝑏‘1)𝑦”⟩
26	2	cv 1538	. . . . . . . . . . . 12 class 𝑔
27		ccgrg 28519	. . . . . . . . . . . 12 class cgrG
28	26, 27	cfv 6560	. . . . . . . . . . 11 class (cgrG‘𝑔)
29	5, 25, 28	wbr 5142	. . . . . . . . . 10 wff 𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩
30	8, 16	cfv 6560	. . . . . . . . . . 11 class (𝑏‘0)
31		vk	. . . . . . . . . . . . 13 setvar 𝑘
32	31	cv 1538	. . . . . . . . . . . 12 class 𝑘
33	22, 32	cfv 6560	. . . . . . . . . . 11 class (𝑘‘(𝑏‘1))
34	20, 30, 33	wbr 5142	. . . . . . . . . 10 wff 𝑥(𝑘‘(𝑏‘1))(𝑏‘0)
35		c2 12322	. . . . . . . . . . . 12 class 2
36	35, 16	cfv 6560	. . . . . . . . . . 11 class (𝑏‘2)
37	24, 36, 33	wbr 5142	. . . . . . . . . 10 wff 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)
38	29, 34, 37	w3a 1086	. . . . . . . . 9 wff (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
39	38, 23, 7	wrex 3069	. . . . . . . 8 wff ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
40	39, 19, 7	wrex 3069	. . . . . . 7 wff ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))
41	18, 40	wa 395	. . . . . 6 wff ((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
42		chlg 28609	. . . . . . 7 class hlG
43	26, 42	cfv 6560	. . . . . 6 class (hlG‘𝑔)
44	41, 31, 43	wsbc 3787	. . . . 5 wff [(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
45		cbs 17248	. . . . . 6 class Base
46	26, 45	cfv 6560	. . . . 5 class (Base‘𝑔)
47	44, 6, 46	wsbc 3787	. . . 4 wff [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))
48	47, 4, 15	copab 5204	. . 3 class {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}
49	2, 3, 48	cmpt 5224	. 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))})
50	1, 49	wceq 1539	1 wff cgrA = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))})

This definition is referenced by:  iscgra  28818