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 
|- P = ( Base ` G )
mirval.d 
|- .- = ( dist ` G )
mirval.i 
|- I = ( Itv ` G )
mirval.l 
|- L = ( LineG ` G )
mirval.s 
|- S = ( pInvG ` G )
mirval.g 
|- ( ph -> G e. TarskiG )
krippen.m 
|- M = ( S ` X )
krippen.n 
|- N = ( S ` Y )
krippen.a 
|- ( ph -> A e. P )
krippen.b 
|- ( ph -> B e. P )
krippen.c 
|- ( ph -> C e. P )
krippen.e 
|- ( ph -> E e. P )
krippen.f 
|- ( ph -> F e. P )
krippen.x 
|- ( ph -> X e. P )
krippen.y 
|- ( ph -> Y e. P )
krippen.1 
|- ( ph -> C e. ( A I E ) )
krippen.2 
|- ( ph -> C e. ( B I F ) )
krippen.3 
|- ( ph -> ( C .- A ) = ( C .- B ) )
krippen.4 
|- ( ph -> ( C .- E ) = ( C .- F ) )
krippen.5 
|- ( ph -> B = ( M ` A ) )
krippen.6 
|- ( ph -> F = ( N ` E ) )
Assertion krippen 
|- ( ph -> C e. ( X I Y ) )

Proof

Step Hyp Ref Expression
1 mirval.p 
 |-  P = ( Base ` G )
2 mirval.d 
 |-  .- = ( dist ` G )
3 mirval.i 
 |-  I = ( Itv ` G )
4 mirval.l 
 |-  L = ( LineG ` G )
5 mirval.s 
 |-  S = ( pInvG ` G )
6 mirval.g 
 |-  ( ph -> G e. TarskiG )
7 krippen.m 
 |-  M = ( S ` X )
8 krippen.n 
 |-  N = ( S ` Y )
9 krippen.a 
 |-  ( ph -> A e. P )
10 krippen.b 
 |-  ( ph -> B e. P )
11 krippen.c 
 |-  ( ph -> C e. P )
12 krippen.e 
 |-  ( ph -> E e. P )
13 krippen.f 
 |-  ( ph -> F e. P )
14 krippen.x 
 |-  ( ph -> X e. P )
15 krippen.y 
 |-  ( ph -> Y e. P )
16 krippen.1 
 |-  ( ph -> C e. ( A I E ) )
17 krippen.2 
 |-  ( ph -> C e. ( B I F ) )
18 krippen.3 
 |-  ( ph -> ( C .- A ) = ( C .- B ) )
19 krippen.4 
 |-  ( ph -> ( C .- E ) = ( C .- F ) )
20 krippen.5 
 |-  ( ph -> B = ( M ` A ) )
21 krippen.6 
 |-  ( ph -> F = ( N ` E ) )
22 6 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> G e. TarskiG )
23 9 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> A e. P )
24 10 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> B e. P )
25 11 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> C e. P )
26 12 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> E e. P )
27 13 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> F e. P )
28 14 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> X e. P )
29 15 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> Y e. P )
30 16 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> C e. ( A I E ) )
31 17 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> C e. ( B I F ) )
32 18 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> ( C .- A ) = ( C .- B ) )
33 19 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> ( C .- E ) = ( C .- F ) )
34 20 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> B = ( M ` A ) )
35 21 adantr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> F = ( N ` E ) )
36 eqid 
 |-  ( leG ` G ) = ( leG ` G )
37 simpr 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> ( C .- A ) ( leG ` G ) ( C .- E ) )
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 
 |-  ( ( ph /\ ( C .- A ) ( leG ` G ) ( C .- E ) ) -> C e. ( X I Y ) )
39 6 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> G e. TarskiG )
40 15 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> Y e. P )
41 11 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> C e. P )
42 14 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> X e. P )
43 12 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> E e. P )
44 13 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> F e. P )
45 9 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> A e. P )
46 10 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> B e. P )
47 16 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> C e. ( A I E ) )
48 1 2 3 39 45 41 43 47 tgbtwncom 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> C e. ( E I A ) )
49 17 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> C e. ( B I F ) )
50 1 2 3 39 46 41 44 49 tgbtwncom 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> C e. ( F I B ) )
51 19 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> ( C .- E ) = ( C .- F ) )
52 18 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> ( C .- A ) = ( C .- B ) )
53 21 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> F = ( N ` E ) )
54 20 adantr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> B = ( M ` A ) )
55 simpr 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> ( C .- E ) ( leG ` G ) ( C .- A ) )
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 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> C e. ( Y I X ) )
57 1 2 3 39 40 41 42 56 tgbtwncom 
 |-  ( ( ph /\ ( C .- E ) ( leG ` G ) ( C .- A ) ) -> C e. ( X I Y ) )
58 1 2 3 36 6 11 9 11 12 legtrid 
 |-  ( ph -> ( ( C .- A ) ( leG ` G ) ( C .- E ) \/ ( C .- E ) ( leG ` G ) ( C .- A ) ) )
59 38 57 58 mpjaodan 
 |-  ( ph -> C e. ( X I Y ) )