axcgrid

Description: If there is no distance between A and B , then A = B . Axiom A3 of Schwabhauser p. 10. (Contributed by Scott Fenton, 3-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		fveecn	$⊢ (C \in 𝔼 (N) \land i \in (1 \dots N)) \to C (i) \in ℂ$
2		subid	$⊢ C (i) \in ℂ \to C (i) - C (i) = 0$
3	2	sq0id	$⊢ C (i) \in ℂ \to {(C (i) - C (i))}^{2} = 0$
4	1 3	syl	$⊢ (C \in 𝔼 (N) \land i \in (1 \dots N)) \to {(C (i) - C (i))}^{2} = 0$
5	4	sumeq2dv	$⊢ C \in 𝔼 (N) \to \sum_{i = 1}^{N} {(C (i) - C (i))}^{2} = \sum_{i = 1}^{N} 0$
6		fzfid	$⊢ C \in 𝔼 (N) \to (1 \dots N) \in Fin$
7		sumz	$⊢ ((1 \dots N) \subseteq ℤ_{\geq 1} \lor (1 \dots N) \in Fin) \to \sum_{i = 1}^{N} 0 = 0$
8	7	olcs	$⊢ (1 \dots N) \in Fin \to \sum_{i = 1}^{N} 0 = 0$
9	6 8	syl	$⊢ C \in 𝔼 (N) \to \sum_{i = 1}^{N} 0 = 0$
10	5 9	eqtrd	$⊢ C \in 𝔼 (N) \to \sum_{i = 1}^{N} {(C (i) - C (i))}^{2} = 0$
11	10	3ad2ant3	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to \sum_{i = 1}^{N} {(C (i) - C (i))}^{2} = 0$
12	11	eqeq2d	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (\sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - C (i))}^{2} \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = 0)$
13		fzfid	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (1 \dots N) \in Fin$
14		fveere	$⊢ (A \in 𝔼 (N) \land i \in (1 \dots N)) \to A (i) \in ℝ$
15	14	adantlr	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land i \in (1 \dots N)) \to A (i) \in ℝ$
16		fveere	$⊢ (B \in 𝔼 (N) \land i \in (1 \dots N)) \to B (i) \in ℝ$
17	16	adantll	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land i \in (1 \dots N)) \to B (i) \in ℝ$
18	15 17	resubcld	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land i \in (1 \dots N)) \to A (i) - B (i) \in ℝ$
19	18	resqcld	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land i \in (1 \dots N)) \to {(A (i) - B (i))}^{2} \in ℝ$
20	18	sqge0d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land i \in (1 \dots N)) \to 0 \leq {(A (i) - B (i))}^{2}$
21	13 19 20	fsum00	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (\sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = 0 \leftrightarrow \forall i \in (1 \dots N) {(A (i) - B (i))}^{2} = 0)$
22		fveecn	$⊢ (A \in 𝔼 (N) \land i \in (1 \dots N)) \to A (i) \in ℂ$
23		fveecn	$⊢ (B \in 𝔼 (N) \land i \in (1 \dots N)) \to B (i) \in ℂ$
24		subcl	$⊢ (A (i) \in ℂ \land B (i) \in ℂ) \to A (i) - B (i) \in ℂ$
25		sqeq0	$⊢ A (i) - B (i) \in ℂ \to ({(A (i) - B (i))}^{2} = 0 \leftrightarrow A (i) - B (i) = 0)$
26	24 25	syl	$⊢ (A (i) \in ℂ \land B (i) \in ℂ) \to ({(A (i) - B (i))}^{2} = 0 \leftrightarrow A (i) - B (i) = 0)$
27		subeq0	$⊢ (A (i) \in ℂ \land B (i) \in ℂ) \to (A (i) - B (i) = 0 \leftrightarrow A (i) = B (i))$
28	26 27	bitrd	$⊢ (A (i) \in ℂ \land B (i) \in ℂ) \to ({(A (i) - B (i))}^{2} = 0 \leftrightarrow A (i) = B (i))$
29	22 23 28	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} = 0 \leftrightarrow A (i) = B (i))$
30	29	anandirs	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land i \in (1 \dots N)) \to ({(A (i) - B (i))}^{2} = 0 \leftrightarrow A (i) = B (i))$
31	30	ralbidva	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (\forall i \in (1 \dots N) {(A (i) - B (i))}^{2} = 0 \leftrightarrow \forall i \in (1 \dots N) A (i) = B (i))$
32	21 31	bitrd	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (\sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = 0 \leftrightarrow \forall i \in (1 \dots N) A (i) = B (i))$
33	32	3adant3	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (\sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = 0 \leftrightarrow \forall i \in (1 \dots N) A (i) = B (i))$
34	12 33	bitrd	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (\sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - C (i))}^{2} \leftrightarrow \forall i \in (1 \dots N) A (i) = B (i))$
35		simp1	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to A \in 𝔼 (N)$
36		simp2	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to B \in 𝔼 (N)$
37		simp3	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to C \in 𝔼 (N)$
38		brcgr	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨C, C⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - C (i))}^{2})$
39	35 36 37 37 38	syl22anc	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (⟨A, B⟩ Cgr ⟨C, C⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - C (i))}^{2})$
40		eqeefv	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (A = B \leftrightarrow \forall i \in (1 \dots N) A (i) = B (i))$
41	40	3adant3	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (A = B \leftrightarrow \forall i \in (1 \dots N) A (i) = B (i))$
42	34 39 41	3bitr4d	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (⟨A, B⟩ Cgr ⟨C, C⟩ \leftrightarrow A = B)$
43	42	biimpd	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (⟨A, B⟩ Cgr ⟨C, C⟩ \to A = B)$
44	43	adantl	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨C, C⟩ \to A = B)$

Metamath Proof Explorer

Theorem axcgrid

Proof