Metamath Proof Explorer

Theorem colperpexlem2

Description: Lemma for colperpex . Second part of lemma 8.20 of Schwabhauser p. 62. (Contributed by Thierry Arnoux, 10-Nov-2019)

Ref Expression
Hypotheses colperpex.p 
|- P = ( Base ` G )
colperpex.d 
|- .- = ( dist ` G )
colperpex.i 
|- I = ( Itv ` G )
colperpex.l 
|- L = ( LineG ` G )
colperpex.g 
|- ( ph -> G e. TarskiG )
colperpexlem.s 
|- S = ( pInvG ` G )
colperpexlem.m 
|- M = ( S ` A )
colperpexlem.n 
|- N = ( S ` B )
colperpexlem.k 
|- K = ( S ` Q )
colperpexlem.a 
|- ( ph -> A e. P )
colperpexlem.b 
|- ( ph -> B e. P )
colperpexlem.c 
|- ( ph -> C e. P )
colperpexlem.q 
|- ( ph -> Q e. P )
colperpexlem.1 
|- ( ph -> <" A B C "> e. ( raG ` G ) )
colperpexlem.2 
|- ( ph -> ( K ` ( M ` C ) ) = ( N ` C ) )
colperpexlem2.e 
|- ( ph -> B =/= C )
Assertion colperpexlem2 
|- ( ph -> A =/= Q )

Proof

Step Hyp Ref Expression
1 colperpex.p 
 |-  P = ( Base ` G )
2 colperpex.d 
 |-  .- = ( dist ` G )
3 colperpex.i 
 |-  I = ( Itv ` G )
4 colperpex.l 
 |-  L = ( LineG ` G )
5 colperpex.g 
 |-  ( ph -> G e. TarskiG )
6 colperpexlem.s 
 |-  S = ( pInvG ` G )
7 colperpexlem.m 
 |-  M = ( S ` A )
8 colperpexlem.n 
 |-  N = ( S ` B )
9 colperpexlem.k 
 |-  K = ( S ` Q )
10 colperpexlem.a 
 |-  ( ph -> A e. P )
11 colperpexlem.b 
 |-  ( ph -> B e. P )
12 colperpexlem.c 
 |-  ( ph -> C e. P )
13 colperpexlem.q 
 |-  ( ph -> Q e. P )
14 colperpexlem.1 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
15 colperpexlem.2 
 |-  ( ph -> ( K ` ( M ` C ) ) = ( N ` C ) )
16 colperpexlem2.e 
 |-  ( ph -> B =/= C )
17 simpr 
 |-  ( ( ph /\ A = Q ) -> A = Q )
18 17 fveq2d 
 |-  ( ( ph /\ A = Q ) -> ( S ` A ) = ( S ` Q ) )
19 18 7 9 3eqtr4g 
 |-  ( ( ph /\ A = Q ) -> M = K )
20 19 fveq1d 
 |-  ( ( ph /\ A = Q ) -> ( M ` ( M ` C ) ) = ( K ` ( M ` C ) ) )
21 1 2 3 4 6 5 10 7 12 mirmir 
 |-  ( ph -> ( M ` ( M ` C ) ) = C )
22 21 adantr 
 |-  ( ( ph /\ A = Q ) -> ( M ` ( M ` C ) ) = C )
23 15 adantr 
 |-  ( ( ph /\ A = Q ) -> ( K ` ( M ` C ) ) = ( N ` C ) )
24 20 22 23 3eqtr3rd 
 |-  ( ( ph /\ A = Q ) -> ( N ` C ) = C )
25 1 2 3 4 6 5 11 8 12 mirinv 
 |-  ( ph -> ( ( N ` C ) = C <-> B = C ) )
26 25 adantr 
 |-  ( ( ph /\ A = Q ) -> ( ( N ` C ) = C <-> B = C ) )
27 24 26 mpbid 
 |-  ( ( ph /\ A = Q ) -> B = C )
28 27 ex 
 |-  ( ph -> ( A = Q -> B = C ) )
29 28 necon3ad 
 |-  ( ph -> ( B =/= C -> -. A = Q ) )
30 16 29 mpd 
 |-  ( ph -> -. A = Q )
31 30 neqned 
 |-  ( ph -> A =/= Q )