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	$⊢ \underset{˙}{-} = dist (G)$
	mirval.i	$⊢ I = Itv (G)$
	mirval.l	$⊢ L = {Line}_{𝒢} (G)$
	mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	krippen.m	$⊢ M = S (X)$
	krippen.n	$⊢ N = S (Y)$
	krippen.a	$⊢ φ \to A \in P$
	krippen.b	$⊢ φ \to B \in P$
	krippen.c	$⊢ φ \to C \in P$
	krippen.e	$⊢ φ \to E \in P$
	krippen.f	$⊢ φ \to F \in P$
	krippen.x	$⊢ φ \to X \in P$
	krippen.y	$⊢ φ \to Y \in P$
	krippen.1	$⊢ φ \to C \in (A I E)$
	krippen.2	$⊢ φ \to C \in (B I F)$
	krippen.3	$⊢ φ \to C \underset{˙}{-} A = C \underset{˙}{-} B$
	krippen.4	$⊢ φ \to C \underset{˙}{-} E = C \underset{˙}{-} F$
	krippen.5	$⊢ φ \to B = M (A)$
	krippen.6	$⊢ φ \to F = N (E)$
Assertion	krippen	$⊢ φ \to C \in (X I Y)$

Proof

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

Metamath Proof Explorer

Theorem krippen

Proof