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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
colperpex.d ⊢ − = ( dist ‘ 𝐺 )
colperpex.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
colperpex.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
colperpex.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
colperpexlem.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
colperpexlem.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
colperpexlem.n ⊢ 𝑁 = ( 𝑆 ‘ 𝐵 )
colperpexlem.k ⊢ 𝐾 = ( 𝑆 ‘ 𝑄 )
colperpexlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
colperpexlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
colperpexlem.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
colperpexlem.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
colperpexlem.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
colperpexlem.2 ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) = ( 𝑁 ‘ 𝐶 ) )
colperpexlem2.e ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion colperpexlem2 ( 𝜑 → 𝐴 ≠ 𝑄 )

Proof

Step Hyp Ref Expression
1 colperpex.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 colperpex.d ⊢ − = ( dist ‘ 𝐺 )
3 colperpex.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 colperpex.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 colperpex.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 colperpexlem.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
7 colperpexlem.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
8 colperpexlem.n ⊢ 𝑁 = ( 𝑆 ‘ 𝐵 )
9 colperpexlem.k ⊢ 𝐾 = ( 𝑆 ‘ 𝑄 )
10 colperpexlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
11 colperpexlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
12 colperpexlem.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
13 colperpexlem.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
14 colperpexlem.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
15 colperpexlem.2 ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) = ( 𝑁 ‘ 𝐶 ) )
16 colperpexlem2.e ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑄 ) → 𝐴 = 𝑄 )
18 17 fveq2d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑄 ) → ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝑄 ) )
19 18 7 9 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑄 ) → 𝑀 = 𝐾 )
20 19 fveq1d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑄 ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝐶 ) ) = ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) )
21 1 2 3 4 6 5 10 7 12 mirmir ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐶 ) ) = 𝐶 )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑄 ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝐶 ) ) = 𝐶 )
23 15 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑄 ) → ( 𝐾 ‘ ( 𝑀 ‘ 𝐶 ) ) = ( 𝑁 ‘ 𝐶 ) )
24 20 22 23 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑄 ) → ( 𝑁 ‘ 𝐶 ) = 𝐶 )
25 1 2 3 4 6 5 11 8 12 mirinv ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐶 ) = 𝐶 ↔ 𝐵 = 𝐶 ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑄 ) → ( ( 𝑁 ‘ 𝐶 ) = 𝐶 ↔ 𝐵 = 𝐶 ) )
27 24 26 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑄 ) → 𝐵 = 𝐶 )
28 27 ex ⊢ ( 𝜑 → ( 𝐴 = 𝑄 → 𝐵 = 𝐶 ) )
29 28 necon3ad ⊢ ( 𝜑 → ( 𝐵 ≠ 𝐶 → ¬ 𝐴 = 𝑄 ) )
30 16 29 mpd ⊢ ( 𝜑 → ¬ 𝐴 = 𝑄 )
31 30 neqned ⊢ ( 𝜑 → 𝐴 ≠ 𝑄 )