Description: The "perpendicular" relation commutes. Theorem 8.12 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isperp.p | |
|
isperp.d | |
||
isperp.i | |
||
isperp.l | |
||
isperp.g | |
||
isperp.a | |
||
isperp.b | |
||
perpcom.1 | |
||
Assertion | perpcom | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isperp.p | |
|
2 | isperp.d | |
|
3 | isperp.i | |
|
4 | isperp.l | |
|
5 | isperp.g | |
|
6 | isperp.a | |
|
7 | isperp.b | |
|
8 | perpcom.1 | |
|
9 | incom | |
|
10 | 9 | a1i | |
11 | ralcom | |
|
12 | eqid | |
|
13 | 5 | ad3antrrr | |
14 | 6 | ad3antrrr | |
15 | simplrr | |
|
16 | 1 4 3 13 14 15 | tglnpt | |
17 | simpllr | |
|
18 | 17 | elin1d | |
19 | 1 4 3 13 14 18 | tglnpt | |
20 | 7 | ad3antrrr | |
21 | simplrl | |
|
22 | 1 4 3 13 20 21 | tglnpt | |
23 | simpr | |
|
24 | 1 2 3 4 12 13 16 19 22 23 | ragcom | |
25 | 5 | ad3antrrr | |
26 | 7 | ad3antrrr | |
27 | simplrl | |
|
28 | 1 4 3 25 26 27 | tglnpt | |
29 | 6 | ad3antrrr | |
30 | simpllr | |
|
31 | 30 | elin1d | |
32 | 1 4 3 25 29 31 | tglnpt | |
33 | simplrr | |
|
34 | 1 4 3 25 29 33 | tglnpt | |
35 | simpr | |
|
36 | 1 2 3 4 12 25 28 32 34 35 | ragcom | |
37 | 24 36 | impbida | |
38 | 37 | 2ralbidva | |
39 | 11 38 | syl5bb | |
40 | 10 39 | rexeqbidva | |
41 | 1 2 3 4 5 6 7 | isperp | |
42 | 1 2 3 4 5 7 6 | isperp | |
43 | 40 41 42 | 3bitr4d | |
44 | 8 43 | mpbid | |