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

Proof

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