| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. 2
⊢ (𝐼 ∈ 𝑉 → (Base‘𝑀) = (Base‘𝑀)) |
| 2 | | eqidd 2738 |
. 2
⊢ (𝐼 ∈ 𝑉 → (+g‘𝑀) = (+g‘𝑀)) |
| 3 | | frmdmnd.m |
. . . . . 6
⊢ 𝑀 = (freeMnd‘𝐼) |
| 4 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑀) =
(Base‘𝑀) |
| 5 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 6 | 3, 4, 5 | frmdadd 18868 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝑥(+g‘𝑀)𝑦) = (𝑥 ++ 𝑦)) |
| 7 | 3, 4 | frmdelbas 18866 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝑀) → 𝑥 ∈ Word 𝐼) |
| 8 | 3, 4 | frmdelbas 18866 |
. . . . . 6
⊢ (𝑦 ∈ (Base‘𝑀) → 𝑦 ∈ Word 𝐼) |
| 9 | | ccatcl 14612 |
. . . . . 6
⊢ ((𝑥 ∈ Word 𝐼 ∧ 𝑦 ∈ Word 𝐼) → (𝑥 ++ 𝑦) ∈ Word 𝐼) |
| 10 | 7, 8, 9 | syl2an 596 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝑥 ++ 𝑦) ∈ Word 𝐼) |
| 11 | 6, 10 | eqeltrd 2841 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝑥(+g‘𝑀)𝑦) ∈ Word 𝐼) |
| 12 | 11 | 3adant1 1131 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝑥(+g‘𝑀)𝑦) ∈ Word 𝐼) |
| 13 | 3, 4 | frmdbas 18865 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → (Base‘𝑀) = Word 𝐼) |
| 14 | 13 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)) → (Base‘𝑀) = Word 𝐼) |
| 15 | 12, 14 | eleqtrrd 2844 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝑥(+g‘𝑀)𝑦) ∈ (Base‘𝑀)) |
| 16 | | simpr1 1195 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝑥 ∈ (Base‘𝑀)) |
| 17 | 16, 7 | syl 17 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝑥 ∈ Word 𝐼) |
| 18 | | simpr2 1196 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝑦 ∈ (Base‘𝑀)) |
| 19 | 18, 8 | syl 17 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝑦 ∈ Word 𝐼) |
| 20 | | simpr3 1197 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝑧 ∈ (Base‘𝑀)) |
| 21 | 3, 4 | frmdelbas 18866 |
. . . . . 6
⊢ (𝑧 ∈ (Base‘𝑀) → 𝑧 ∈ Word 𝐼) |
| 22 | 20, 21 | syl 17 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝑧 ∈ Word 𝐼) |
| 23 | | ccatass 14626 |
. . . . 5
⊢ ((𝑥 ∈ Word 𝐼 ∧ 𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼) → ((𝑥 ++ 𝑦) ++ 𝑧) = (𝑥 ++ (𝑦 ++ 𝑧))) |
| 24 | 17, 19, 22, 23 | syl3anc 1373 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → ((𝑥 ++ 𝑦) ++ 𝑧) = (𝑥 ++ (𝑦 ++ 𝑧))) |
| 25 | 16, 18, 10 | syl2anc 584 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑥 ++ 𝑦) ∈ Word 𝐼) |
| 26 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (Base‘𝑀) = Word 𝐼) |
| 27 | 25, 26 | eleqtrrd 2844 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑥 ++ 𝑦) ∈ (Base‘𝑀)) |
| 28 | 3, 4, 5 | frmdadd 18868 |
. . . . 5
⊢ (((𝑥 ++ 𝑦) ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀)) → ((𝑥 ++ 𝑦)(+g‘𝑀)𝑧) = ((𝑥 ++ 𝑦) ++ 𝑧)) |
| 29 | 27, 20, 28 | syl2anc 584 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → ((𝑥 ++ 𝑦)(+g‘𝑀)𝑧) = ((𝑥 ++ 𝑦) ++ 𝑧)) |
| 30 | | ccatcl 14612 |
. . . . . . 7
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼) → (𝑦 ++ 𝑧) ∈ Word 𝐼) |
| 31 | 19, 22, 30 | syl2anc 584 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑦 ++ 𝑧) ∈ Word 𝐼) |
| 32 | 31, 26 | eleqtrrd 2844 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑦 ++ 𝑧) ∈ (Base‘𝑀)) |
| 33 | 3, 4, 5 | frmdadd 18868 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑀) ∧ (𝑦 ++ 𝑧) ∈ (Base‘𝑀)) → (𝑥(+g‘𝑀)(𝑦 ++ 𝑧)) = (𝑥 ++ (𝑦 ++ 𝑧))) |
| 34 | 16, 32, 33 | syl2anc 584 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑥(+g‘𝑀)(𝑦 ++ 𝑧)) = (𝑥 ++ (𝑦 ++ 𝑧))) |
| 35 | 24, 29, 34 | 3eqtr4d 2787 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → ((𝑥 ++ 𝑦)(+g‘𝑀)𝑧) = (𝑥(+g‘𝑀)(𝑦 ++ 𝑧))) |
| 36 | 16, 18, 6 | syl2anc 584 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑥(+g‘𝑀)𝑦) = (𝑥 ++ 𝑦)) |
| 37 | 36 | oveq1d 7446 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → ((𝑥(+g‘𝑀)𝑦)(+g‘𝑀)𝑧) = ((𝑥 ++ 𝑦)(+g‘𝑀)𝑧)) |
| 38 | 3, 4, 5 | frmdadd 18868 |
. . . . 5
⊢ ((𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀)) → (𝑦(+g‘𝑀)𝑧) = (𝑦 ++ 𝑧)) |
| 39 | 18, 20, 38 | syl2anc 584 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑦(+g‘𝑀)𝑧) = (𝑦 ++ 𝑧)) |
| 40 | 39 | oveq2d 7447 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑥(+g‘𝑀)(𝑦(+g‘𝑀)𝑧)) = (𝑥(+g‘𝑀)(𝑦 ++ 𝑧))) |
| 41 | 35, 37, 40 | 3eqtr4d 2787 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → ((𝑥(+g‘𝑀)𝑦)(+g‘𝑀)𝑧) = (𝑥(+g‘𝑀)(𝑦(+g‘𝑀)𝑧))) |
| 42 | | wrd0 14577 |
. . 3
⊢ ∅
∈ Word 𝐼 |
| 43 | 42, 13 | eleqtrrid 2848 |
. 2
⊢ (𝐼 ∈ 𝑉 → ∅ ∈ (Base‘𝑀)) |
| 44 | 3, 4, 5 | frmdadd 18868 |
. . . 4
⊢ ((∅
∈ (Base‘𝑀) ∧
𝑥 ∈ (Base‘𝑀)) →
(∅(+g‘𝑀)𝑥) = (∅ ++ 𝑥)) |
| 45 | 43, 44 | sylan 580 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑀)) → (∅(+g‘𝑀)𝑥) = (∅ ++ 𝑥)) |
| 46 | 7 | adantl 481 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑀)) → 𝑥 ∈ Word 𝐼) |
| 47 | | ccatlid 14624 |
. . . 4
⊢ (𝑥 ∈ Word 𝐼 → (∅ ++ 𝑥) = 𝑥) |
| 48 | 46, 47 | syl 17 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑀)) → (∅ ++ 𝑥) = 𝑥) |
| 49 | 45, 48 | eqtrd 2777 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑀)) → (∅(+g‘𝑀)𝑥) = 𝑥) |
| 50 | 3, 4, 5 | frmdadd 18868 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑀) ∧ ∅ ∈
(Base‘𝑀)) →
(𝑥(+g‘𝑀)∅) = (𝑥 ++ ∅)) |
| 51 | 50 | ancoms 458 |
. . . 4
⊢ ((∅
∈ (Base‘𝑀) ∧
𝑥 ∈ (Base‘𝑀)) → (𝑥(+g‘𝑀)∅) = (𝑥 ++ ∅)) |
| 52 | 43, 51 | sylan 580 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑀)) → (𝑥(+g‘𝑀)∅) = (𝑥 ++ ∅)) |
| 53 | | ccatrid 14625 |
. . . 4
⊢ (𝑥 ∈ Word 𝐼 → (𝑥 ++ ∅) = 𝑥) |
| 54 | 46, 53 | syl 17 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑀)) → (𝑥 ++ ∅) = 𝑥) |
| 55 | 52, 54 | eqtrd 2777 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑀)) → (𝑥(+g‘𝑀)∅) = 𝑥) |
| 56 | 1, 2, 15, 41, 43, 49, 55 | ismndd 18769 |
1
⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd) |