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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐵 , 𝐴 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		fveecn	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
2		fveecn	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
3		sqsubswap	⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) )
4	1 2 3	syl2an	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) )
5	4	anandirs	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) )
6	5	sumeq2dv	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) )
7		id	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
8		simpr	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
9		simpl	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
10		brcgr	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐵 , 𝐴 ⟩ ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) ) )
11	7 8 9 10	syl12anc	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐵 , 𝐴 ⟩ ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↑ 2 ) ) )
12	6 11	mpbird	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐵 , 𝐴 ⟩ )
13	12	3adant1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐵 , 𝐴 ⟩ )