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 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cperpg	⊢ ⟂G
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		va	⊢ 𝑎
4		vb	⊢ 𝑏
5	3	cv	⊢ 𝑎
6		clng	⊢ LineG
7	1	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( LineG ‘ 𝑔 )
9	8	crn	⊢ ran ( LineG ‘ 𝑔 )
10	5 9	wcel	⊢ 𝑎 ∈ ran ( LineG ‘ 𝑔 )
11	4	cv	⊢ 𝑏
12	11 9	wcel	⊢ 𝑏 ∈ ran ( LineG ‘ 𝑔 )
13	10 12	wa	⊢ ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) )
14		vx	⊢ 𝑥
15	5 11	cin	⊢ ( 𝑎 ∩ 𝑏 )
16		vu	⊢ 𝑢
17		vv	⊢ 𝑣
18	16	cv	⊢ 𝑢
19	14	cv	⊢ 𝑥
20	17	cv	⊢ 𝑣
21	18 19 20	cs3	⊢ ⟨“ 𝑢 𝑥 𝑣 ”⟩
22		crag	⊢ ∟G
23	7 22	cfv	⊢ ( ∟G ‘ 𝑔 )
24	21 23	wcel	⊢ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 )
25	24 17 11	wral	⊢ ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 )
26	25 16 5	wral	⊢ ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 )
27	26 14 15	wrex	⊢ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 )
28	13 27	wa	⊢ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) )
29	28 3 4	copab	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ) }
30	1 2 29	cmpt	⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ) } )
31	0 30	wceq	⊢ ⟂G = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ∃ 𝑥 ∈ ( 𝑎 ∩ 𝑏 ) ∀ 𝑢 ∈ 𝑎 ∀ 𝑣 ∈ 𝑏 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝑔 ) ) } )