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