cgrsub

Description: Removing identical parts from the end of a line segment preserves congruence. Theorem 4.3 of Schwabhauser p. 35. (Contributed by Scott Fenton, 4-Oct-2013)

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

Proof

Step	Hyp	Ref	Expression
1		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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩)$
2		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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)$
3		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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to A \in 𝔼 (N)$
5		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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to D \in 𝔼 (N)$
6		cgrtriv	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land D \in 𝔼 (N)) \to ⟨A, A⟩ Cgr ⟨D, D⟩$
7	3 4 5 6	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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to ⟨A, A⟩ Cgr ⟨D, D⟩$
8		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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to ⟨A, C⟩ Cgr ⟨D, F⟩$
9		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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to C \in 𝔼 (N)$
10		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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to F \in 𝔼 (N)$
11		cgrcomlr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, C⟩ Cgr ⟨D, F⟩ \leftrightarrow ⟨C, A⟩ Cgr ⟨F, D⟩)$
12	3 4 9 5 10 11	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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to (⟨A, C⟩ Cgr ⟨D, F⟩ \leftrightarrow ⟨C, A⟩ Cgr ⟨F, D⟩)$
13	8 12	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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to ⟨C, A⟩ Cgr ⟨F, D⟩$
14	7 13	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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to (⟨A, A⟩ Cgr ⟨D, D⟩ \land ⟨C, A⟩ Cgr ⟨F, D⟩)$
15		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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to B \in 𝔼 (N)$
16		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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to E \in 𝔼 (N)$
17		brifs	$⊢ ((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⟩⟩ InnerFiveSeg ⟨⟨D, E⟩, ⟨F, D⟩⟩ \leftrightarrow ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \land (⟨A, A⟩ Cgr ⟨D, D⟩ \land ⟨C, A⟩ Cgr ⟨F, D⟩)))$
18		ifscgr	$⊢ ((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⟩⟩ InnerFiveSeg ⟨⟨D, E⟩, ⟨F, D⟩⟩ \to ⟨B, A⟩ Cgr ⟨E, D⟩)$
19	17 18	sylbird	$⊢ ((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 (((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \land (⟨A, A⟩ Cgr ⟨D, D⟩ \land ⟨C, A⟩ Cgr ⟨F, D⟩)) \to ⟨B, A⟩ Cgr ⟨E, D⟩)$
20	3 4 15 9 4 5 16 10 5 19	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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to (((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩) \land (⟨A, A⟩ Cgr ⟨D, D⟩ \land ⟨C, A⟩ Cgr ⟨F, D⟩)) \to ⟨B, A⟩ Cgr ⟨E, D⟩)$
21	1 2 14 20	mp3and	$⊢ ((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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to ⟨B, A⟩ Cgr ⟨E, D⟩$
22		cgrcomlr	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land A \in 𝔼 (N)) \land (E \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨B, A⟩ Cgr ⟨E, D⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨D, E⟩)$
23	3 15 4 16 5 22	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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to (⟨B, A⟩ Cgr ⟨E, D⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨D, E⟩)$
24	21 23	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 ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, F⟩) \land (⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))) \to ⟨A, B⟩ Cgr ⟨D, E⟩$
25	24	ex	$⊢ (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, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to ⟨A, B⟩ Cgr ⟨D, E⟩)$

Metamath Proof Explorer

Theorem cgrsub

Proof