Step | Hyp | Ref
| Expression |
1 | | ecgrtg.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
2 | | ecgrtg.1 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | | eengbas 25661 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
5 | | ecgrtg.2 |
. . . . 5
⊢ 𝑃 = (Base‘(EEG‘𝑁)) |
6 | 4, 5 | syl6eqr 2662 |
. . . 4
⊢ (𝜑 → (𝔼‘𝑁) = 𝑃) |
7 | 1, 6 | eleqtrrd 2691 |
. . 3
⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) |
8 | | ecgrtg.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
9 | 8, 6 | eleqtrrd 2691 |
. . 3
⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) |
10 | | ecgrtg.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
11 | 10, 6 | eleqtrrd 2691 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) |
12 | | ecgrtg.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
13 | 12, 6 | eleqtrrd 2691 |
. . 3
⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) |
14 | | brcgr 25580 |
. . 3
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))) |
15 | 7, 9, 11, 13, 14 | syl22anc 1319 |
. 2
⊢ (𝜑 → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))) |
16 | | dsid 15886 |
. . . . . . 7
⊢ dist =
Slot (dist‘ndx) |
17 | | fvex 6113 |
. . . . . . . 8
⊢
(EEG‘𝑁) ∈
V |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (EEG‘𝑁) ∈ V) |
19 | | eengstr 25660 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) Struct
〈1, ;17〉) |
20 | 2, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (EEG‘𝑁) Struct 〈1, ;17〉) |
21 | | isstruct 15705 |
. . . . . . . . . 10
⊢
((EEG‘𝑁)
Struct 〈1, ;17〉 ↔
((1 ∈ ℕ ∧ ;17
∈ ℕ ∧ 1 ≤ ;17)
∧ Fun ((EEG‘𝑁)
∖ {∅}) ∧ dom (EEG‘𝑁) ⊆ (1...;17))) |
22 | 21 | simp2bi 1070 |
. . . . . . . . 9
⊢
((EEG‘𝑁)
Struct 〈1, ;17〉 →
Fun ((EEG‘𝑁) ∖
{∅})) |
23 | 20, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Fun ((EEG‘𝑁) ∖
{∅})) |
24 | | structcnvcnv 15706 |
. . . . . . . . . 10
⊢
((EEG‘𝑁)
Struct 〈1, ;17〉 →
◡◡(EEG‘𝑁) = ((EEG‘𝑁) ∖ {∅})) |
25 | 20, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ◡◡(EEG‘𝑁) = ((EEG‘𝑁) ∖ {∅})) |
26 | 25 | funeqd 5825 |
. . . . . . . 8
⊢ (𝜑 → (Fun ◡◡(EEG‘𝑁) ↔ Fun ((EEG‘𝑁) ∖ {∅}))) |
27 | 23, 26 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → Fun ◡◡(EEG‘𝑁)) |
28 | | opex 4859 |
. . . . . . . . . 10
⊢
〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈ V |
29 | 28 | prid2 4242 |
. . . . . . . . 9
⊢
〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈
{〈(Base‘ndx), (𝔼‘𝑁)〉, 〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉} |
30 | | elun1 3742 |
. . . . . . . . 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 〈𝑥, 𝑧〉)})〉})) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . 8
⊢
〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈
({〈(Base‘ndx), (𝔼‘𝑁)〉, 〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉} ∪
{〈(Itv‘ndx), (𝑥
∈ (𝔼‘𝑁),
𝑦 ∈
(𝔼‘𝑁) ↦
{𝑧 ∈
(𝔼‘𝑁) ∣
𝑧 Btwn 〈𝑥, 𝑦〉})〉, 〈(LineG‘ndx),
(𝑥 ∈
(𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn 〈𝑥, 𝑦〉 ∨ 𝑥 Btwn 〈𝑧, 𝑦〉 ∨ 𝑦 Btwn 〈𝑥, 𝑧〉)})〉}) |
32 | | eengv 25659 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) =
({〈(Base‘ndx), (𝔼‘𝑁)〉, 〈(dist‘ndx), (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉} ∪
{〈(Itv‘ndx), (𝑥
∈ (𝔼‘𝑁),
𝑦 ∈
(𝔼‘𝑁) ↦
{𝑧 ∈
(𝔼‘𝑁) ∣
𝑧 Btwn 〈𝑥, 𝑦〉})〉, 〈(LineG‘ndx),
(𝑥 ∈
(𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn 〈𝑥, 𝑦〉 ∨ 𝑥 Btwn 〈𝑧, 𝑦〉 ∨ 𝑦 Btwn 〈𝑥, 𝑧〉)})〉})) |
33 | 2, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (EEG‘𝑁) = ({〈(Base‘ndx),
(𝔼‘𝑁)〉,
〈(dist‘ndx), (𝑥
∈ (𝔼‘𝑁),
𝑦 ∈
(𝔼‘𝑁) ↦
Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉} ∪
{〈(Itv‘ndx), (𝑥
∈ (𝔼‘𝑁),
𝑦 ∈
(𝔼‘𝑁) ↦
{𝑧 ∈
(𝔼‘𝑁) ∣
𝑧 Btwn 〈𝑥, 𝑦〉})〉, 〈(LineG‘ndx),
(𝑥 ∈
(𝔼‘𝑁), 𝑦 ∈ ((𝔼‘𝑁) ∖ {𝑥}) ↦ {𝑧 ∈ (𝔼‘𝑁) ∣ (𝑧 Btwn 〈𝑥, 𝑦〉 ∨ 𝑥 Btwn 〈𝑧, 𝑦〉 ∨ 𝑦 Btwn 〈𝑥, 𝑧〉)})〉})) |
34 | 31, 33 | syl5eleqr 2695 |
. . . . . . 7
⊢ (𝜑 → 〈(dist‘ndx),
(𝑥 ∈
(𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))〉 ∈ (EEG‘𝑁)) |
35 | | fvex 6113 |
. . . . . . . . 9
⊢
(𝔼‘𝑁)
∈ V |
36 | 35, 35 | mpt2ex 7136 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)) ∈ V |
37 | 36 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)) ∈ V) |
38 | 16, 18, 27, 34, 37 | strfv2d 15733 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2)) = (dist‘(EEG‘𝑁))) |
39 | | ecgrtg.3 |
. . . . . 6
⊢ − =
(dist‘(EEG‘𝑁)) |
40 | 38, 39 | syl6reqr 2663 |
. . . . 5
⊢ (𝜑 → − = (𝑥 ∈ (𝔼‘𝑁), 𝑦 ∈ (𝔼‘𝑁) ↦ Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2))) |
41 | | simplrl 796 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 = 𝐴) |
42 | 41 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (𝐴‘𝑖)) |
43 | | simplrr 797 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑦 = 𝐵) |
44 | 43 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = (𝐵‘𝑖)) |
45 | 42, 44 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) − (𝑦‘𝑖)) = ((𝐴‘𝑖) − (𝐵‘𝑖))) |
46 | 45 | oveq1d 6564 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) |
47 | 46 | sumeq2dv 14281 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) |
48 | | sumex 14266 |
. . . . . 6
⊢
Σ𝑖 ∈
(1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ V |
49 | 48 | a1i 11 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ V) |
50 | 40, 47, 7, 9, 49 | ovmpt2d 6686 |
. . . 4
⊢ (𝜑 → (𝐴 − 𝐵) = Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) |
51 | 50 | eqcomd 2616 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = (𝐴 − 𝐵)) |
52 | | simplrl 796 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 = 𝐶) |
53 | 52 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (𝐶‘𝑖)) |
54 | | simplrr 797 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑦 = 𝐷) |
55 | 54 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = (𝐷‘𝑖)) |
56 | 53, 55 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) − (𝑦‘𝑖)) = ((𝐶‘𝑖) − (𝐷‘𝑖))) |
57 | 56 | oveq1d 6564 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = (((𝐶‘𝑖) − (𝐷‘𝑖))↑2)) |
58 | 57 | sumeq2dv 14281 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) → Σ𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) − (𝑦‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)) |
59 | | sumex 14266 |
. . . . . 6
⊢
Σ𝑖 ∈
(1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ V |
60 | 59 | a1i 11 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ V) |
61 | 40, 58, 11, 13, 60 | ovmpt2d 6686 |
. . . 4
⊢ (𝜑 → (𝐶 − 𝐷) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)) |
62 | 61 | eqcomd 2616 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) = (𝐶 − 𝐷)) |
63 | 51, 62 | eqeq12d 2625 |
. 2
⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ↔ (𝐴 − 𝐵) = (𝐶 − 𝐷))) |
64 | 15, 63 | bitrd 267 |
1
⊢ (𝜑 → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ (𝐴 − 𝐵) = (𝐶 − 𝐷))) |