Metamath Proof Explorer


Theorem krippen

Description: Krippenlemma (German for crib's lemma) Lemma 7.22 of Schwabhauser p. 53. proven by Gupta 1965 as Theorem 3.45. (Contributed by Thierry Arnoux, 12-Aug-2019)

Ref Expression
Hypotheses mirval.p 𝑃 = ( Base ‘ 𝐺 )
mirval.d = ( dist ‘ 𝐺 )
mirval.i 𝐼 = ( Itv ‘ 𝐺 )
mirval.l 𝐿 = ( LineG ‘ 𝐺 )
mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ( 𝜑𝐺 ∈ TarskiG )
krippen.m 𝑀 = ( 𝑆𝑋 )
krippen.n 𝑁 = ( 𝑆𝑌 )
krippen.a ( 𝜑𝐴𝑃 )
krippen.b ( 𝜑𝐵𝑃 )
krippen.c ( 𝜑𝐶𝑃 )
krippen.e ( 𝜑𝐸𝑃 )
krippen.f ( 𝜑𝐹𝑃 )
krippen.x ( 𝜑𝑋𝑃 )
krippen.y ( 𝜑𝑌𝑃 )
krippen.1 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
krippen.2 ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐹 ) )
krippen.3 ( 𝜑 → ( 𝐶 𝐴 ) = ( 𝐶 𝐵 ) )
krippen.4 ( 𝜑 → ( 𝐶 𝐸 ) = ( 𝐶 𝐹 ) )
krippen.5 ( 𝜑𝐵 = ( 𝑀𝐴 ) )
krippen.6 ( 𝜑𝐹 = ( 𝑁𝐸 ) )
Assertion krippen ( 𝜑𝐶 ∈ ( 𝑋 𝐼 𝑌 ) )

Proof

Step Hyp Ref Expression
1 mirval.p 𝑃 = ( Base ‘ 𝐺 )
2 mirval.d = ( dist ‘ 𝐺 )
3 mirval.i 𝐼 = ( Itv ‘ 𝐺 )
4 mirval.l 𝐿 = ( LineG ‘ 𝐺 )
5 mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
6 mirval.g ( 𝜑𝐺 ∈ TarskiG )
7 krippen.m 𝑀 = ( 𝑆𝑋 )
8 krippen.n 𝑁 = ( 𝑆𝑌 )
9 krippen.a ( 𝜑𝐴𝑃 )
10 krippen.b ( 𝜑𝐵𝑃 )
11 krippen.c ( 𝜑𝐶𝑃 )
12 krippen.e ( 𝜑𝐸𝑃 )
13 krippen.f ( 𝜑𝐹𝑃 )
14 krippen.x ( 𝜑𝑋𝑃 )
15 krippen.y ( 𝜑𝑌𝑃 )
16 krippen.1 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
17 krippen.2 ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐹 ) )
18 krippen.3 ( 𝜑 → ( 𝐶 𝐴 ) = ( 𝐶 𝐵 ) )
19 krippen.4 ( 𝜑 → ( 𝐶 𝐸 ) = ( 𝐶 𝐹 ) )
20 krippen.5 ( 𝜑𝐵 = ( 𝑀𝐴 ) )
21 krippen.6 ( 𝜑𝐹 = ( 𝑁𝐸 ) )
22 6 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐺 ∈ TarskiG )
23 9 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐴𝑃 )
24 10 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐵𝑃 )
25 11 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐶𝑃 )
26 12 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐸𝑃 )
27 13 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐹𝑃 )
28 14 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝑋𝑃 )
29 15 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝑌𝑃 )
30 16 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
31 17 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝐹 ) )
32 18 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → ( 𝐶 𝐴 ) = ( 𝐶 𝐵 ) )
33 19 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → ( 𝐶 𝐸 ) = ( 𝐶 𝐹 ) )
34 20 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐵 = ( 𝑀𝐴 ) )
35 21 adantr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐹 = ( 𝑁𝐸 ) )
36 eqid ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 )
37 simpr ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) )
38 1 2 3 4 5 22 7 8 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 krippenlem ( ( 𝜑 ∧ ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ) → 𝐶 ∈ ( 𝑋 𝐼 𝑌 ) )
39 6 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐺 ∈ TarskiG )
40 15 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝑌𝑃 )
41 11 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐶𝑃 )
42 14 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝑋𝑃 )
43 12 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐸𝑃 )
44 13 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐹𝑃 )
45 9 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐴𝑃 )
46 10 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐵𝑃 )
47 16 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
48 1 2 3 39 45 41 43 47 tgbtwncom ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐶 ∈ ( 𝐸 𝐼 𝐴 ) )
49 17 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝐹 ) )
50 1 2 3 39 46 41 44 49 tgbtwncom ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐶 ∈ ( 𝐹 𝐼 𝐵 ) )
51 19 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → ( 𝐶 𝐸 ) = ( 𝐶 𝐹 ) )
52 18 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → ( 𝐶 𝐴 ) = ( 𝐶 𝐵 ) )
53 21 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐹 = ( 𝑁𝐸 ) )
54 20 adantr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐵 = ( 𝑀𝐴 ) )
55 simpr ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) )
56 1 2 3 4 5 39 8 7 43 44 41 45 46 40 42 48 50 51 52 53 54 36 55 krippenlem ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐶 ∈ ( 𝑌 𝐼 𝑋 ) )
57 1 2 3 39 40 41 42 56 tgbtwncom ( ( 𝜑 ∧ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) → 𝐶 ∈ ( 𝑋 𝐼 𝑌 ) )
58 1 2 3 36 6 11 9 11 12 legtrid ( 𝜑 → ( ( 𝐶 𝐴 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐸 ) ∨ ( 𝐶 𝐸 ) ( ≤G ‘ 𝐺 ) ( 𝐶 𝐴 ) ) )
59 38 57 58 mpjaodan ( 𝜑𝐶 ∈ ( 𝑋 𝐼 𝑌 ) )