Proof of Theorem frmdup3lem
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝑀) =
(Base‘𝑀) |
2 | | frmdup3.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
3 | 1, 2 | mhmf 18077 |
. . . . 5
⊢ (𝐹 ∈ (𝑀 MndHom 𝐺) → 𝐹:(Base‘𝑀)⟶𝐵) |
4 | 3 | ad2antrl 728 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹:(Base‘𝑀)⟶𝐵) |
5 | | frmdup3.m |
. . . . . . . 8
⊢ 𝑀 = (freeMnd‘𝐼) |
6 | 5, 1 | frmdbas 18133 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (Base‘𝑀) = Word 𝐼) |
7 | 6 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) → (Base‘𝑀) = Word 𝐼) |
8 | 7 | adantr 484 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → (Base‘𝑀) = Word 𝐼) |
9 | 8 | feq2d 6490 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → (𝐹:(Base‘𝑀)⟶𝐵 ↔ 𝐹:Word 𝐼⟶𝐵)) |
10 | 4, 9 | mpbid 235 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹:Word 𝐼⟶𝐵) |
11 | 10 | feqmptd 6737 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹 = (𝑥 ∈ Word 𝐼 ↦ (𝐹‘𝑥))) |
12 | | simplrl 777 |
. . . . 5
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → 𝐹 ∈ (𝑀 MndHom 𝐺)) |
13 | | simpr 488 |
. . . . . 6
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → 𝑥 ∈ Word 𝐼) |
14 | | frmdup3.u |
. . . . . . . . . 10
⊢ 𝑈 =
(varFMnd‘𝐼) |
15 | 14 | vrmdf 18139 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → 𝑈:𝐼⟶Word 𝐼) |
16 | 15 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) → 𝑈:𝐼⟶Word 𝐼) |
17 | 7 | feq3d 6491 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) → (𝑈:𝐼⟶(Base‘𝑀) ↔ 𝑈:𝐼⟶Word 𝐼)) |
18 | 16, 17 | mpbird 260 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) → 𝑈:𝐼⟶(Base‘𝑀)) |
19 | 18 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → 𝑈:𝐼⟶(Base‘𝑀)) |
20 | | wrdco 14282 |
. . . . . 6
⊢ ((𝑥 ∈ Word 𝐼 ∧ 𝑈:𝐼⟶(Base‘𝑀)) → (𝑈 ∘ 𝑥) ∈ Word (Base‘𝑀)) |
21 | 13, 19, 20 | syl2anc 587 |
. . . . 5
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → (𝑈 ∘ 𝑥) ∈ Word (Base‘𝑀)) |
22 | 1 | gsumwmhm 18126 |
. . . . 5
⊢ ((𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝑈 ∘ 𝑥) ∈ Word (Base‘𝑀)) → (𝐹‘(𝑀 Σg (𝑈 ∘ 𝑥))) = (𝐺 Σg (𝐹 ∘ (𝑈 ∘ 𝑥)))) |
23 | 12, 21, 22 | syl2anc 587 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → (𝐹‘(𝑀 Σg (𝑈 ∘ 𝑥))) = (𝐺 Σg (𝐹 ∘ (𝑈 ∘ 𝑥)))) |
24 | | simpll2 1214 |
. . . . . 6
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → 𝐼 ∈ 𝑉) |
25 | 5, 14 | frmdgsum 18143 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word 𝐼) → (𝑀 Σg (𝑈 ∘ 𝑥)) = 𝑥) |
26 | 24, 13, 25 | syl2anc 587 |
. . . . 5
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → (𝑀 Σg (𝑈 ∘ 𝑥)) = 𝑥) |
27 | 26 | fveq2d 6678 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → (𝐹‘(𝑀 Σg (𝑈 ∘ 𝑥))) = (𝐹‘𝑥)) |
28 | | coass 6098 |
. . . . . 6
⊢ ((𝐹 ∘ 𝑈) ∘ 𝑥) = (𝐹 ∘ (𝑈 ∘ 𝑥)) |
29 | | simplrr 778 |
. . . . . . 7
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → (𝐹 ∘ 𝑈) = 𝐴) |
30 | 29 | coeq1d 5704 |
. . . . . 6
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → ((𝐹 ∘ 𝑈) ∘ 𝑥) = (𝐴 ∘ 𝑥)) |
31 | 28, 30 | eqtr3id 2787 |
. . . . 5
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → (𝐹 ∘ (𝑈 ∘ 𝑥)) = (𝐴 ∘ 𝑥)) |
32 | 31 | oveq2d 7186 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → (𝐺 Σg (𝐹 ∘ (𝑈 ∘ 𝑥))) = (𝐺 Σg (𝐴 ∘ 𝑥))) |
33 | 23, 27, 32 | 3eqtr3d 2781 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) ∧ 𝑥 ∈ Word 𝐼) → (𝐹‘𝑥) = (𝐺 Σg (𝐴 ∘ 𝑥))) |
34 | 33 | mpteq2dva 5125 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → (𝑥 ∈ Word 𝐼 ↦ (𝐹‘𝑥)) = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))) |
35 | 11, 34 | eqtrd 2773 |
1
⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))) |