Step | Hyp | Ref
| Expression |
1 | | dpjfval.p |
. 2
⊢ 𝑃 = (𝐺dProj𝑆) |
2 | | df-dpj 19597 |
. . . 4
⊢ dProj =
(𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “
{𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))))) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → dProj = (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))) |
4 | | simprr 770 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → 𝑠 = 𝑆) |
5 | 4 | dmeqd 5813 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → dom 𝑠 = dom 𝑆) |
6 | | dpjfval.2 |
. . . . . 6
⊢ (𝜑 → dom 𝑆 = 𝐼) |
7 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → dom 𝑆 = 𝐼) |
8 | 5, 7 | eqtrd 2780 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → dom 𝑠 = 𝐼) |
9 | | simprl 768 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → 𝑔 = 𝐺) |
10 | 9 | fveq2d 6775 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (proj1‘𝑔) =
(proj1‘𝐺)) |
11 | | dpjfval.q |
. . . . . 6
⊢ 𝑄 = (proj1‘𝐺) |
12 | 10, 11 | eqtr4di 2798 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (proj1‘𝑔) = 𝑄) |
13 | 4 | fveq1d 6773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (𝑠‘𝑖) = (𝑆‘𝑖)) |
14 | 8 | difeq1d 4061 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (dom 𝑠 ∖ {𝑖}) = (𝐼 ∖ {𝑖})) |
15 | 4, 14 | reseq12d 5891 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (𝑠 ↾ (dom 𝑠 ∖ {𝑖})) = (𝑆 ↾ (𝐼 ∖ {𝑖}))) |
16 | 9, 15 | oveq12d 7289 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))) = (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖})))) |
17 | 12, 13, 16 | oveq123d 7292 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))) = ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖}))))) |
18 | 8, 17 | mpteq12dv 5170 |
. . 3
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑠 = 𝑆)) → (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))) = (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖})))))) |
19 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
20 | 19 | sneqd 4579 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → {𝑔} = {𝐺}) |
21 | 20 | imaeq2d 5968 |
. . 3
⊢ ((𝜑 ∧ 𝑔 = 𝐺) → (dom DProd “ {𝑔}) = (dom DProd “ {𝐺})) |
22 | | dpjfval.1 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
23 | | dprdgrp 19606 |
. . . 4
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
24 | 22, 23 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Grp) |
25 | | reldmdprd 19598 |
. . . . 5
⊢ Rel dom
DProd |
26 | | elrelimasn 5992 |
. . . . 5
⊢ (Rel dom
DProd → (𝑆 ∈ (dom
DProd “ {𝐺}) ↔
𝐺dom DProd 𝑆)) |
27 | 25, 26 | ax-mp 5 |
. . . 4
⊢ (𝑆 ∈ (dom DProd “
{𝐺}) ↔ 𝐺dom DProd 𝑆) |
28 | 22, 27 | sylibr 233 |
. . 3
⊢ (𝜑 → 𝑆 ∈ (dom DProd “ {𝐺})) |
29 | 22, 6 | dprddomcld 19602 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
30 | 29 | mptexd 7097 |
. . 3
⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖}))))) ∈ V) |
31 | 3, 18, 21, 24, 28, 30 | ovmpodx 7418 |
. 2
⊢ (𝜑 → (𝐺dProj𝑆) = (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖})))))) |
32 | 1, 31 | eqtrid 2792 |
1
⊢ (𝜑 → 𝑃 = (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖})))))) |