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 e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. Cgr <. B , A >. )

Proof

Step	Hyp	Ref	Expression
1		fveecn	|- ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
2		fveecn	|- ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
3		sqsubswap	|- ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) -> ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = ( ( ( B ` i ) - ( A ` i ) ) ^ 2 ) )
4	1 2 3	syl2an	|- ( ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) /\ ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) ) -> ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = ( ( ( B ` i ) - ( A ` i ) ) ^ 2 ) )
5	4	anandirs	|- ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = ( ( ( B ` i ) - ( A ` i ) ) ^ 2 ) )
6	5	sumeq2dv	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) ^ 2 ) )
7		id	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
8		simpr	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B e. ( EE ` N ) )
9		simpl	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A e. ( EE ` N ) )
10		brcgr	|- ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. B , A >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) ^ 2 ) ) )
11	7 8 9 10	syl12anc	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( <. A , B >. Cgr <. B , A >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) ^ 2 ) ) )
12	6 11	mpbird	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. Cgr <. B , A >. )
13	12	3adant1	|- ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. Cgr <. B , A >. )