Definition 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	⊢ cgrA = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( hlG ‘ 𝑔 ) / 𝑘 ] ( ( 𝑎 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑎 ( cgrG ‘ 𝑔 ) ⟨“ 𝑥 ( 𝑏 ‘ 1 ) 𝑦 ”⟩ ∧ 𝑥 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 0 ) ∧ 𝑦 ( 𝑘 ‘ ( 𝑏 ‘ 1 ) ) ( 𝑏 ‘ 2 ) ) ) } )

Detailed syntax breakdown

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