Definition df-perpg 25591

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

Assertion

Ref	Expression
df-perpg	|- ⟂G = ( g e. _V |-> { <. a , b >. | ( ( a e. ran (LineG ` g ) /\ b e. ran (LineG ` g ) ) /\ E. x e. ( a i^i b ) A. u e. a A. v e. b <" u x v "> e. (∟G ` g ) ) } )

Distinct variable group:   a, b, u, v, x, g

Detailed syntax breakdown of Definition df-perpg

Step	Hyp	Ref	Expression
1		cperpg 25590	. 2 class ⟂G
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		va	. . . . . . . 8 setvar a
5	4	cv 1482	. . . . . . 7 class a
6	2	cv 1482	. . . . . . . . 9 class g
7		clng 25336	. . . . . . . . 9 class LineG
8	6, 7	cfv 5888	. . . . . . . 8 class (LineG ` g )
9	8	crn 5115	. . . . . . 7 class ran (LineG ` g )
10	5, 9	wcel 1990	. . . . . 6 wff a e. ran (LineG ` g )
11		vb	. . . . . . . 8 setvar b
12	11	cv 1482	. . . . . . 7 class b
13	12, 9	wcel 1990	. . . . . 6 wff b e. ran (LineG ` g )
14	10, 13	wa 384	. . . . 5 wff ( a e. ran (LineG ` g ) /\ b e. ran (LineG ` g ) )
15		vu	. . . . . . . . . . 11 setvar u
16	15	cv 1482	. . . . . . . . . 10 class u
17		vx	. . . . . . . . . . 11 setvar x
18	17	cv 1482	. . . . . . . . . 10 class x
19		vv	. . . . . . . . . . 11 setvar v
20	19	cv 1482	. . . . . . . . . 10 class v
21	16, 18, 20	cs3 13587	. . . . . . . . 9 class <" u x v ">
22		crag 25588	. . . . . . . . . 10 class ∟G
23	6, 22	cfv 5888	. . . . . . . . 9 class (∟G ` g )
24	21, 23	wcel 1990	. . . . . . . 8 wff <" u x v "> e. (∟G ` g )
25	24, 19, 12	wral 2912	. . . . . . 7 wff A. v e. b <" u x v "> e. (∟G ` g )
26	25, 15, 5	wral 2912	. . . . . 6 wff A. u e. a A. v e. b <" u x v "> e. (∟G ` g )
27	5, 12	cin 3573	. . . . . 6 class ( a i^i b )
28	26, 17, 27	wrex 2913	. . . . 5 wff E. x e. ( a i^i b ) A. u e. a A. v e. b <" u x v "> e. (∟G ` g )
29	14, 28	wa 384	. . . 4 wff ( ( a e. ran (LineG ` g ) /\ b e. ran (LineG ` g ) ) /\ E. x e. ( a i^i b ) A. u e. a A. v e. b <" u x v "> e. (∟G ` g ) )
30	29, 4, 11	copab 4712	. . 3 class { <. a , b >. | ( ( a e. ran (LineG ` g ) /\ b e. ran (LineG ` g ) ) /\ E. x e. ( a i^i b ) A. u e. a A. v e. b <" u x v "> e. (∟G ` g ) ) }
31	2, 3, 30	cmpt 4729	. 2 class ( g e. _V |-> { <. a , b >. | ( ( a e. ran (LineG ` g ) /\ b e. ran (LineG ` g ) ) /\ E. x e. ( a i^i b ) A. u e. a A. v e. b <" u x v "> e. (∟G ` g ) ) } )
32	1, 31	wceq 1483	1 wff ⟂G = ( g e. _V |-> { <. a , b >. | ( ( a e. ran (LineG ` g ) /\ b e. ran (LineG ` g ) ) /\ E. x e. ( a i^i b ) A. u e. a A. v e. b <" u x v "> e. (∟G ` g ) ) } )

This definition is referenced by:  perpln1  25605  perpln2  25606  isperp  25607