Definition df-perpg 27057

Description: Define the "perpendicular" relation. Definition 8.11 of [Schwabhauser] p. 59. See isperp 27073. (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 27056	. 2 class ⟂G
2		vg	. . 3 setvar 𝑔
3		cvv 3432	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1538	. . . . . . 7 class 𝑎
6	2	cv 1538	. . . . . . . . 9 class 𝑔
7		clng 26795	. . . . . . . . 9 class LineG
8	6, 7	cfv 6433	. . . . . . . 8 class (LineG‘𝑔)
9	8	crn 5590	. . . . . . 7 class ran (LineG‘𝑔)
10	5, 9	wcel 2106	. . . . . 6 wff 𝑎 ∈ ran (LineG‘𝑔)
11		vb	. . . . . . . 8 setvar 𝑏
12	11	cv 1538	. . . . . . 7 class 𝑏
13	12, 9	wcel 2106	. . . . . 6 wff 𝑏 ∈ ran (LineG‘𝑔)
14	10, 13	wa 396	. . . . 5 wff (𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔))
15		vu	. . . . . . . . . . 11 setvar 𝑢
16	15	cv 1538	. . . . . . . . . 10 class 𝑢
17		vx	. . . . . . . . . . 11 setvar 𝑥
18	17	cv 1538	. . . . . . . . . 10 class 𝑥
19		vv	. . . . . . . . . . 11 setvar 𝑣
20	19	cv 1538	. . . . . . . . . 10 class 𝑣
21	16, 18, 20	cs3 14555	. . . . . . . . 9 class ⟨“𝑢𝑥𝑣”⟩
22		crag 27054	. . . . . . . . . 10 class ∟G
23	6, 22	cfv 6433	. . . . . . . . 9 class (∟G‘𝑔)
24	21, 23	wcel 2106	. . . . . . . 8 wff ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)
25	24, 19, 12	wral 3064	. . . . . . 7 wff ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)
26	25, 15, 5	wral 3064	. . . . . 6 wff ∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)
27	5, 12	cin 3886	. . . . . 6 class (𝑎 ∩ 𝑏)
28	26, 17, 27	wrex 3065	. . . . 5 wff ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)
29	14, 28	wa 396	. . . 4 wff ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))
30	29, 4, 11	copab 5136	. . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))}
31	2, 3, 30	cmpt 5157	. 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))})
32	1, 31	wceq 1539	1 wff ⟂G = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎 ∩ 𝑏)∀𝑢 ∈ 𝑎 ∀𝑣 ∈ 𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))})

This definition is referenced by:  perpln1  27071  perpln2  27072  isperp  27073