# 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 ${⊢}{P}={\mathrm{Base}}_{{G}}$
isperp.d
isperp.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
isperp.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
isperp.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
isperp.a ${⊢}{\phi }\to {A}\in \mathrm{ran}{L}$
isperp.b ${⊢}{\phi }\to {B}\in \mathrm{ran}{L}$
perpcom.1 ${⊢}{\phi }\to {A}{⟂}_{𝒢}\left({G}\right){B}$
Assertion perpcom ${⊢}{\phi }\to {B}{⟂}_{𝒢}\left({G}\right){A}$

### Proof

Step Hyp Ref Expression
1 isperp.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 isperp.d
3 isperp.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 isperp.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
5 isperp.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
6 isperp.a ${⊢}{\phi }\to {A}\in \mathrm{ran}{L}$
7 isperp.b ${⊢}{\phi }\to {B}\in \mathrm{ran}{L}$
8 perpcom.1 ${⊢}{\phi }\to {A}{⟂}_{𝒢}\left({G}\right){B}$
9 incom ${⊢}{A}\cap {B}={B}\cap {A}$
10 9 a1i ${⊢}{\phi }\to {A}\cap {B}={B}\cap {A}$
11 ralcom ${⊢}\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)↔\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)$
12 eqid ${⊢}{pInv}_{𝒢}\left({G}\right)={pInv}_{𝒢}\left({G}\right)$
13 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
14 6 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {A}\in \mathrm{ran}{L}$
15 simplrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {u}\in {A}$
16 1 4 3 13 14 15 tglnpt ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {u}\in {P}$
17 simpllr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {x}\in \left({A}\cap {B}\right)$
18 17 elin1d ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {x}\in {A}$
19 1 4 3 13 14 18 tglnpt ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {x}\in {P}$
20 7 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {B}\in \mathrm{ran}{L}$
21 simplrl ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {v}\in {B}$
22 1 4 3 13 20 21 tglnpt ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {v}\in {P}$
23 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)$
24 1 2 3 4 12 13 16 19 22 23 ragcom ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)$
25 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
26 7 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {B}\in \mathrm{ran}{L}$
27 simplrl ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {v}\in {B}$
28 1 4 3 25 26 27 tglnpt ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {v}\in {P}$
29 6 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {A}\in \mathrm{ran}{L}$
30 simpllr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {x}\in \left({A}\cap {B}\right)$
31 30 elin1d ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {x}\in {A}$
32 1 4 3 25 29 31 tglnpt ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {x}\in {P}$
33 simplrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {u}\in {A}$
34 1 4 3 25 29 33 tglnpt ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to {u}\in {P}$
35 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)$
36 1 2 3 4 12 25 28 32 34 35 ragcom ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\wedge ⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)\to ⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)$
37 24 36 impbida ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\wedge \left({v}\in {B}\wedge {u}\in {A}\right)\right)\to \left(⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)↔⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)$
38 37 2ralbidva ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\to \left(\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)↔\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)$
39 11 38 syl5bb ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap {B}\right)\right)\to \left(\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}⟨“{u}{x}{v}”⟩\in {∟}_{𝒢}\left({G}\right)↔\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)$
40 10 39 rexeqbidva ${⊢}{\phi }\to \left(\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)↔\exists {x}\in \left({B}\cap {A}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)$
41 1 2 3 4 5 6 7 isperp ${⊢}{\phi }\to \left({A}{⟂}_{𝒢}\left({G}\right){B}↔\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)$
42 1 2 3 4 5 7 6 isperp ${⊢}{\phi }\to \left({B}{⟂}_{𝒢}\left({G}\right){A}↔\exists {x}\in \left({B}\cap {A}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in {B}\phantom{\rule{.4em}{0ex}}\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}⟨“{v}{x}{u}”⟩\in {∟}_{𝒢}\left({G}\right)\right)$
43 40 41 42 3bitr4d ${⊢}{\phi }\to \left({A}{⟂}_{𝒢}\left({G}\right){B}↔{B}{⟂}_{𝒢}\left({G}\right){A}\right)$
44 8 43 mpbid ${⊢}{\phi }\to {B}{⟂}_{𝒢}\left({G}\right){A}$