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 𝑓 ) ) )