df-cgra

Description: Define the congruence relation between angles. As for triangles we use "words of points". See iscgra for a more human readable version. (Contributed by Thierry Arnoux, 30-Jul-2020)

		Ref	Expression
	Assertion	df-cgra	$⊢ \sim_{𝒢}^{∠} = (g \in V ⟼ \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccgra	$class \sim_{𝒢}^{∠}$
1		vg	$setvar g$
2		cvv	$class V$
3		va	$setvar a$
4		vb	$setvar b$
5		cbs	$class Base$
6	1	cv	$setvar g$
7	6 5	cfv	$class {Base}_{g}$
8		vp	$setvar p$
9		chlg	$class {hl}_{𝒢}$
10	6 9	cfv	$class {hl}_{𝒢} (g)$
11		vk	$setvar k$
12	3	cv	$setvar a$
13	8	cv	$setvar p$
14		cmap	$class ↑_{𝑚}$
15		cc0	$class 0$
16		cfzo	$class ..^$
17		c3	$class 3$
18	15 17 16	co	$class (0 ..^3)$
19	13 18 14	co	$class (p^{(0 ..^3)})$
20	12 19	wcel	$wff a \in (p^{(0 ..^3)})$
21	4	cv	$setvar b$
22	21 19	wcel	$wff b \in (p^{(0 ..^3)})$
23	20 22	wa	$wff (a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)}))$
24		vx	$setvar x$
25		vy	$setvar y$
26		ccgrg	$class \sim_{𝒢}$
27	6 26	cfv	$class \sim_{𝒢} (g)$
28	24	cv	$setvar x$
29		c1	$class 1$
30	29 21	cfv	$class b (1)$
31	25	cv	$setvar y$
32	28 30 31	cs3	$class ⟨“ x b (1) y ”⟩$
33	12 32 27	wbr	$wff a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩$
34	11	cv	$setvar k$
35	30 34	cfv	$class k (b (1))$
36	15 21	cfv	$class b (0)$
37	28 36 35	wbr	$wff x k (b (1)) b (0)$
38		c2	$class 2$
39	38 21	cfv	$class b (2)$
40	31 39 35	wbr	$wff y k (b (1)) b (2)$
41	33 37 40	w3a	$wff (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2))$
42	41 25 13	wrex	$wff \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2))$
43	42 24 13	wrex	$wff \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2))$
44	23 43	wa	$wff ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))$
45	44 11 10	wsbc	$wff \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))$
46	45 8 7	wsbc	$wff \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))$
47	46 3 4	copab	$class \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))\}$
48	1 2 47	cmpt	$class (g \in V ⟼ \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))\})$
49	0 48	wceq	$wff \sim_{𝒢}^{∠} = (g \in V ⟼ \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} {hl}_{𝒢} (g) / k \underset{˙}{]} ((a \in (p^{(0 ..^3)}) \land b \in (p^{(0 ..^3)})) \land \exists x \in p \exists y \in p (a \sim_{𝒢} (g) ⟨“ x b (1) y ”⟩ \land x k (b (1)) b (0) \land y k (b (1)) b (2)))\})$

Metamath Proof Explorer

Definition df-cgra

Detailed syntax breakdown