Metamath Proof Explorer

Theorem perpcom

Description: The "perpendicular" relation commutes. Theorem 8.12 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019)

Ref Expression
Hypotheses isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isperp.d ⊢ − = ( dist ‘ 𝐺 )
isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
isperp.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
perpcom.1 ⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
Assertion perpcom ( 𝜑 → 𝐵 ( ⟂G ‘ 𝐺 ) 𝐴 )

Proof

Step Hyp Ref Expression
1 isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isperp.d ⊢ − = ( dist ‘ 𝐺 )
3 isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7 isperp.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
8 perpcom.1 ⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
9 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
10 9 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 ) )
11 ralcom ⊢ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐴 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
12 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
13 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝐺 ∈ TarskiG )
14 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝐴 ∈ ran 𝐿 )
15 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑢 ∈ 𝐴 )
16 1 4 3 13 14 15 tglnpt ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑢 ∈ 𝑃 )
17 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
18 17 elin1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑥 ∈ 𝐴 )
19 1 4 3 13 14 18 tglnpt ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑥 ∈ 𝑃 )
20 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝐵 ∈ ran 𝐿 )
21 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑣 ∈ 𝐵 )
22 1 4 3 13 20 21 tglnpt ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑣 ∈ 𝑃 )
23 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
24 1 2 3 4 12 13 16 19 22 23 ragcom ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
25 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝐺 ∈ TarskiG )
26 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝐵 ∈ ran 𝐿 )
27 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑣 ∈ 𝐵 )
28 1 4 3 25 26 27 tglnpt ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑣 ∈ 𝑃 )
29 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝐴 ∈ ran 𝐿 )
30 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
31 30 elin1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑥 ∈ 𝐴 )
32 1 4 3 25 29 31 tglnpt ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑥 ∈ 𝑃 )
33 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑢 ∈ 𝐴 )
34 1 4 3 25 29 33 tglnpt ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝑢 ∈ 𝑃 )
35 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
36 1 2 3 4 12 25 28 32 34 35 ragcom ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) ∧ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
37 24 36 impbida ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) → ( ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
38 37 2ralbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐴 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐴 ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
39 11 38 syl5bb ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐴 ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
40 10 39 rexeqbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ( 𝐵 ∩ 𝐴 ) ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐴 ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
41 1 2 3 4 5 6 7 isperp ⊢ ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
42 1 2 3 4 5 7 6 isperp ⊢ ( 𝜑 → ( 𝐵 ( ⟂G ‘ 𝐺 ) 𝐴 ↔ ∃ 𝑥 ∈ ( 𝐵 ∩ 𝐴 ) ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐴 ⟨“ 𝑣 𝑥 𝑢 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
43 40 41 42 3bitr4d ⊢ ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ 𝐵 ( ⟂G ‘ 𝐺 ) 𝐴 ) )
44 8 43 mpbid ⊢ ( 𝜑 → 𝐵 ( ⟂G ‘ 𝐺 ) 𝐴 )