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=BaseG
isperp.d -˙=distG
isperp.i I=ItvG
isperp.l L=Line𝒢G
isperp.g φG𝒢Tarski
isperp.a φAranL
isperp.b φBranL
perpcom.1 φA𝒢GB
Assertion perpcom φB𝒢GA

Proof

Step Hyp Ref Expression
1 isperp.p P=BaseG
2 isperp.d -˙=distG
3 isperp.i I=ItvG
4 isperp.l L=Line𝒢G
5 isperp.g φG𝒢Tarski
6 isperp.a φAranL
7 isperp.b φBranL
8 perpcom.1 φA𝒢GB
9 incom AB=BA
10 9 a1i φAB=BA
11 ralcom uAvB⟨“uxv”⟩𝒢GvBuA⟨“uxv”⟩𝒢G
12 eqid pInv𝒢G=pInv𝒢G
13 5 ad3antrrr φxABvBuA⟨“uxv”⟩𝒢GG𝒢Tarski
14 6 ad3antrrr φxABvBuA⟨“uxv”⟩𝒢GAranL
15 simplrr φxABvBuA⟨“uxv”⟩𝒢GuA
16 1 4 3 13 14 15 tglnpt φxABvBuA⟨“uxv”⟩𝒢GuP
17 simpllr φxABvBuA⟨“uxv”⟩𝒢GxAB
18 17 elin1d φxABvBuA⟨“uxv”⟩𝒢GxA
19 1 4 3 13 14 18 tglnpt φxABvBuA⟨“uxv”⟩𝒢GxP
20 7 ad3antrrr φxABvBuA⟨“uxv”⟩𝒢GBranL
21 simplrl φxABvBuA⟨“uxv”⟩𝒢GvB
22 1 4 3 13 20 21 tglnpt φxABvBuA⟨“uxv”⟩𝒢GvP
23 simpr φxABvBuA⟨“uxv”⟩𝒢G⟨“uxv”⟩𝒢G
24 1 2 3 4 12 13 16 19 22 23 ragcom φxABvBuA⟨“uxv”⟩𝒢G⟨“vxu”⟩𝒢G
25 5 ad3antrrr φxABvBuA⟨“vxu”⟩𝒢GG𝒢Tarski
26 7 ad3antrrr φxABvBuA⟨“vxu”⟩𝒢GBranL
27 simplrl φxABvBuA⟨“vxu”⟩𝒢GvB
28 1 4 3 25 26 27 tglnpt φxABvBuA⟨“vxu”⟩𝒢GvP
29 6 ad3antrrr φxABvBuA⟨“vxu”⟩𝒢GAranL
30 simpllr φxABvBuA⟨“vxu”⟩𝒢GxAB
31 30 elin1d φxABvBuA⟨“vxu”⟩𝒢GxA
32 1 4 3 25 29 31 tglnpt φxABvBuA⟨“vxu”⟩𝒢GxP
33 simplrr φxABvBuA⟨“vxu”⟩𝒢GuA
34 1 4 3 25 29 33 tglnpt φxABvBuA⟨“vxu”⟩𝒢GuP
35 simpr φxABvBuA⟨“vxu”⟩𝒢G⟨“vxu”⟩𝒢G
36 1 2 3 4 12 25 28 32 34 35 ragcom φxABvBuA⟨“vxu”⟩𝒢G⟨“uxv”⟩𝒢G
37 24 36 impbida φxABvBuA⟨“uxv”⟩𝒢G⟨“vxu”⟩𝒢G
38 37 2ralbidva φxABvBuA⟨“uxv”⟩𝒢GvBuA⟨“vxu”⟩𝒢G
39 11 38 syl5bb φxABuAvB⟨“uxv”⟩𝒢GvBuA⟨“vxu”⟩𝒢G
40 10 39 rexeqbidva φxABuAvB⟨“uxv”⟩𝒢GxBAvBuA⟨“vxu”⟩𝒢G
41 1 2 3 4 5 6 7 isperp φA𝒢GBxABuAvB⟨“uxv”⟩𝒢G
42 1 2 3 4 5 7 6 isperp φB𝒢GAxBAvBuA⟨“vxu”⟩𝒢G
43 40 41 42 3bitr4d φA𝒢GBB𝒢GA
44 8 43 mpbid φB𝒢GA