Metamath Proof Explorer

Theorem ecgrtg

Description: The congruence relation used in the Tarski structure for the Euclidean geometry is the same as Cgr . (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Hypotheses ecgrtg.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
ecgrtg.2 ⊢ 𝑃 = ( Base ‘ ( EEG ‘ 𝑁 ) )
ecgrtg.3 ⊢ − = ( dist ‘ ( EEG ‘ 𝑁 ) )
ecgrtg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
ecgrtg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
ecgrtg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
ecgrtg.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
Assertion ecgrtg ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 ecgrtg.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 ecgrtg.2 ⊢ 𝑃 = ( Base ‘ ( EEG ‘ 𝑁 ) )
3 ecgrtg.3 ⊢ − = ( dist ‘ ( EEG ‘ 𝑁 ) )
4 ecgrtg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5 ecgrtg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6 ecgrtg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7 ecgrtg.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
8 eengbas ⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
9 1 8 syl ⊢ ( 𝜑 → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
10 9 2 eqtr4di ⊢ ( 𝜑 → ( 𝔼 ‘ 𝑁 ) = 𝑃 )
11 4 10 eleqtrrd ⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
12 5 10 eleqtrrd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
13 6 10 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
14 7 10 eleqtrrd ⊢ ( 𝜑 → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
15 brcgr ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
16 11 12 13 14 15 syl22anc ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
17 dsid ⊢ dist = Slot ( dist ‘ ndx )
18 fvexd ⊢ ( 𝜑 → ( EEG ‘ 𝑁 ) ∈ V )
19 eengstr ⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) Struct ⟨ 1 , 1 7 ⟩ )
20 1 19 syl ⊢ ( 𝜑 → ( EEG ‘ 𝑁 ) Struct ⟨ 1 , 1 7 ⟩ )
21 structn0fun ⊢ ( ( EEG ‘ 𝑁 ) Struct ⟨ 1 , 1 7 ⟩ → Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
22 20 21 syl ⊢ ( 𝜑 → Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
23 structcnvcnv ⊢ ( ( EEG ‘ 𝑁 ) Struct ⟨ 1 , 1 7 ⟩ → ◡ ◡ ( EEG ‘ 𝑁 ) = ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
24 20 23 syl ⊢ ( 𝜑 → ◡ ◡ ( EEG ‘ 𝑁 ) = ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
25 24 funeqd ⊢ ( 𝜑 → ( Fun ◡ ◡ ( EEG ‘ 𝑁 ) ↔ Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) ) )
26 22 25 mpbird ⊢ ( 𝜑 → Fun ◡ ◡ ( EEG ‘ 𝑁 ) )
27 opex ⊢ ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ ∈ V
28 27 prid2 ⊢ ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ ∈ { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ }
29 elun1 ⊢ ( ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ ∈ { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } → ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
30 28 29 ax-mp ⊢ ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } )
31 eengv ⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
32 1 31 syl ⊢ ( 𝜑 → ( EEG ‘ 𝑁 ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
33 30 32 eleqtrrid ⊢ ( 𝜑 → ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ ∈ ( EEG ‘ 𝑁 ) )
34 fvex ⊢ ( 𝔼 ‘ 𝑁 ) ∈ V
35 34 34 mpoex ⊢ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ V
36 35 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ V )
37 17 18 26 33 36 strfv2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) = ( dist ‘ ( EEG ‘ 𝑁 ) ) )
38 3 37 eqtr4id ⊢ ( 𝜑 → − = ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) )
39 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑥 = 𝐴 )
40 39 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
41 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑦 = 𝐵 )
42 41 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) )
43 40 42 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) )
44 43 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) )
45 44 sumeq2dv ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) )
46 sumex ⊢ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ∈ V
47 46 a1i ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ∈ V )
48 38 45 11 12 47 ovmpod ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) )
49 48 eqcomd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = ( 𝐴 − 𝐵 ) )
50 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑥 = 𝐶 )
51 50 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑖 ) )
52 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑦 = 𝐷 )
53 52 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑖 ) )
54 51 53 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) = ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) )
55 54 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
56 55 sumeq2dv ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
57 sumex ⊢ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ∈ V
58 57 a1i ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ∈ V )
59 38 56 13 14 58 ovmpod ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
60 59 eqcomd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) = ( 𝐶 − 𝐷 ) )
61 49 60 eqeq12d ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) )
62 16 61 bitrd ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) )