Step | Hyp | Ref
| Expression |
1 | | ecgrtg.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
2 | | ecgrtg.1 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | | eengbas 26330 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
5 | | ecgrtg.2 |
. . . . 5
⊢ 𝑃 = (Base‘(EEG‘𝑁)) |
6 | 4, 5 | syl6eqr 2831 |
. . . 4
⊢ (𝜑 → (𝔼‘𝑁) = 𝑃) |
7 | 1, 6 | eleqtrrd 2861 |
. . 3
⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) |
8 | | ecgrtg.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
9 | 8, 6 | eleqtrrd 2861 |
. . 3
⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) |
10 | | ecgrtg.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
11 | 10, 6 | eleqtrrd 2861 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) |
12 | | ecgrtg.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
13 | 12, 6 | eleqtrrd 2861 |
. . 3
⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) |
14 | | brcgr 26249 |
. . 3
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))) |
15 | 7, 9, 11, 13, 14 | syl22anc 829 |
. 2
⊢ (𝜑 → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))) |
16 | | dsid 16449 |
. . . . . . 7
⊢ dist =
Slot (dist‘ndx) |
17 | | fvexd 6461 |
. . . . . . 7
⊢ (𝜑 → (EEG‘𝑁) ∈ V) |
18 | | eengstr 26329 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) Struct
〈1, ;17〉) |
19 | 2, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (EEG‘𝑁) Struct 〈1, ;17〉) |
20 | | isstruct 16268 |
. . . . . . . . . 10
⊢
((EEG‘𝑁)
Struct 〈1, ;17〉 ↔
((1 ∈ ℕ ∧ ;17
∈ ℕ ∧ 1 ≤ ;17)
∧ Fun ((EEG‘𝑁)
∖ {∅}) ∧ dom (EEG‘𝑁) ⊆ (1...;17))) |
21 | 20 | simp2bi 1137 |
. . . . . . . . 9
⊢
((EEG‘𝑁)
Struct 〈1, ;17〉 →
Fun ((EEG‘𝑁) ∖
{∅})) |
22 | 19, 21 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Fun ((EEG‘𝑁) ∖
{∅})) |
23 | | structcnvcnv 16269 |
. . . . . . . . . 10
⊢
((EEG‘𝑁)
Struct 〈1, ;17〉 →
◡◡(EEG‘𝑁) = ((EEG‘𝑁) ∖ {∅})) |
24 | 19, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ◡◡(EEG‘𝑁) = ((EEG‘𝑁) ∖ {∅})) |
25 | 24 | funeqd 6157 |
. . . . . . . 8
⊢ (𝜑 → (Fun ◡◡(EEG‘𝑁) ↔ Fun ((EEG‘𝑁) ∖ {∅}))) |
26 | 22, 25 | mpbird 249 |
. . . . . . 7
⊢ (𝜑 → Fun ◡◡(EEG‘𝑁)) |
27 | | opex 5164 |
. . . . . . . . . 10
⊢
〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈ V |
28 | 27 | prid2 4529 |
. . . . . . . . 9
⊢
〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈
{〈(Base‘ndx), (𝔼‘𝑁)〉, 〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉} |
29 | | elun1 4002 |
. . . . . . . . 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 26328 |
. . . . . . . . 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 | syl5eleqr 2865 |
. . . . . . 7
⊢ (𝜑 → 〈(dist‘ndx),
(𝑥 ∈
(𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈ (EEG‘𝑁)) |
34 | | fvex 6459 |
. . . . . . . . 9
⊢
(𝔼‘𝑁)
∈ V |
35 | 34, 34 | mpt2ex 7527 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)) ∈ V |
36 | 35 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)) ∈ V) |
37 | 16, 17, 26, 33, 36 | strfv2d 16301 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)) = (dist‘(EEG‘𝑁))) |
38 | | ecgrtg.3 |
. . . . . 6
⊢ − =
(dist‘(EEG‘𝑁)) |
39 | 37, 38 | syl6reqr 2832 |
. . . . 5
⊢ (𝜑 → − = (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))) |
40 | | simplrl 767 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 = 𝐴) |
41 | 40 | fveq1d 6448 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (𝐴‘𝑖)) |
42 | | simplrr 768 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑦 = 𝐵) |
43 | 42 | fveq1d 6448 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = (𝐵‘𝑖)) |
44 | 41, 43 | oveq12d 6940 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) − (𝑦‘𝑖)) = ((𝐴‘𝑖) − (𝐵‘𝑖))) |
45 | 44 | oveq1d 6937 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) |
46 | 45 | sumeq2dv 14841 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) |
47 | | sumex 14826 |
. . . . . 6
⊢
Σ𝑖 ∈
(1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ V |
48 | 47 | a1i 11 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ V) |
49 | 39, 46, 7, 9, 48 | ovmpt2d 7065 |
. . . 4
⊢ (𝜑 → (𝐴 − 𝐵) = Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) |
50 | 49 | eqcomd 2783 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = (𝐴 − 𝐵)) |
51 | | simplrl 767 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 = 𝐶) |
52 | 51 | fveq1d 6448 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (𝐶‘𝑖)) |
53 | | simplrr 768 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑦 = 𝐷) |
54 | 53 | fveq1d 6448 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = (𝐷‘𝑖)) |
55 | 52, 54 | oveq12d 6940 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) − (𝑦‘𝑖)) = ((𝐶‘𝑖) − (𝐷‘𝑖))) |
56 | 55 | oveq1d 6937 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = (((𝐶‘𝑖) − (𝐷‘𝑖))↑2)) |
57 | 56 | sumeq2dv 14841 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) → Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)) |
58 | | sumex 14826 |
. . . . . 6
⊢
Σ𝑖 ∈
(1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ V |
59 | 58 | a1i 11 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ V) |
60 | 39, 57, 11, 13, 59 | ovmpt2d 7065 |
. . . 4
⊢ (𝜑 → (𝐶 − 𝐷) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)) |
61 | 60 | eqcomd 2783 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) = (𝐶 − 𝐷)) |
62 | 50, 61 | eqeq12d 2792 |
. 2
⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ↔ (𝐴 − 𝐵) = (𝐶 − 𝐷))) |
63 | 15, 62 | bitrd 271 |
1
⊢ (𝜑 → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ (𝐴 − 𝐵) = (𝐶 − 𝐷))) |