seglecgr12

Description: Substitution law for segment comparison under congruence. Biconditional version. (Contributed by Scott Fenton, 15-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	seglecgr12	$⊢ ((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⟩) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩))$

Proof

Step	Hyp	Ref	Expression
1		df-3an	$⊢ (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩ \land ⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩) \leftrightarrow ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \land ⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩)$
2		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⟩)$
3	1 2	syl5bir	$⊢ ((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⟩)$
4	3	expd	$⊢ ((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⟩) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \to ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩))$
5		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 ℕ$
6		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)$
7		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)$
8		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)$
9		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)$
10		cgrcom	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \leftrightarrow ⟨E, F⟩ Cgr ⟨A, B⟩)$
11	5 6 7 8 9 10	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⟩ Cgr ⟨E, F⟩ \leftrightarrow ⟨E, F⟩ Cgr ⟨A, B⟩)$
12		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)$
13		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)$
14		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)$
15		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)$
16		cgrcom	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨C, D⟩ Cgr ⟨G, H⟩ \leftrightarrow ⟨G, H⟩ Cgr ⟨C, D⟩)$
17	5 12 13 14 15 16	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 (⟨C, D⟩ Cgr ⟨G, H⟩ \leftrightarrow ⟨G, H⟩ Cgr ⟨C, D⟩)$
18	11 17	anbi12d	$⊢ ((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⟩) \leftrightarrow (⟨E, F⟩ Cgr ⟨A, B⟩ \land ⟨G, H⟩ Cgr ⟨C, D⟩))$
19		df-3an	$⊢ (⟨E, F⟩ Cgr ⟨A, B⟩ \land ⟨G, H⟩ Cgr ⟨C, D⟩ \land ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩) \leftrightarrow ((⟨E, F⟩ Cgr ⟨A, B⟩ \land ⟨G, H⟩ Cgr ⟨C, D⟩) \land ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩)$
20		seglecgr12im	$⊢ ((N \in ℕ \land E \in 𝔼 (N) \land F \in 𝔼 (N)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((⟨E, F⟩ Cgr ⟨A, B⟩ \land ⟨G, H⟩ Cgr ⟨C, D⟩ \land ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩) \to ⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩)$
21	5 8 9 14 15 6 7 12 13 20	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 G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((⟨E, F⟩ Cgr ⟨A, B⟩ \land ⟨G, H⟩ Cgr ⟨C, D⟩ \land ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩) \to ⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩)$
22	19 21	syl5bir	$⊢ ((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⟩ Cgr ⟨A, B⟩ \land ⟨G, H⟩ Cgr ⟨C, D⟩) \land ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩) \to ⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩)$
23	22	expd	$⊢ ((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⟩ Cgr ⟨A, B⟩ \land ⟨G, H⟩ Cgr ⟨C, D⟩) \to (⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩ \to ⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩))$
24	18 23	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))) \to ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩) \to (⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩ \to ⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩))$
25	4 24	impbidd	$⊢ ((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⟩) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow ⟨E, F⟩ {Seg}_{\leq} ⟨G, H⟩))$

Metamath Proof Explorer

Theorem seglecgr12

Proof