Definition df-perpg 28704

Description: Define the "perpendicular" relation. Definition 8.11 of [Schwabhauser] p. 59. See isperp 28720. (Contributed by Thierry Arnoux, 8-Sep-2019.)

Assertion

Ref	Expression
df-perpg	⊢ ⟂G = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))})

Distinct variable group:   𝑎,𝑏,𝑢,𝑣,𝑥,𝑔

Detailed syntax breakdown of Definition df-perpg

Step	Hyp	Ref	Expression
1		cperpg 28703	. 2 class ⟂G
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1539	. . . . . . 7 class 𝑎
6	2	cv 1539	. . . . . . . . 9 class 𝑔
7		clng 28442	. . . . . . . . 9 class LineG
8	6, 7	cfv 6561	. . . . . . . 8 class (LineG‘𝑔)
9	8	crn 5686	. . . . . . 7 class ran (LineG‘𝑔)
10	5, 9	wcel 2108	. . . . . 6 wff 𝑎 ∈ ran (LineG‘𝑔)
11		vb	. . . . . . . 8 setvar 𝑏
12	11	cv 1539	. . . . . . 7 class 𝑏
13	12, 9	wcel 2108	. . . . . 6 wff 𝑏 ∈ ran (LineG‘𝑔)
14	10, 13	wa 395	. . . . 5 wff (𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔))
15		vu	. . . . . . . . . . 11 setvar 𝑢
16	15	cv 1539	. . . . . . . . . 10 class 𝑢
17		vx	. . . . . . . . . . 11 setvar 𝑥
18	17	cv 1539	. . . . . . . . . 10 class 𝑥
19		vv	. . . . . . . . . . 11 setvar 𝑣
20	19	cv 1539	. . . . . . . . . 10 class 𝑣
21	16, 18, 20	cs3 14881	. . . . . . . . 9 class ⟨“𝑢𝑥𝑣”⟩
22		crag 28701	. . . . . . . . . 10 class ∟G
23	6, 22	cfv 6561	. . . . . . . . 9 class (∟G‘𝑔)
24	21, 23	wcel 2108	. . . . . . . 8 wff ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)
25	24, 19, 12	wral 3061	. . . . . . 7 wff ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)
26	25, 15, 5	wral 3061	. . . . . 6 wff ∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)
27	5, 12	cin 3950	. . . . . 6 class (𝑎 ∩ 𝑏)
28	26, 17, 27	wrex 3070	. . . . 5 wff ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)
29	14, 28	wa 395	. . . 4 wff ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))
30	29, 4, 11	copab 5205	. . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))}
31	2, 3, 30	cmpt 5225	. 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))})
32	1, 31	wceq 1540	1 wff ⟂G = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))})

This definition is referenced by:  perpln1  28718  perpln2  28719  isperp  28720