Step |
Hyp |
Ref |
Expression |
1 |
|
eldprdi.0 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
2 |
|
eldprdi.w |
⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 } |
3 |
|
eldprdi.1 |
⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 ) |
4 |
|
eldprdi.2 |
⊢ ( 𝜑 → dom 𝑆 = 𝐼 ) |
5 |
|
eldprdi.3 |
⊢ ( 𝜑 → 𝐹 ∈ 𝑊 ) |
6 |
|
eqid |
⊢ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) |
7 |
|
oveq2 |
⊢ ( 𝑓 = 𝐹 → ( 𝐺 Σg 𝑓 ) = ( 𝐺 Σg 𝐹 ) ) |
8 |
7
|
rspceeqv |
⊢ ( ( 𝐹 ∈ 𝑊 ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) ) → ∃ 𝑓 ∈ 𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) |
9 |
5 6 8
|
sylancl |
⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) |
10 |
1 2
|
eldprd |
⊢ ( dom 𝑆 = 𝐼 → ( ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ 𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ) |
11 |
4 10
|
syl |
⊢ ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ 𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) ) |
12 |
3 9 11
|
mpbir2and |
⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) ) |