| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ecgrtg.a | . . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) | 
| 2 |  | ecgrtg.1 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 3 |  | eengbas 28997 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) | 
| 4 | 2, 3 | syl 17 | . . . . 5
⊢ (𝜑 → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) | 
| 5 |  | ecgrtg.2 | . . . . 5
⊢ 𝑃 = (Base‘(EEG‘𝑁)) | 
| 6 | 4, 5 | eqtr4di 2794 | . . . 4
⊢ (𝜑 → (𝔼‘𝑁) = 𝑃) | 
| 7 | 1, 6 | eleqtrrd 2843 | . . 3
⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) | 
| 8 |  | ecgrtg.b | . . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) | 
| 9 | 8, 6 | eleqtrrd 2843 | . . 3
⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) | 
| 10 |  | ecgrtg.c | . . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) | 
| 11 | 10, 6 | eleqtrrd 2843 | . . 3
⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) | 
| 12 |  | ecgrtg.d | . . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑃) | 
| 13 | 12, 6 | eleqtrrd 2843 | . . 3
⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) | 
| 14 |  | brcgr 28916 | . . 3
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))) | 
| 15 | 7, 9, 11, 13, 14 | syl22anc 838 | . 2
⊢ (𝜑 → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))) | 
| 16 |  | ecgrtg.3 | . . . . . 6
⊢  − =
(dist‘(EEG‘𝑁)) | 
| 17 |  | dsid 17431 | . . . . . . 7
⊢ dist =
Slot (dist‘ndx) | 
| 18 |  | fvexd 6920 | . . . . . . 7
⊢ (𝜑 → (EEG‘𝑁) ∈ V) | 
| 19 |  | eengstr 28996 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) Struct
〈1, ;17〉) | 
| 20 | 2, 19 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (EEG‘𝑁) Struct 〈1, ;17〉) | 
| 21 |  | structn0fun 17189 | . . . . . . . . 9
⊢
((EEG‘𝑁)
Struct 〈1, ;17〉 →
Fun ((EEG‘𝑁) ∖
{∅})) | 
| 22 | 20, 21 | syl 17 | . . . . . . . 8
⊢ (𝜑 → Fun ((EEG‘𝑁) ∖
{∅})) | 
| 23 |  | structcnvcnv 17191 | . . . . . . . . . 10
⊢
((EEG‘𝑁)
Struct 〈1, ;17〉 →
◡◡(EEG‘𝑁) = ((EEG‘𝑁) ∖ {∅})) | 
| 24 | 20, 23 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ◡◡(EEG‘𝑁) = ((EEG‘𝑁) ∖ {∅})) | 
| 25 | 24 | funeqd 6587 | . . . . . . . 8
⊢ (𝜑 → (Fun ◡◡(EEG‘𝑁) ↔ Fun ((EEG‘𝑁) ∖ {∅}))) | 
| 26 | 22, 25 | mpbird 257 | . . . . . . 7
⊢ (𝜑 → Fun ◡◡(EEG‘𝑁)) | 
| 27 |  | opex 5468 | . . . . . . . . . 10
⊢
〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈ V | 
| 28 | 27 | prid2 4762 | . . . . . . . . 9
⊢
〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈
{〈(Base‘ndx), (𝔼‘𝑁)〉, 〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉} | 
| 29 |  | elun1 4181 | . . . . . . . . 9
⊢
(〈(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 5 | . . . . . . . 8
⊢
〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈
({〈(Base‘ndx), (𝔼‘𝑁)〉, 〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉} ∪
{〈(Itv‘ndx), (𝑥
∈ (𝔼‘𝑁),
𝑦 ∈
(𝔼‘𝑁) ↦
{𝑧 ∈
(𝔼‘𝑁) ∣
𝑧 Btwn 〈𝑥, 𝑦〉})〉, 〈(LineG‘ndx),
(𝑥 ∈
(𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn 〈𝑥, 𝑦〉 ∨ 𝑥 Btwn 〈𝑧, 𝑦〉 ∨ 𝑦 Btwn 〈𝑥, 𝑧〉)})〉}) | 
| 31 |  | eengv 28995 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) =
({〈(Base‘ndx), (𝔼‘𝑁)〉, 〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉} ∪
{〈(Itv‘ndx), (𝑥
∈ (𝔼‘𝑁),
𝑦 ∈
(𝔼‘𝑁) ↦
{𝑧 ∈
(𝔼‘𝑁) ∣
𝑧 Btwn 〈𝑥, 𝑦〉})〉, 〈(LineG‘ndx),
(𝑥 ∈
(𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn 〈𝑥, 𝑦〉 ∨ 𝑥 Btwn 〈𝑧, 𝑦〉 ∨ 𝑦 Btwn 〈𝑥, 𝑧〉)})〉})) | 
| 32 | 2, 31 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (EEG‘𝑁) = ({〈(Base‘ndx),
(𝔼‘𝑁)〉,
〈(dist‘ndx), (𝑥
∈ (𝔼‘𝑁),
𝑦 ∈
(𝔼‘𝑁) ↦
Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉} ∪
{〈(Itv‘ndx), (𝑥
∈ (𝔼‘𝑁),
𝑦 ∈
(𝔼‘𝑁) ↦
{𝑧 ∈
(𝔼‘𝑁) ∣
𝑧 Btwn 〈𝑥, 𝑦〉})〉, 〈(LineG‘ndx),
(𝑥 ∈
(𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn 〈𝑥, 𝑦〉 ∨ 𝑥 Btwn 〈𝑧, 𝑦〉 ∨ 𝑦 Btwn 〈𝑥, 𝑧〉)})〉})) | 
| 33 | 30, 32 | eleqtrrid 2847 | . . . . . . 7
⊢ (𝜑 → 〈(dist‘ndx),
(𝑥 ∈
(𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈ (EEG‘𝑁)) | 
| 34 |  | fvex 6918 | . . . . . . . . 9
⊢
(𝔼‘𝑁)
∈ V | 
| 35 | 34, 34 | mpoex 8105 | . . . . . . . 8
⊢ (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)) ∈ V | 
| 36 | 35 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)) ∈ V) | 
| 37 | 17, 18, 26, 33, 36 | strfv2d 17239 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)) = (dist‘(EEG‘𝑁))) | 
| 38 | 16, 37 | eqtr4id 2795 | . . . . 5
⊢ (𝜑 → − = (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))) | 
| 39 |  | simplrl 776 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 = 𝐴) | 
| 40 | 39 | fveq1d 6907 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (𝐴‘𝑖)) | 
| 41 |  | simplrr 777 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑦 = 𝐵) | 
| 42 | 41 | fveq1d 6907 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = (𝐵‘𝑖)) | 
| 43 | 40, 42 | oveq12d 7450 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) − (𝑦‘𝑖)) = ((𝐴‘𝑖) − (𝐵‘𝑖))) | 
| 44 | 43 | oveq1d 7447 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) | 
| 45 | 44 | sumeq2dv 15739 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) | 
| 46 |  | sumex 15725 | . . . . . 6
⊢
Σ𝑖 ∈
(1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ V | 
| 47 | 46 | a1i 11 | . . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ V) | 
| 48 | 38, 45, 7, 9, 47 | ovmpod 7586 | . . . 4
⊢ (𝜑 → (𝐴 − 𝐵) = Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) | 
| 49 | 48 | eqcomd 2742 | . . 3
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = (𝐴 − 𝐵)) | 
| 50 |  | simplrl 776 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 = 𝐶) | 
| 51 | 50 | fveq1d 6907 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (𝐶‘𝑖)) | 
| 52 |  | simplrr 777 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑦 = 𝐷) | 
| 53 | 52 | fveq1d 6907 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = (𝐷‘𝑖)) | 
| 54 | 51, 53 | oveq12d 7450 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) − (𝑦‘𝑖)) = ((𝐶‘𝑖) − (𝐷‘𝑖))) | 
| 55 | 54 | oveq1d 7447 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = (((𝐶‘𝑖) − (𝐷‘𝑖))↑2)) | 
| 56 | 55 | sumeq2dv 15739 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) → Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)) | 
| 57 |  | sumex 15725 | . . . . . 6
⊢
Σ𝑖 ∈
(1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ V | 
| 58 | 57 | a1i 11 | . . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ V) | 
| 59 | 38, 56, 11, 13, 58 | ovmpod 7586 | . . . 4
⊢ (𝜑 → (𝐶 − 𝐷) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)) | 
| 60 | 59 | eqcomd 2742 | . . 3
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) = (𝐶 − 𝐷)) | 
| 61 | 49, 60 | eqeq12d 2752 | . 2
⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ↔ (𝐴 − 𝐵) = (𝐶 − 𝐷))) | 
| 62 | 15, 61 | bitrd 279 | 1
⊢ (𝜑 → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ (𝐴 − 𝐵) = (𝐶 − 𝐷))) |