seglecgr12im

Description: Substitution law for segment comparison under congruence. Theorem 5.6 of Schwabhauser p. 42. (Contributed by Scott Fenton, 11-Oct-2013)

		Ref	Expression
	Assertion	seglecgr12im	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩) \to ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩)$

Proof

Step	Hyp	Ref	Expression
1		simprrl	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to y Btwn ⟨C, D⟩$
2		simprlr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to ⟨C, D⟩ Cgr ⟨G, H⟩$
3		simpl11	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \to N \in ℕ$
4		simpl21	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \to C \in 𝔼 (N)$
5		simpr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \to y \in 𝔼 (N)$
6		simpl22	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \to D \in 𝔼 (N)$
7		simpl32	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \to G \in 𝔼 (N)$
8		simpl33	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \to H \in 𝔼 (N)$
9		cgrxfr	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land y \in 𝔼 (N) \land D \in 𝔼 (N)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((y Btwn ⟨C, D⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \to \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩))$
10	3 4 5 6 7 8 9	syl132anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \to ((y Btwn ⟨C, D⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \to \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩))$
11	10	adantr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to ((y Btwn ⟨C, D⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \to \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩))$
12	1 2 11	mp2and	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩)$
13		anass	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \land z \in 𝔼 (N)) \leftrightarrow (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N)))$
14		simpl11	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to N \in ℕ$
15		simpl21	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to C \in 𝔼 (N)$
16		simprl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to y \in 𝔼 (N)$
17		simpl22	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to D \in 𝔼 (N)$
18		simpl32	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to G \in 𝔼 (N)$
19		simprr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to z \in 𝔼 (N)$
20		simpl33	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to H \in 𝔼 (N)$
21		brcgr3	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land y \in 𝔼 (N) \land D \in 𝔼 (N)) \land (G \in 𝔼 (N) \land z \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩ \leftrightarrow (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩))$
22	14 15 16 17 18 19 20 21	syl133anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩ \leftrightarrow (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩))$
23	22	adantr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩ \leftrightarrow (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩))$
24		df-3an	$⊢ ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩)) \leftrightarrow (((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \land (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩))$
25		simpl23	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to E \in 𝔼 (N)$
26		simpl31	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to F \in 𝔼 (N)$
27		simpl12	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to A \in 𝔼 (N)$
28		simpl13	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to B \in 𝔼 (N)$
29		simpr1l	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩))) \to ⟨A, B⟩ Cgr ⟨E, F⟩$
30		simpr2r	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩))) \to ⟨A, B⟩ Cgr ⟨C, y⟩$
31	14 27 28 25 26 15 16 29 30	cgrtr4and	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩))) \to ⟨E, F⟩ Cgr ⟨C, y⟩$
32		simpr31	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩))) \to ⟨C, y⟩ Cgr ⟨G, z⟩$
33	14 25 26 15 16 18 19 31 32	cgrtrand	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩))) \to ⟨E, F⟩ Cgr ⟨G, z⟩$
34	24 33	sylan2br	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land (((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \land (⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩))) \to ⟨E, F⟩ Cgr ⟨G, z⟩$
35	34	expr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to ((⟨C, y⟩ Cgr ⟨G, z⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨y, D⟩ Cgr ⟨z, H⟩) \to ⟨E, F⟩ Cgr ⟨G, z⟩)$
36	23 35	sylbid	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩ \to ⟨E, F⟩ Cgr ⟨G, z⟩)$
37	36	anim2d	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to ((z Btwn ⟨G, H⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩) \to (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩))$
38	13 37	sylanb	$⊢ (((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \land z \in 𝔼 (N)) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to ((z Btwn ⟨G, H⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩) \to (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩))$
39	38	an32s	$⊢ (((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \land z \in 𝔼 (N)) \to ((z Btwn ⟨G, H⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩) \to (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩))$
40	39	reximdva	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to (\exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨G, ⟨z, H⟩⟩) \to \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩))$
41	12 40	mpd	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \land ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩)$
42	41	expr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \to \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩))$
43	42	an32s	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \land y \in 𝔼 (N)) \to ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \to \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩))$
44	43	rexlimdva	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to (\exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \to \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩))$
45		simp11	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to N \in ℕ$
46		simp12	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to A \in 𝔼 (N)$
47		simp13	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to B \in 𝔼 (N)$
48		simp21	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to C \in 𝔼 (N)$
49		simp22	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to D \in 𝔼 (N)$
50		brsegle	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
51	45 46 47 48 49 50	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
52	51	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
53		simp23	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to E \in 𝔼 (N)$
54		simp31	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to F \in 𝔼 (N)$
55		simp32	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to G \in 𝔼 (N)$
56		simp33	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to H \in 𝔼 (N)$
57		brsegle	$⊢ (N \in ℕ \land (E \in 𝔼 (N) \land F \in 𝔼 (N)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩ \leftrightarrow \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩))$
58	45 53 54 55 56 57	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩ \leftrightarrow \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩))$
59	58	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to (⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩ \leftrightarrow \exists z \in 𝔼 (N) (z Btwn ⟨G, H⟩ \land ⟨E, F⟩ Cgr ⟨G, z⟩))$
60	44 52 59	3imtr4d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \to ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩)$
61	60	exp32	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \to (⟨C, D⟩ Cgr ⟨G, H⟩ \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \to ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩)))$
62	61	3impd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩) \to ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩)$

Metamath Proof Explorer

Theorem seglecgr12im

Proof