Step | Hyp | Ref
| Expression |
1 | | dpjfval.p |
. 2
⊢ 𝑃 = (𝐺dProj𝑆) |
2 | | df-dpj 18218 |
. . . 4
⊢ dProj =
(𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “
{𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))))) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → dProj = (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))) |
4 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → 𝑠 = 𝑆) |
5 | 4 | dmeqd 5248 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → dom 𝑠 = dom 𝑆) |
6 | | dpjfval.2 |
. . . . . 6
⊢ (𝜑 → dom 𝑆 = 𝐼) |
7 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → dom 𝑆 = 𝐼) |
8 | 5, 7 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → dom 𝑠 = 𝐼) |
9 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → 𝑔 = 𝐺) |
10 | 9 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (proj1‘𝑔) =
(proj1‘𝐺)) |
11 | | dpjfval.q |
. . . . . 6
⊢ 𝑄 = (proj1‘𝐺) |
12 | 10, 11 | syl6eqr 2662 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (proj1‘𝑔) = 𝑄) |
13 | 4 | fveq1d 6105 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (𝑠‘𝑖) = (𝑆‘𝑖)) |
14 | 8 | difeq1d 3689 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (dom 𝑠 ∖ {𝑖}) = (𝐼 ∖ {𝑖})) |
15 | 4, 14 | reseq12d 5318 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (𝑠 ↾ (dom 𝑠 ∖ {𝑖})) = (𝑆 ↾ (𝐼 ∖ {𝑖}))) |
16 | 9, 15 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))) = (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖})))) |
17 | 12, 13, 16 | oveq123d 6570 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))) = ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖}))))) |
18 | 8, 17 | mpteq12dv 4663 |
. . 3
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))) = (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖})))))) |
19 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
20 | 19 | sneqd 4137 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → {𝑔} = {𝐺}) |
21 | 20 | imaeq2d 5385 |
. . 3
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (dom DProd “ {𝑔}) = (dom DProd “ {𝐺})) |
22 | | dpjfval.1 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
23 | | dprdgrp 18227 |
. . . 4
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
24 | 22, 23 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Grp) |
25 | | reldmdprd 18219 |
. . . . 5
⊢ Rel dom
DProd |
26 | | elrelimasn 5408 |
. . . . 5
⊢ (Rel dom
DProd → (𝑆 ∈ (dom
DProd “ {𝐺}) ↔
𝐺dom DProd 𝑆)) |
27 | 25, 26 | ax-mp 5 |
. . . 4
⊢ (𝑆 ∈ (dom DProd “
{𝐺}) ↔ 𝐺dom DProd 𝑆) |
28 | 22, 27 | sylibr 223 |
. . 3
⊢ (𝜑 → 𝑆 ∈ (dom DProd “ {𝐺})) |
29 | 22, 6 | dprddomcld 18223 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
30 | | mptexg 6389 |
. . . 4
⊢ (𝐼 ∈ V → (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖}))))) ∈ V) |
31 | 29, 30 | syl 17 |
. . 3
⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖}))))) ∈ V) |
32 | 3, 18, 21, 24, 28, 31 | ovmpt2dx 6685 |
. 2
⊢ (𝜑 → (𝐺dProj𝑆) = (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖})))))) |
33 | 1, 32 | syl5eq 2656 |
1
⊢ (𝜑 → 𝑃 = (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖})))))) |