linecgr

Description: Congruence rule for lines. Theorem 4.17 of Schwabhauser p. 37. (Contributed by Scott Fenton, 6-Oct-2013)

		Ref	Expression
	Assertion	linecgr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \to ⟨C, P⟩ Cgr ⟨C, Q⟩)$

Proof

Step	Hyp	Ref	Expression
1		simprlr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \land ((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩))) \to A Colinear ⟨B, C⟩$
2		cgr3rflx	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨A, ⟨B, C⟩⟩$
3	2	3adant3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨A, ⟨B, C⟩⟩$
4	3	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \land ((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩))) \to ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨A, ⟨B, C⟩⟩$
5		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \land ((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩))) \to (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)$
6	1 4 5	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \land ((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩))) \to (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨A, ⟨B, C⟩⟩ \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩))$
7		simprll	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \land ((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩))) \to A \neq B$
8	6 7	jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \land ((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩))) \to ((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨A, ⟨B, C⟩⟩ \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \land A \neq B)$
9	8	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \to ((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨A, ⟨B, C⟩⟩ \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \land A \neq B))$
10		simp1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to N \in ℕ$
11		simp21	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to A \in 𝔼 (N)$
12		simp22	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to B \in 𝔼 (N)$
13		simp23	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to C \in 𝔼 (N)$
14		simp3l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to P \in 𝔼 (N)$
15		simp3r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to Q \in 𝔼 (N)$
16		brfs	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, P⟩⟩ FiveSeg ⟨⟨A, B⟩, ⟨C, Q⟩⟩ \leftrightarrow (A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨A, ⟨B, C⟩⟩ \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)))$
17	16	anbi1d	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N) \land Q \in 𝔼 (N))) \to ((⟨⟨A, B⟩, ⟨C, P⟩⟩ FiveSeg ⟨⟨A, B⟩, ⟨C, Q⟩⟩ \land A \neq B) \leftrightarrow ((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨A, ⟨B, C⟩⟩ \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \land A \neq B))$
18		fscgr	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N) \land Q \in 𝔼 (N))) \to ((⟨⟨A, B⟩, ⟨C, P⟩⟩ FiveSeg ⟨⟨A, B⟩, ⟨C, Q⟩⟩ \land A \neq B) \to ⟨C, P⟩ Cgr ⟨C, Q⟩)$
19	17 18	sylbird	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨A, ⟨B, C⟩⟩ \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \land A \neq B) \to ⟨C, P⟩ Cgr ⟨C, Q⟩)$
20	10 11 12 13 14 11 12 13 15 19	syl333anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (((A Colinear ⟨B, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨A, ⟨B, C⟩⟩ \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \land A \neq B) \to ⟨C, P⟩ Cgr ⟨C, Q⟩)$
21	9 20	syld	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (((A \neq B \land A Colinear ⟨B, C⟩) \land (⟨A, P⟩ Cgr ⟨A, Q⟩ \land ⟨B, P⟩ Cgr ⟨B, Q⟩)) \to ⟨C, P⟩ Cgr ⟨C, Q⟩)$

Metamath Proof Explorer

Theorem linecgr

Proof