btwnconn1lem10

Description: Lemma for btwnconn1 . Now we establish a congruence that will give us D = d when we compute P = Q later on. (Contributed by Scott Fenton, 8-Oct-2013)

		Ref	Expression
	Assertion	btwnconn1lem10	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, D⟩ Cgr ⟨P, Q⟩$

Proof

Step	Hyp	Ref	Expression
1		simp11	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to N \in ℕ$
2		simp2r1	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to d \in 𝔼 (N)$
3		simp2r3	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to E \in 𝔼 (N)$
4		simp2l2	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to D \in 𝔼 (N)$
5		simp31	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to P \in 𝔼 (N)$
6		simp33	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to R \in 𝔼 (N)$
7		simp32	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to Q \in 𝔼 (N)$
8		simprlr	$⊢ ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩)))) \to E Btwn ⟨D, d⟩$
9	8	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to E Btwn ⟨D, d⟩$
10	1 3 4 2 9	btwncomand	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to E Btwn ⟨d, D⟩$
11		simpr3l	$⊢ ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))) \to R Btwn ⟨P, Q⟩$
12	11	ad2antll	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to R Btwn ⟨P, Q⟩$
13		btwnconn1lem8	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨R, P⟩ Cgr ⟨E, d⟩$
14		cgrcomlr	$⊢ (N \in ℕ \land (R \in 𝔼 (N) \land P \in 𝔼 (N)) \land (E \in 𝔼 (N) \land d \in 𝔼 (N))) \to (⟨R, P⟩ Cgr ⟨E, d⟩ \leftrightarrow ⟨P, R⟩ Cgr ⟨d, E⟩)$
15	1 6 5 3 2 14	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨R, P⟩ Cgr ⟨E, d⟩ \leftrightarrow ⟨P, R⟩ Cgr ⟨d, E⟩)$
16		cgrcom	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land R \in 𝔼 (N)) \land (d \in 𝔼 (N) \land E \in 𝔼 (N))) \to (⟨P, R⟩ Cgr ⟨d, E⟩ \leftrightarrow ⟨d, E⟩ Cgr ⟨P, R⟩)$
17	1 5 6 2 3 16	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨P, R⟩ Cgr ⟨d, E⟩ \leftrightarrow ⟨d, E⟩ Cgr ⟨P, R⟩)$
18	15 17	bitrd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨R, P⟩ Cgr ⟨E, d⟩ \leftrightarrow ⟨d, E⟩ Cgr ⟨P, R⟩)$
19	18	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (⟨R, P⟩ Cgr ⟨E, d⟩ \leftrightarrow ⟨d, E⟩ Cgr ⟨P, R⟩)$
20	13 19	mpbid	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, E⟩ Cgr ⟨P, R⟩$
21		btwnconn1lem9	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨R, Q⟩ Cgr ⟨E, D⟩$
22	1 6 7 3 4 21	cgrcomand	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨E, D⟩ Cgr ⟨R, Q⟩$
23	1 2 3 4 5 6 7 10 12 20 22	cgrextendand	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, D⟩ Cgr ⟨P, Q⟩$

Metamath Proof Explorer

Theorem btwnconn1lem10

Proof