Step |
Hyp |
Ref |
Expression |
1 |
|
frmdup.m |
⊢ 𝑀 = ( freeMnd ‘ 𝐼 ) |
2 |
|
frmdup.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
3 |
|
frmdup.e |
⊢ 𝐸 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) |
4 |
|
frmdup.g |
⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
5 |
|
frmdup.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑋 ) |
6 |
|
frmdup.a |
⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐵 ) |
7 |
|
frmdup2.u |
⊢ 𝑈 = ( varFMnd ‘ 𝐼 ) |
8 |
|
frmdup2.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐼 ) |
9 |
7
|
vrmdval |
⊢ ( ( 𝐼 ∈ 𝑋 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑌 ) = 〈“ 𝑌 ”〉 ) |
10 |
5 8 9
|
syl2anc |
⊢ ( 𝜑 → ( 𝑈 ‘ 𝑌 ) = 〈“ 𝑌 ”〉 ) |
11 |
10
|
fveq2d |
⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝑌 ) ) = ( 𝐸 ‘ 〈“ 𝑌 ”〉 ) ) |
12 |
8
|
s1cld |
⊢ ( 𝜑 → 〈“ 𝑌 ”〉 ∈ Word 𝐼 ) |
13 |
|
coeq2 |
⊢ ( 𝑥 = 〈“ 𝑌 ”〉 → ( 𝐴 ∘ 𝑥 ) = ( 𝐴 ∘ 〈“ 𝑌 ”〉 ) ) |
14 |
13
|
oveq2d |
⊢ ( 𝑥 = 〈“ 𝑌 ”〉 → ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) = ( 𝐺 Σg ( 𝐴 ∘ 〈“ 𝑌 ”〉 ) ) ) |
15 |
|
ovex |
⊢ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ∈ V |
16 |
14 3 15
|
fvmpt3i |
⊢ ( 〈“ 𝑌 ”〉 ∈ Word 𝐼 → ( 𝐸 ‘ 〈“ 𝑌 ”〉 ) = ( 𝐺 Σg ( 𝐴 ∘ 〈“ 𝑌 ”〉 ) ) ) |
17 |
12 16
|
syl |
⊢ ( 𝜑 → ( 𝐸 ‘ 〈“ 𝑌 ”〉 ) = ( 𝐺 Σg ( 𝐴 ∘ 〈“ 𝑌 ”〉 ) ) ) |
18 |
|
s1co |
⊢ ( ( 𝑌 ∈ 𝐼 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝐴 ∘ 〈“ 𝑌 ”〉 ) = 〈“ ( 𝐴 ‘ 𝑌 ) ”〉 ) |
19 |
8 6 18
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 ∘ 〈“ 𝑌 ”〉 ) = 〈“ ( 𝐴 ‘ 𝑌 ) ”〉 ) |
20 |
19
|
oveq2d |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐴 ∘ 〈“ 𝑌 ”〉 ) ) = ( 𝐺 Σg 〈“ ( 𝐴 ‘ 𝑌 ) ”〉 ) ) |
21 |
6 8
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝐴 ‘ 𝑌 ) ∈ 𝐵 ) |
22 |
2
|
gsumws1 |
⊢ ( ( 𝐴 ‘ 𝑌 ) ∈ 𝐵 → ( 𝐺 Σg 〈“ ( 𝐴 ‘ 𝑌 ) ”〉 ) = ( 𝐴 ‘ 𝑌 ) ) |
23 |
21 22
|
syl |
⊢ ( 𝜑 → ( 𝐺 Σg 〈“ ( 𝐴 ‘ 𝑌 ) ”〉 ) = ( 𝐴 ‘ 𝑌 ) ) |
24 |
17 20 23
|
3eqtrd |
⊢ ( 𝜑 → ( 𝐸 ‘ 〈“ 𝑌 ”〉 ) = ( 𝐴 ‘ 𝑌 ) ) |
25 |
11 24
|
eqtrd |
⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝑌 ) ) = ( 𝐴 ‘ 𝑌 ) ) |