| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . 2
⊢ ((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) → 𝐺dom DProd 𝑆) | 
| 2 |  | reldmdprd 20018 | . . . . . 6
⊢ Rel dom
DProd | 
| 3 | 2 | brrelex2i 5741 | . . . . 5
⊢ (𝐺dom DProd 𝑆 → 𝑆 ∈ V) | 
| 4 | 3 | adantr 480 | . . . 4
⊢ ((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) → 𝑆 ∈ V) | 
| 5 | 2 | brrelex1i 5740 | . . . . . 6
⊢ (𝐺dom DProd 𝑠 → 𝐺 ∈ V) | 
| 6 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑔dom DProd 𝑠 ↔ 𝐺dom DProd 𝑠)) | 
| 7 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑔 DProd 𝑠) = (𝐺 DProd 𝑠)) | 
| 8 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑔 = 𝐺 → (0g‘𝑔) = (0g‘𝐺)) | 
| 9 |  | dprdval.0 | . . . . . . . . . . . . . 14
⊢  0 =
(0g‘𝐺) | 
| 10 | 8, 9 | eqtr4di 2794 | . . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (0g‘𝑔) = 0 ) | 
| 11 | 10 | breq2d 5154 | . . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (ℎ finSupp (0g‘𝑔) ↔ ℎ finSupp 0 )) | 
| 12 | 11 | rabbidv 3443 | . . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} = {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 }) | 
| 13 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑔 Σg 𝑓) = (𝐺 Σg 𝑓)) | 
| 14 | 12, 13 | mpteq12dv 5232 | . . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)) = (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓))) | 
| 15 | 14 | rneqd 5948 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓))) | 
| 16 | 7, 15 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑔 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)) ↔ (𝐺 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓)))) | 
| 17 | 6, 16 | imbi12d 344 | . . . . . . 7
⊢ (𝑔 = 𝐺 → ((𝑔dom DProd 𝑠 → (𝑔 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓))) ↔ (𝐺dom DProd 𝑠 → (𝐺 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓))))) | 
| 18 |  | df-br 5143 | . . . . . . . . 9
⊢ (𝑔dom DProd 𝑠 ↔ 〈𝑔, 𝑠〉 ∈ dom DProd ) | 
| 19 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠‘𝑖) ∈ V | 
| 20 | 19 | rgenw 3064 | . . . . . . . . . . . . . . . 16
⊢
∀𝑖 ∈ dom
𝑠(𝑠‘𝑖) ∈ V | 
| 21 |  | ixpexg 8963 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑖 ∈
dom 𝑠(𝑠‘𝑖) ∈ V → X𝑖 ∈
dom 𝑠(𝑠‘𝑖) ∈ V) | 
| 22 | 20, 21 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢ X𝑖 ∈
dom 𝑠(𝑠‘𝑖) ∈ V | 
| 23 | 22 | mptrabex 7246 | . . . . . . . . . . . . . 14
⊢ (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)) ∈ V | 
| 24 | 23 | rnex 7933 | . . . . . . . . . . . . 13
⊢ ran
(𝑓 ∈ {ℎ ∈ X𝑖 ∈
dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)) ∈ V | 
| 25 | 24 | rgen2w 3065 | . . . . . . . . . . . 12
⊢
∀𝑔 ∈ Grp
∀𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))}ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)) ∈ V | 
| 26 |  | df-dprd 20016 | . . . . . . . . . . . . 13
⊢  DProd =
(𝑔 ∈ Grp, 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))} ↦ ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓))) | 
| 27 | 26 | fmpox 8093 | . . . . . . . . . . . 12
⊢
(∀𝑔 ∈
Grp ∀𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))}ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)) ∈ V ↔ DProd
:∪ 𝑔 ∈ Grp ({𝑔} × {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))})⟶V) | 
| 28 | 25, 27 | mpbi 230 | . . . . . . . . . . 11
⊢  DProd
:∪ 𝑔 ∈ Grp ({𝑔} × {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))})⟶V | 
| 29 | 28 | fdmi 6746 | . . . . . . . . . 10
⊢ dom DProd
= ∪ 𝑔 ∈ Grp ({𝑔} × {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))}) | 
| 30 | 29 | eleq2i 2832 | . . . . . . . . 9
⊢
(〈𝑔, 𝑠〉 ∈ dom DProd ↔
〈𝑔, 𝑠〉 ∈ ∪ 𝑔 ∈ Grp ({𝑔} × {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))})) | 
| 31 |  | opeliunxp 5751 | . . . . . . . . 9
⊢
(〈𝑔, 𝑠〉 ∈ ∪ 𝑔 ∈ Grp ({𝑔} × {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))}) ↔ (𝑔 ∈ Grp ∧ 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))})) | 
| 32 | 18, 30, 31 | 3bitri 297 | . . . . . . . 8
⊢ (𝑔dom DProd 𝑠 ↔ (𝑔 ∈ Grp ∧ 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))})) | 
| 33 | 26 | ovmpt4g 7581 | . . . . . . . . 9
⊢ ((𝑔 ∈ Grp ∧ 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))} ∧ ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)) ∈ V) → (𝑔 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓))) | 
| 34 | 24, 33 | mp3an3 1451 | . . . . . . . 8
⊢ ((𝑔 ∈ Grp ∧ 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑖 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑖})(ℎ‘𝑖) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑖) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑖})))) =
{(0g‘𝑔)}))}) → (𝑔 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓))) | 
| 35 | 32, 34 | sylbi 217 | . . . . . . 7
⊢ (𝑔dom DProd 𝑠 → (𝑔 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓))) | 
| 36 | 17, 35 | vtoclg 3553 | . . . . . 6
⊢ (𝐺 ∈ V → (𝐺dom DProd 𝑠 → (𝐺 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓)))) | 
| 37 | 5, 36 | mpcom 38 | . . . . 5
⊢ (𝐺dom DProd 𝑠 → (𝐺 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓))) | 
| 38 | 37 | sbcth 3802 | . . . 4
⊢ (𝑆 ∈ V → [𝑆 / 𝑠](𝐺dom DProd 𝑠 → (𝐺 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓)))) | 
| 39 | 4, 38 | syl 17 | . . 3
⊢ ((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) → [𝑆 / 𝑠](𝐺dom DProd 𝑠 → (𝐺 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓)))) | 
| 40 |  | simpr 484 | . . . . . 6
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) | 
| 41 | 40 | breq2d 5154 | . . . . 5
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑆)) | 
| 42 | 40 | oveq2d 7448 | . . . . . 6
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑆)) | 
| 43 | 40 | dmeqd 5915 | . . . . . . . . . . . . 13
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → dom 𝑠 = dom 𝑆) | 
| 44 |  | simplr 768 | . . . . . . . . . . . . 13
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → dom 𝑆 = 𝐼) | 
| 45 | 43, 44 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → dom 𝑠 = 𝐼) | 
| 46 | 45 | ixpeq1d 8950 | . . . . . . . . . . 11
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → X𝑖 ∈ dom 𝑠(𝑠‘𝑖) = X𝑖 ∈ 𝐼 (𝑠‘𝑖)) | 
| 47 | 40 | fveq1d 6907 | . . . . . . . . . . . 12
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → (𝑠‘𝑖) = (𝑆‘𝑖)) | 
| 48 | 47 | ixpeq2dv 8954 | . . . . . . . . . . 11
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → X𝑖 ∈ 𝐼 (𝑠‘𝑖) = X𝑖 ∈ 𝐼 (𝑆‘𝑖)) | 
| 49 | 46, 48 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → X𝑖 ∈ dom 𝑠(𝑠‘𝑖) = X𝑖 ∈ 𝐼 (𝑆‘𝑖)) | 
| 50 | 49 | rabeqdv 3451 | . . . . . . . . 9
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 }) | 
| 51 |  | dprdval.w | . . . . . . . . 9
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } | 
| 52 | 50, 51 | eqtr4di 2794 | . . . . . . . 8
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } = 𝑊) | 
| 53 |  | eqidd 2737 | . . . . . . . 8
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → (𝐺 Σg 𝑓) = (𝐺 Σg 𝑓)) | 
| 54 | 52, 53 | mpteq12dv 5232 | . . . . . . 7
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓)) = (𝑓 ∈ 𝑊 ↦ (𝐺 Σg 𝑓))) | 
| 55 | 54 | rneqd 5948 | . . . . . 6
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓)) = ran (𝑓 ∈ 𝑊 ↦ (𝐺 Σg 𝑓))) | 
| 56 | 42, 55 | eqeq12d 2752 | . . . . 5
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → ((𝐺 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓)) ↔ (𝐺 DProd 𝑆) = ran (𝑓 ∈ 𝑊 ↦ (𝐺 Σg 𝑓)))) | 
| 57 | 41, 56 | imbi12d 344 | . . . 4
⊢ (((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) ∧ 𝑠 = 𝑆) → ((𝐺dom DProd 𝑠 → (𝐺 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓))) ↔ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) = ran (𝑓 ∈ 𝑊 ↦ (𝐺 Σg 𝑓))))) | 
| 58 | 4, 57 | sbcied 3831 | . . 3
⊢ ((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) → ([𝑆 / 𝑠](𝐺dom DProd 𝑠 → (𝐺 DProd 𝑠) = ran (𝑓 ∈ {ℎ ∈ X𝑖 ∈ dom 𝑠(𝑠‘𝑖) ∣ ℎ finSupp 0 } ↦ (𝐺 Σg
𝑓))) ↔ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) = ran (𝑓 ∈ 𝑊 ↦ (𝐺 Σg 𝑓))))) | 
| 59 | 39, 58 | mpbid 232 | . 2
⊢ ((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) → (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) = ran (𝑓 ∈ 𝑊 ↦ (𝐺 Σg 𝑓)))) | 
| 60 | 1, 59 | mpd 15 | 1
⊢ ((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) → (𝐺 DProd 𝑆) = ran (𝑓 ∈ 𝑊 ↦ (𝐺 Σg 𝑓))) |