Metamath Proof Explorer

Theorem axcgrrflx

Description: A is as far from B as B is from A . Axiom A1 of Schwabhauser p. 10. (Contributed by Scott Fenton, 3-Jun-2013)

		Ref	Expression
	Assertion	axcgrrflx	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to ⟨A, B⟩ Cgr ⟨B, A⟩$

Proof

Step	Hyp	Ref	Expression
1		fveecn	$⊢ (A \in 𝔼 (N) \land i \in (1 \dots N)) \to A (i) \in ℂ$
2		fveecn	$⊢ (B \in 𝔼 (N) \land i \in (1 \dots N)) \to B (i) \in ℂ$
3		sqsubswap	$⊢ (A (i) \in ℂ \land B (i) \in ℂ) \to {(A (i) - B (i))}^{2} = {(B (i) - A (i))}^{2}$
4	1 2 3	syl2an	$⊢ ((A \in 𝔼 (N) \land i \in (1 \dots N)) \land (B \in 𝔼 (N) \land i \in (1 \dots N))) \to {(A (i) - B (i))}^{2} = {(B (i) - A (i))}^{2}$
5	4	anandirs	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land i \in (1 \dots N)) \to {(A (i) - B (i))}^{2} = {(B (i) - A (i))}^{2}$
6	5	sumeq2dv	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(B (i) - A (i))}^{2}$
7		id	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (A \in 𝔼 (N) \land B \in 𝔼 (N))$
8		simpr	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to B \in 𝔼 (N)$
9		simpl	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to A \in 𝔼 (N)$
10		brcgr	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (B \in 𝔼 (N) \land A \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨B, A⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(B (i) - A (i))}^{2})$
11	7 8 9 10	syl12anc	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (⟨A, B⟩ Cgr ⟨B, A⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(B (i) - A (i))}^{2})$
12	6 11	mpbird	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to ⟨A, B⟩ Cgr ⟨B, A⟩$
13	12	3adant1	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \to ⟨A, B⟩ Cgr ⟨B, A⟩$