Metamath Proof Explorer

Theorem dprdval

Description: The value of the internal direct product operation, which is a function mapping the (infinite, but finitely supported) cartesian product of subgroups (which mutually commute and have trivial intersections) to its (group) sum . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

Ref Expression
Hypotheses dprdval.0 ⊢ 0 = ( 0g ‘ 𝐺 )
dprdval.w ⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
Assertion dprdval ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 dprdval.0 ⊢ 0 = ( 0g ‘ 𝐺 )
2 dprdval.w ⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
3 simpl ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → 𝐺 dom DProd 𝑆 )
4 reldmdprd ⊢ Rel dom DProd
5 4 brrelex2i ⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 ∈ V )
6 5 adantr ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → 𝑆 ∈ V )
7 4 brrelex1i ⊢ ( 𝐺 dom DProd 𝑠 → 𝐺 ∈ V )
8 breq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 dom DProd 𝑠 ↔ 𝐺 dom DProd 𝑠 ) )
9 oveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 DProd 𝑠 ) = ( 𝐺 DProd 𝑠 ) )
10 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 0g ‘ 𝑔 ) = ( 0g ‘ 𝐺 ) )
11 10 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( 0g ‘ 𝑔 ) = 0 )
12 11 breq2d ⊢ ( 𝑔 = 𝐺 → ( ℎ finSupp ( 0g ‘ 𝑔 ) ↔ ℎ finSupp 0 ) )
13 12 rabbidv ⊢ ( 𝑔 = 𝐺 → { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } = { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } )
14 oveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 Σg 𝑓 ) = ( 𝐺 Σg 𝑓 ) )
15 13 14 mpteq12dv ⊢ ( 𝑔 = 𝐺 → ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) = ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) )
16 15 rneqd ⊢ ( 𝑔 = 𝐺 → ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) )
17 9 16 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ↔ ( 𝐺 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) ) )
18 8 17 imbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 dom DProd 𝑠 → ( 𝑔 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ) ↔ ( 𝐺 dom DProd 𝑠 → ( 𝐺 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) ) ) )
19 df-br ⊢ ( 𝑔 dom DProd 𝑠 ↔ ⟨ 𝑔 , 𝑠 ⟩ ∈ dom DProd )
20 fvex ⊢ ( 𝑠 ‘ 𝑖 ) ∈ V
21 20 rgenw ⊢ ∀ 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∈ V
22 ixpexg ⊢ ( ∀ 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∈ V → X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∈ V )
23 21 22 ax-mp ⊢ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∈ V
24 23 mptrabex ⊢ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ∈ V
25 24 rnex ⊢ ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ∈ V
26 25 rgen2w ⊢ ∀ 𝑔 ∈ Grp ∀ 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑖 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑖 } ) ( ℎ ‘ 𝑖 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑖 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑖 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ∈ V
27 df-dprd ⊢ DProd = ( 𝑔 ∈ Grp , 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑖 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑖 } ) ( ℎ ‘ 𝑖 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑖 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑖 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ↦ ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) )
28 27 fmpox ⊢ ( ∀ 𝑔 ∈ 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 )
29 26 28 mpbi ⊢ DProd : ∪ 𝑔 ∈ Grp ( { 𝑔 } × { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑖 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑖 } ) ( ℎ ‘ 𝑖 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑖 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑖 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ) ⟶ V
30 29 fdmi ⊢ dom DProd = ∪ 𝑔 ∈ Grp ( { 𝑔 } × { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑖 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑖 } ) ( ℎ ‘ 𝑖 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑖 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑖 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } )
31 30 eleq2i ⊢ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ dom DProd ↔ ⟨ 𝑔 , 𝑠 ⟩ ∈ ∪ 𝑔 ∈ Grp ( { 𝑔 } × { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑖 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑖 } ) ( ℎ ‘ 𝑖 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑖 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑖 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ) )
32 opeliunxp ⊢ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ ∪ 𝑔 ∈ Grp ( { 𝑔 } × { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑖 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑖 } ) ( ℎ ‘ 𝑖 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑖 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑖 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ) ↔ ( 𝑔 ∈ Grp ∧ 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑖 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑖 } ) ( ℎ ‘ 𝑖 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑖 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑖 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ) )
33 19 31 32 3bitri ⊢ ( 𝑔 dom DProd 𝑠 ↔ ( 𝑔 ∈ Grp ∧ 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑖 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑖 } ) ( ℎ ‘ 𝑖 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑖 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑖 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ) )
34 27 ovmpt4g ⊢ ( ( 𝑔 ∈ Grp ∧ 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑖 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑖 } ) ( ℎ ‘ 𝑖 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑖 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑖 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ∧ ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ∈ V ) → ( 𝑔 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) )
35 25 34 mp3an3 ⊢ ( ( 𝑔 ∈ Grp ∧ 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑖 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑖 } ) ( ℎ ‘ 𝑖 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑖 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑖 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ) → ( 𝑔 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) )
36 33 35 sylbi ⊢ ( 𝑔 dom DProd 𝑠 → ( 𝑔 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) )
37 18 36 vtoclg ⊢ ( 𝐺 ∈ V → ( 𝐺 dom DProd 𝑠 → ( 𝐺 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) ) )
38 7 37 mpcom ⊢ ( 𝐺 dom DProd 𝑠 → ( 𝐺 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) )
39 38 sbcth ⊢ ( 𝑆 ∈ V → [ 𝑆 / 𝑠 ] ( 𝐺 dom DProd 𝑠 → ( 𝐺 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) ) )
40 6 39 syl ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → [ 𝑆 / 𝑠 ] ( 𝐺 dom DProd 𝑠 → ( 𝐺 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) ) )
41 simpr ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
42 41 breq2d ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → ( 𝐺 dom DProd 𝑠 ↔ 𝐺 dom DProd 𝑆 ) )
43 41 oveq2d ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → ( 𝐺 DProd 𝑠 ) = ( 𝐺 DProd 𝑆 ) )
44 41 dmeqd ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → dom 𝑠 = dom 𝑆 )
45 simplr ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → dom 𝑆 = 𝐼 )
46 44 45 eqtrd ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → dom 𝑠 = 𝐼 )
47 46 ixpeq1d ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) = X 𝑖 ∈ 𝐼 ( 𝑠 ‘ 𝑖 ) )
48 41 fveq1d ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → ( 𝑠 ‘ 𝑖 ) = ( 𝑆 ‘ 𝑖 ) )
49 48 ixpeq2dv ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → X 𝑖 ∈ 𝐼 ( 𝑠 ‘ 𝑖 ) = X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) )
50 47 49 eqtrd ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) = X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) )
51 50 rabeqdv ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 } )
52 51 2 eqtr4di ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } = 𝑊 )
53 eqidd ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → ( 𝐺 Σg 𝑓 ) = ( 𝐺 Σg 𝑓 ) )
54 52 53 mpteq12dv ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) = ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) )
55 54 rneqd ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) = ran ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) )
56 43 55 eqeq12d ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → ( ( 𝐺 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) ↔ ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) ) )
57 42 56 imbi12d ⊢ ( ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑠 = 𝑆 ) → ( ( 𝐺 dom DProd 𝑠 → ( 𝐺 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) ) ↔ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) ) ) )
58 6 57 sbcied ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → ( [ 𝑆 / 𝑠 ] ( 𝐺 dom DProd 𝑠 → ( 𝐺 DProd 𝑠 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑠 ( 𝑠 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝐺 Σg 𝑓 ) ) ) ↔ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) ) ) )
59 40 58 mpbid ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) ) )
60 3 59 mpd ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ 𝑊 ↦ ( 𝐺 Σg 𝑓 ) ) )