Metamath Proof Explorer

Theorem axcgrtr

Description: Congruence is transitive. Axiom A2 of Schwabhauser p. 10. (Contributed by Scott Fenton, 3-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		eqtr2	$⊢ (\sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} \land \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(E (i) - F (i))}^{2}) \to \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} = \sum_{i = 1}^{N} {(E (i) - F (i))}^{2}$
2		simpl1	$⊢ ((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 \in 𝔼 (N)$
3		simpl2	$⊢ ((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)$
4		simpl3	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to C \in 𝔼 (N)$
5		simpr1	$⊢ ((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)$
6		brcgr	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨C, D⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
7	2 3 4 5 6	syl22anc	$⊢ ((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 ⟨C, D⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
8		simpr2	$⊢ ((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)$
9		simpr3	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to F \in 𝔼 (N)$
10		brcgr	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(E (i) - F (i))}^{2})$
11	2 3 8 9 10	syl22anc	$⊢ ((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 ⟨E, F⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(E (i) - F (i))}^{2})$
12	7 11	anbi12d	$⊢ ((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 ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨E, F⟩) \leftrightarrow (\sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} \land \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(E (i) - F (i))}^{2}))$
13		brcgr	$⊢ ((C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨C, D⟩ Cgr ⟨E, F⟩ \leftrightarrow \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} = \sum_{i = 1}^{N} {(E (i) - F (i))}^{2})$
14	4 5 8 9 13	syl22anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨C, D⟩ Cgr ⟨E, F⟩ \leftrightarrow \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} = \sum_{i = 1}^{N} {(E (i) - F (i))}^{2})$
15	12 14	imbi12d	$⊢ ((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 ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨E, F⟩) \to ⟨C, D⟩ Cgr ⟨E, F⟩) \leftrightarrow ((\sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} \land \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(E (i) - F (i))}^{2}) \to \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} = \sum_{i = 1}^{N} {(E (i) - F (i))}^{2}))$
16	1 15	mpbiri	$⊢ ((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 ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨E, F⟩) \to ⟨C, D⟩ Cgr ⟨E, F⟩)$
17	16	3adant1	$⊢ (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 ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨E, F⟩) \to ⟨C, D⟩ Cgr ⟨E, F⟩)$