# 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 ${⊢}{⟂}_{𝒢}=\left({g}\in \mathrm{V}⟼\left\{⟨{a},{b}⟩|\left(\left({a}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\wedge {b}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\right)\wedge \exists {x}\in \left({a}\cap {b}\right)\phantom{\rule{.4em}{0ex}}\forall {u}\in {a}\phantom{\rule{.4em}{0ex}}\forall {v}\in {b}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({g}\right)\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cperpg ${class}{⟂}_{𝒢}$
1 vg ${setvar}{g}$
2 cvv ${class}\mathrm{V}$
3 va ${setvar}{a}$
4 vb ${setvar}{b}$
5 3 cv ${setvar}{a}$
6 clng ${class}{Line}_{𝒢}$
7 1 cv ${setvar}{g}$
8 7 6 cfv ${class}{Line}_{𝒢}\left({g}\right)$
9 8 crn ${class}\mathrm{ran}{Line}_{𝒢}\left({g}\right)$
10 5 9 wcel ${wff}{a}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)$
11 4 cv ${setvar}{b}$
12 11 9 wcel ${wff}{b}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)$
13 10 12 wa ${wff}\left({a}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\wedge {b}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\right)$
14 vx ${setvar}{x}$
15 5 11 cin ${class}\left({a}\cap {b}\right)$
16 vu ${setvar}{u}$
17 vv ${setvar}{v}$
18 16 cv ${setvar}{u}$
19 14 cv ${setvar}{x}$
20 17 cv ${setvar}{v}$
21 18 19 20 cs3 ${class}⟨“{u}{x}{v}”⟩$
22 crag ${class}{∟}_{𝒢}$
23 7 22 cfv ${class}{∟}_{𝒢}\left({g}\right)$
24 21 23 wcel ${wff}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({g}\right)$
25 24 17 11 wral ${wff}\forall {v}\in {b}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({g}\right)$
26 25 16 5 wral ${wff}\forall {u}\in {a}\phantom{\rule{.4em}{0ex}}\forall {v}\in {b}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({g}\right)$
27 26 14 15 wrex ${wff}\exists {x}\in \left({a}\cap {b}\right)\phantom{\rule{.4em}{0ex}}\forall {u}\in {a}\phantom{\rule{.4em}{0ex}}\forall {v}\in {b}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({g}\right)$
28 13 27 wa ${wff}\left(\left({a}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\wedge {b}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\right)\wedge \exists {x}\in \left({a}\cap {b}\right)\phantom{\rule{.4em}{0ex}}\forall {u}\in {a}\phantom{\rule{.4em}{0ex}}\forall {v}\in {b}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({g}\right)\right)$
29 28 3 4 copab ${class}\left\{⟨{a},{b}⟩|\left(\left({a}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\wedge {b}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\right)\wedge \exists {x}\in \left({a}\cap {b}\right)\phantom{\rule{.4em}{0ex}}\forall {u}\in {a}\phantom{\rule{.4em}{0ex}}\forall {v}\in {b}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({g}\right)\right)\right\}$
30 1 2 29 cmpt ${class}\left({g}\in \mathrm{V}⟼\left\{⟨{a},{b}⟩|\left(\left({a}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\wedge {b}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\right)\wedge \exists {x}\in \left({a}\cap {b}\right)\phantom{\rule{.4em}{0ex}}\forall {u}\in {a}\phantom{\rule{.4em}{0ex}}\forall {v}\in {b}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({g}\right)\right)\right\}\right)$
31 0 30 wceq ${wff}{⟂}_{𝒢}=\left({g}\in \mathrm{V}⟼\left\{⟨{a},{b}⟩|\left(\left({a}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\wedge {b}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)\right)\wedge \exists {x}\in \left({a}\cap {b}\right)\phantom{\rule{.4em}{0ex}}\forall {u}\in {a}\phantom{\rule{.4em}{0ex}}\forall {v}\in {b}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({g}\right)\right)\right\}\right)$