Metamath Proof Explorer

Definition df-perpg

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

Ref Expression
Assertion df-perpg ⊢⟂𝒢=g∈V⟼ab|a∈ran⁡Line𝒢⁡g∧b∈ran⁡Line𝒢⁡g∧∃x∈a∩b∀u∈a∀v∈b⟨“uxv”⟩∈∟𝒢⁡g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cperpg class⟂𝒢
1 vg setvarg
2 cvv classV
3 va setvara
4 vb setvarb
5 3 cv setvara
6 clng classLine𝒢
7 1 cv setvarg
8 7 6 cfv classLine𝒢⁡g
9 8 crn classran⁡Line𝒢⁡g
10 5 9 wcel wffa∈ran⁡Line𝒢⁡g
11 4 cv setvarb
12 11 9 wcel wffb∈ran⁡Line𝒢⁡g
13 10 12 wa wffa∈ran⁡Line𝒢⁡g∧b∈ran⁡Line𝒢⁡g
14 vx setvarx
15 5 11 cin classa∩b
16 vu setvaru
17 vv setvarv
18 16 cv setvaru
19 14 cv setvarx
20 17 cv setvarv
21 18 19 20 cs3 class⟨“uxv”⟩
22 crag class∟𝒢
23 7 22 cfv class∟𝒢⁡g
24 21 23 wcel wff⟨“uxv”⟩∈∟𝒢⁡g
25 24 17 11 wral wff∀v∈b⟨“uxv”⟩∈∟𝒢⁡g
26 25 16 5 wral wff∀u∈a∀v∈b⟨“uxv”⟩∈∟𝒢⁡g
27 26 14 15 wrex wff∃x∈a∩b∀u∈a∀v∈b⟨“uxv”⟩∈∟𝒢⁡g
28 13 27 wa wffa∈ran⁡Line𝒢⁡g∧b∈ran⁡Line𝒢⁡g∧∃x∈a∩b∀u∈a∀v∈b⟨“uxv”⟩∈∟𝒢⁡g
29 28 3 4 copab classab|a∈ran⁡Line𝒢⁡g∧b∈ran⁡Line𝒢⁡g∧∃x∈a∩b∀u∈a∀v∈b⟨“uxv”⟩∈∟𝒢⁡g
30 1 2 29 cmpt classg∈V⟼ab|a∈ran⁡Line𝒢⁡g∧b∈ran⁡Line𝒢⁡g∧∃x∈a∩b∀u∈a∀v∈b⟨“uxv”⟩∈∟𝒢⁡g
31 0 30 wceq wff⟂𝒢=g∈V⟼ab|a∈ran⁡Line𝒢⁡g∧b∈ran⁡Line𝒢⁡g∧∃x∈a∩b∀u∈a∀v∈b⟨“uxv”⟩∈∟𝒢⁡g