cgrextend

Description: Link congruence over a pair of line segments. Theorem 2.11 of Schwabhauser p. 29. (Contributed by Scott Fenton, 12-Jun-2013)

		Ref	Expression
	Assertion	cgrextend	$⊢ (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))) \to (((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to ⟨A, C⟩ Cgr ⟨D, F⟩)$

Proof

Step	Hyp	Ref	Expression
1		opeq1	$⊢ A = B \to ⟨A, B⟩ = ⟨B, B⟩$
2	1	breq1d	$⊢ A = B \to (⟨A, B⟩ Cgr ⟨D, E⟩ \leftrightarrow ⟨B, B⟩ Cgr ⟨D, E⟩)$
3	2	adantr	$⊢ (A = B \land (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)))) \to (⟨A, B⟩ Cgr ⟨D, E⟩ \leftrightarrow ⟨B, B⟩ Cgr ⟨D, E⟩)$
4		simp1	$⊢ (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))) \to N \in ℕ$
5		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))) \to B \in 𝔼 (N)$
6		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))) \to D \in 𝔼 (N)$
7		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))) \to E \in 𝔼 (N)$
8		cgrid2	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N))) \to (⟨B, B⟩ Cgr ⟨D, E⟩ \to D = E)$
9	4 5 6 7 8	syl13anc	$⊢ (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))) \to (⟨B, B⟩ Cgr ⟨D, E⟩ \to D = E)$
10	9	adantl	$⊢ (A = B \land (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)))) \to (⟨B, B⟩ Cgr ⟨D, E⟩ \to D = E)$
11	3 10	sylbid	$⊢ (A = B \land (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)))) \to (⟨A, B⟩ Cgr ⟨D, E⟩ \to D = E)$
12		opeq1	$⊢ A = B \to ⟨A, C⟩ = ⟨B, C⟩$
13		opeq1	$⊢ D = E \to ⟨D, F⟩ = ⟨E, F⟩$
14	12 13	breqan12d	$⊢ (A = B \land D = E) \to (⟨A, C⟩ Cgr ⟨D, F⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨E, F⟩)$
15	14	exbiri	$⊢ A = B \to (D = E \to (⟨B, C⟩ Cgr ⟨E, F⟩ \to ⟨A, C⟩ Cgr ⟨D, F⟩))$
16	15	adantr	$⊢ (A = B \land (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)))) \to (D = E \to (⟨B, C⟩ Cgr ⟨E, F⟩ \to ⟨A, C⟩ Cgr ⟨D, F⟩))$
17	11 16	syld	$⊢ (A = B \land (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)))) \to (⟨A, B⟩ Cgr ⟨D, E⟩ \to (⟨B, C⟩ Cgr ⟨E, F⟩ \to ⟨A, C⟩ Cgr ⟨D, F⟩))$
18	17	impd	$⊢ (A = B \land (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)))) \to ((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \to ⟨A, C⟩ Cgr ⟨D, F⟩)$
19	18	adantld	$⊢ (A = B \land (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)))) \to (((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to ⟨A, C⟩ Cgr ⟨D, F⟩)$
20	19	ex	$⊢ A = B \to ((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))) \to (((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to ⟨A, C⟩ Cgr ⟨D, F⟩))$
21		simpl1	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to N \in ℕ$
22		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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to A \in 𝔼 (N)$
23		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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to B \in 𝔼 (N)$
24	21 22 23	3jca	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N))$
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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to C \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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to D \in 𝔼 (N)$
27	25 22 26	3jca	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to (C \in 𝔼 (N) \land A \in 𝔼 (N) \land D \in 𝔼 (N))$
28		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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to E \in 𝔼 (N)$
29		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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to F \in 𝔼 (N)$
30	28 29 26	3jca	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to (E \in 𝔼 (N) \land F \in 𝔼 (N) \land D \in 𝔼 (N))$
31	24 27 30	3jca	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land A \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land D \in 𝔼 (N)))$
32		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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩)$
33		simprrr	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)$
34		cgrtriv	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land D \in 𝔼 (N)) \to ⟨A, A⟩ Cgr ⟨D, D⟩$
35	21 22 26 34	syl3anc	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to ⟨A, A⟩ Cgr ⟨D, D⟩$
36	33	simpld	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to ⟨A, B⟩ Cgr ⟨D, E⟩$
37		cgrcomlr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨D, E⟩ \leftrightarrow ⟨B, A⟩ Cgr ⟨E, D⟩)$
38	21 22 23 26 28 37	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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to (⟨A, B⟩ Cgr ⟨D, E⟩ \leftrightarrow ⟨B, A⟩ Cgr ⟨E, D⟩)$
39	36 38	mpbid	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to ⟨B, A⟩ Cgr ⟨E, D⟩$
40	35 39	jca	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to (⟨A, A⟩ Cgr ⟨D, D⟩ \land ⟨B, A⟩ Cgr ⟨E, D⟩)$
41		brofs	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land A \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, A⟩⟩ OuterFiveSeg ⟨⟨D, E⟩, ⟨F, D⟩⟩ \leftrightarrow ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \land (⟨A, A⟩ Cgr ⟨D, D⟩ \land ⟨B, A⟩ Cgr ⟨E, D⟩)))$
42	21 22 23 25 22 26 28 29 26 41	syl333anc	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to (⟨⟨A, B⟩, ⟨C, A⟩⟩ OuterFiveSeg ⟨⟨D, E⟩, ⟨F, D⟩⟩ \leftrightarrow ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \land (⟨A, A⟩ Cgr ⟨D, D⟩ \land ⟨B, A⟩ Cgr ⟨E, D⟩)))$
43	32 33 40 42	mpbir3and	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to ⟨⟨A, B⟩, ⟨C, A⟩⟩ OuterFiveSeg ⟨⟨D, E⟩, ⟨F, D⟩⟩$
44		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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to A \neq B$
45	43 44	jca	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to (⟨⟨A, B⟩, ⟨C, A⟩⟩ OuterFiveSeg ⟨⟨D, E⟩, ⟨F, D⟩⟩ \land A \neq B)$
46		5segofs	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land A \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((⟨⟨A, B⟩, ⟨C, A⟩⟩ OuterFiveSeg ⟨⟨D, E⟩, ⟨F, D⟩⟩ \land A \neq B) \to ⟨C, A⟩ Cgr ⟨F, D⟩)$
47	31 45 46	sylc	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to ⟨C, A⟩ Cgr ⟨F, D⟩$
48		cgrcomlr	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land A \in 𝔼 (N)) \land (F \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨C, A⟩ Cgr ⟨F, D⟩ \leftrightarrow ⟨A, C⟩ Cgr ⟨D, F⟩)$
49	21 25 22 29 26 48	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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to (⟨C, A⟩ Cgr ⟨F, D⟩ \leftrightarrow ⟨A, C⟩ Cgr ⟨D, F⟩)$
50	47 49	mpbid	$⊢ ((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 (A \neq B \land ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)))) \to ⟨A, C⟩ Cgr ⟨D, F⟩$
51	50	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))) \to (A \neq B \to (((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to ⟨A, C⟩ Cgr ⟨D, F⟩))$
52	51	com12	$⊢ A \neq B \to ((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))) \to (((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to ⟨A, C⟩ Cgr ⟨D, F⟩))$
53	20 52	pm2.61ine	$⊢ (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))) \to (((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to ⟨A, C⟩ Cgr ⟨D, F⟩)$

Metamath Proof Explorer

Theorem cgrextend

Proof