Step |
Hyp |
Ref |
Expression |
1 |
|
frmdup3.m |
⊢ 𝑀 = ( freeMnd ‘ 𝐼 ) |
2 |
|
frmdup3.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
3 |
|
frmdup3.u |
⊢ 𝑈 = ( varFMnd ‘ 𝐼 ) |
4 |
|
eqid |
⊢ ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) |
5 |
|
simp1 |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝐺 ∈ Mnd ) |
6 |
|
simp2 |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝐼 ∈ 𝑉 ) |
7 |
|
simp3 |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝐴 : 𝐼 ⟶ 𝐵 ) |
8 |
1 2 4 5 6 7
|
frmdup1 |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∈ ( 𝑀 MndHom 𝐺 ) ) |
9 |
5
|
adantr |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝐺 ∈ Mnd ) |
10 |
6
|
adantr |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ 𝑉 ) |
11 |
7
|
adantr |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝐴 : 𝐼 ⟶ 𝐵 ) |
12 |
|
simpr |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 ) |
13 |
1 2 4 9 10 11 3 12
|
frmdup2 |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) = ( 𝐴 ‘ 𝑦 ) ) |
14 |
13
|
mpteq2dva |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝐴 ‘ 𝑦 ) ) ) |
15 |
|
eqid |
⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) |
16 |
15 2
|
mhmf |
⊢ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∈ ( 𝑀 MndHom 𝐺 ) → ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) : ( Base ‘ 𝑀 ) ⟶ 𝐵 ) |
17 |
8 16
|
syl |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) : ( Base ‘ 𝑀 ) ⟶ 𝐵 ) |
18 |
3
|
vrmdf |
⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ Word 𝐼 ) |
19 |
18
|
3ad2ant2 |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝑈 : 𝐼 ⟶ Word 𝐼 ) |
20 |
1 15
|
frmdbas |
⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝑀 ) = Word 𝐼 ) |
21 |
20
|
3ad2ant2 |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( Base ‘ 𝑀 ) = Word 𝐼 ) |
22 |
21
|
feq3d |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( 𝑈 : 𝐼 ⟶ ( Base ‘ 𝑀 ) ↔ 𝑈 : 𝐼 ⟶ Word 𝐼 ) ) |
23 |
19 22
|
mpbird |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝑀 ) ) |
24 |
|
fcompt |
⊢ ( ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) : ( Base ‘ 𝑀 ) ⟶ 𝐵 ∧ 𝑈 : 𝐼 ⟶ ( Base ‘ 𝑀 ) ) → ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) ) ) |
25 |
17 23 24
|
syl2anc |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) ) ) |
26 |
7
|
feqmptd |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → 𝐴 = ( 𝑦 ∈ 𝐼 ↦ ( 𝐴 ‘ 𝑦 ) ) ) |
27 |
14 25 26
|
3eqtr4d |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) = 𝐴 ) |
28 |
1 2 3
|
frmdup3lem |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝑚 ∘ 𝑈 ) = 𝐴 ) ) → 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ) |
29 |
28
|
expr |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) ∧ 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ) → ( ( 𝑚 ∘ 𝑈 ) = 𝐴 → 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ) ) |
30 |
29
|
ralrimiva |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ∀ 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ( ( 𝑚 ∘ 𝑈 ) = 𝐴 → 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ) ) |
31 |
|
coeq1 |
⊢ ( 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) → ( 𝑚 ∘ 𝑈 ) = ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) ) |
32 |
31
|
eqeq1d |
⊢ ( 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) → ( ( 𝑚 ∘ 𝑈 ) = 𝐴 ↔ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) = 𝐴 ) ) |
33 |
32
|
eqreu |
⊢ ( ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ∘ 𝑈 ) = 𝐴 ∧ ∀ 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ( ( 𝑚 ∘ 𝑈 ) = 𝐴 → 𝑚 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴 ∘ 𝑥 ) ) ) ) ) → ∃! 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 ) |
34 |
8 27 30 33
|
syl3anc |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 : 𝐼 ⟶ 𝐵 ) → ∃! 𝑚 ∈ ( 𝑀 MndHom 𝐺 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 ) |