| Step | Hyp | Ref
| Expression |
| 1 | | gsumwun.w |
. 2
⊢ (𝜑 → 𝑊 ∈ Word (𝐸 ∪ 𝐹)) |
| 2 | | oveq2 7439 |
. . . . . 6
⊢ (𝑣 = ∅ → (𝑀 Σg
𝑣) = (𝑀 Σg
∅)) |
| 3 | 2 | eqeq1d 2739 |
. . . . 5
⊢ (𝑣 = ∅ → ((𝑀 Σg
𝑣) = (𝑒 + 𝑓) ↔ (𝑀 Σg ∅) =
(𝑒 + 𝑓))) |
| 4 | 3 | 2rexbidv 3222 |
. . . 4
⊢ (𝑣 = ∅ → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg ∅) =
(𝑒 + 𝑓))) |
| 5 | 4 | imbi2d 340 |
. . 3
⊢ (𝑣 = ∅ → ((𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓)) ↔ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg ∅) =
(𝑒 + 𝑓)))) |
| 6 | | oveq2 7439 |
. . . . . 6
⊢ (𝑣 = 𝑤 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑤)) |
| 7 | 6 | eqeq1d 2739 |
. . . . 5
⊢ (𝑣 = 𝑤 → ((𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ (𝑀 Σg 𝑤) = (𝑒 + 𝑓))) |
| 8 | 7 | 2rexbidv 3222 |
. . . 4
⊢ (𝑣 = 𝑤 → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑤) = (𝑒 + 𝑓))) |
| 9 | 8 | imbi2d 340 |
. . 3
⊢ (𝑣 = 𝑤 → ((𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓)) ↔ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑤) = (𝑒 + 𝑓)))) |
| 10 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑒 = 𝑖 → (𝑒 + 𝑓) = (𝑖 + 𝑓)) |
| 11 | 10 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑒 = 𝑖 → ((𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ (𝑀 Σg 𝑣) = (𝑖 + 𝑓))) |
| 12 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑓 = 𝑗 → (𝑖 + 𝑓) = (𝑖 + 𝑗)) |
| 13 | 12 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑓 = 𝑗 → ((𝑀 Σg 𝑣) = (𝑖 + 𝑓) ↔ (𝑀 Σg 𝑣) = (𝑖 + 𝑗))) |
| 14 | 11, 13 | cbvrex2vw 3242 |
. . . . 5
⊢
(∃𝑒 ∈
𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑖 + 𝑗)) |
| 15 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑣 = (𝑤 ++ 〈“𝑥”〉) → (𝑀 Σg 𝑣) = (𝑀 Σg (𝑤 ++ 〈“𝑥”〉))) |
| 16 | 15 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑣 = (𝑤 ++ 〈“𝑥”〉) → ((𝑀 Σg 𝑣) = (𝑖 + 𝑗) ↔ (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗))) |
| 17 | 16 | 2rexbidv 3222 |
. . . . 5
⊢ (𝑣 = (𝑤 ++ 〈“𝑥”〉) → (∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑖 + 𝑗) ↔ ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗))) |
| 18 | 14, 17 | bitrid 283 |
. . . 4
⊢ (𝑣 = (𝑤 ++ 〈“𝑥”〉) → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗))) |
| 19 | 18 | imbi2d 340 |
. . 3
⊢ (𝑣 = (𝑤 ++ 〈“𝑥”〉) → ((𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓)) ↔ (𝜑 → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)))) |
| 20 | | oveq2 7439 |
. . . . . 6
⊢ (𝑣 = 𝑊 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑊)) |
| 21 | 20 | eqeq1d 2739 |
. . . . 5
⊢ (𝑣 = 𝑊 → ((𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ (𝑀 Σg 𝑊) = (𝑒 + 𝑓))) |
| 22 | 21 | 2rexbidv 3222 |
. . . 4
⊢ (𝑣 = 𝑊 → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑊) = (𝑒 + 𝑓))) |
| 23 | 22 | imbi2d 340 |
. . 3
⊢ (𝑣 = 𝑊 → ((𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓)) ↔ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑊) = (𝑒 + 𝑓)))) |
| 24 | | oveq1 7438 |
. . . . 5
⊢ (𝑒 = (0g‘𝑀) → (𝑒 + 𝑓) = ((0g‘𝑀) + 𝑓)) |
| 25 | 24 | eqeq2d 2748 |
. . . 4
⊢ (𝑒 = (0g‘𝑀) → ((𝑀 Σg ∅) =
(𝑒 + 𝑓) ↔ (𝑀 Σg ∅) =
((0g‘𝑀)
+ 𝑓))) |
| 26 | | oveq2 7439 |
. . . . 5
⊢ (𝑓 = (0g‘𝑀) →
((0g‘𝑀)
+ 𝑓) = ((0g‘𝑀) + (0g‘𝑀))) |
| 27 | 26 | eqeq2d 2748 |
. . . 4
⊢ (𝑓 = (0g‘𝑀) → ((𝑀 Σg ∅) =
((0g‘𝑀)
+ 𝑓) ↔ (𝑀 Σg ∅) =
((0g‘𝑀)
+
(0g‘𝑀)))) |
| 28 | | gsumwun.e |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (SubMnd‘𝑀)) |
| 29 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 30 | 29 | subm0cl 18824 |
. . . . 5
⊢ (𝐸 ∈ (SubMnd‘𝑀) →
(0g‘𝑀)
∈ 𝐸) |
| 31 | 28, 30 | syl 17 |
. . . 4
⊢ (𝜑 → (0g‘𝑀) ∈ 𝐸) |
| 32 | | gsumwun.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (SubMnd‘𝑀)) |
| 33 | 29 | subm0cl 18824 |
. . . . 5
⊢ (𝐹 ∈ (SubMnd‘𝑀) →
(0g‘𝑀)
∈ 𝐹) |
| 34 | 32, 33 | syl 17 |
. . . 4
⊢ (𝜑 → (0g‘𝑀) ∈ 𝐹) |
| 35 | 29 | gsum0 18697 |
. . . . 5
⊢ (𝑀 Σg
∅) = (0g‘𝑀) |
| 36 | | gsumwun.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ CMnd) |
| 37 | 36 | cmnmndd 19822 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ Mnd) |
| 38 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑀) =
(Base‘𝑀) |
| 39 | 38, 29 | mndidcl 18762 |
. . . . . 6
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ (Base‘𝑀)) |
| 40 | | gsumwun.p |
. . . . . . 7
⊢ + =
(+g‘𝑀) |
| 41 | 38, 40, 29 | mndlid 18767 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧
(0g‘𝑀)
∈ (Base‘𝑀))
→ ((0g‘𝑀) + (0g‘𝑀)) = (0g‘𝑀)) |
| 42 | 37, 39, 41 | syl2anc2 585 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑀)
+
(0g‘𝑀)) =
(0g‘𝑀)) |
| 43 | 35, 42 | eqtr4id 2796 |
. . . 4
⊢ (𝜑 → (𝑀 Σg ∅) =
((0g‘𝑀)
+
(0g‘𝑀))) |
| 44 | 25, 27, 31, 34, 43 | 2rspcedvdw 3636 |
. . 3
⊢ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg ∅) =
(𝑒 + 𝑓)) |
| 45 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑒 + 𝑥) → (𝑖 + 𝑗) = ((𝑒 + 𝑥) + 𝑗)) |
| 46 | 45 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑒 + 𝑥) → ((𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗) ↔ (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑒 + 𝑥) + 𝑗))) |
| 47 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑓 → ((𝑒 + 𝑥) + 𝑗) = ((𝑒 + 𝑥) + 𝑓)) |
| 48 | 47 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑓 → ((𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑒 + 𝑥) + 𝑗) ↔ (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑒 + 𝑥) + 𝑓))) |
| 49 | 28 | ad6antr 736 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → 𝐸 ∈ (SubMnd‘𝑀)) |
| 50 | | simp-4r 784 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → 𝑒 ∈ 𝐸) |
| 51 | | simpr 484 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → 𝑥 ∈ 𝐸) |
| 52 | 40, 49, 50, 51 | submcld 33040 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → (𝑒 + 𝑥) ∈ 𝐸) |
| 53 | | simpllr 776 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → 𝑓 ∈ 𝐹) |
| 54 | 37 | ad5antr 734 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑀 ∈ Mnd) |
| 55 | 38 | submss 18822 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸 ∈ (SubMnd‘𝑀) → 𝐸 ⊆ (Base‘𝑀)) |
| 56 | 28, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐸 ⊆ (Base‘𝑀)) |
| 57 | 38 | submss 18822 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (SubMnd‘𝑀) → 𝐹 ⊆ (Base‘𝑀)) |
| 58 | 32, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ⊆ (Base‘𝑀)) |
| 59 | 56, 58 | unssd 4192 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 ∪ 𝐹) ⊆ (Base‘𝑀)) |
| 60 | | sswrd 14560 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸 ∪ 𝐹) ⊆ (Base‘𝑀) → Word (𝐸 ∪ 𝐹) ⊆ Word (Base‘𝑀)) |
| 61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ⊆ Word (Base‘𝑀)) |
| 62 | 61 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑤 ∈ Word (Base‘𝑀)) |
| 63 | 62 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑤 ∈ Word (Base‘𝑀)) |
| 64 | 59 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → (𝐸 ∪ 𝐹) ⊆ (Base‘𝑀)) |
| 65 | 64 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) → 𝑥 ∈ (Base‘𝑀)) |
| 66 | 65 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑥 ∈ (Base‘𝑀)) |
| 67 | 38, 40 | gsumccatsn 18856 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word (Base‘𝑀) ∧ 𝑥 ∈ (Base‘𝑀)) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑀 Σg
𝑤) + 𝑥)) |
| 68 | 54, 63, 66, 67 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑀 Σg
𝑤) + 𝑥)) |
| 69 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) |
| 70 | 69 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → ((𝑀 Σg 𝑤) + 𝑥) = ((𝑒 + 𝑓) + 𝑥)) |
| 71 | 56 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) → 𝐸 ⊆ (Base‘𝑀)) |
| 72 | 71 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) → 𝑒 ∈ (Base‘𝑀)) |
| 73 | 72 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑒 ∈ (Base‘𝑀)) |
| 74 | 58 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) → 𝐹 ⊆ (Base‘𝑀)) |
| 75 | 74 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) → 𝑓 ∈ (Base‘𝑀)) |
| 76 | 75 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑓 ∈ (Base‘𝑀)) |
| 77 | 36 | ad5antr 734 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑀 ∈ CMnd) |
| 78 | 38, 40 | cmncom 19816 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ CMnd ∧ 𝑓 ∈ (Base‘𝑀) ∧ 𝑥 ∈ (Base‘𝑀)) → (𝑓 + 𝑥) = (𝑥 + 𝑓)) |
| 79 | 77, 76, 66, 78 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑓 + 𝑥) = (𝑥 + 𝑓)) |
| 80 | 38, 40, 54, 73, 76, 66, 79 | mnd32g 18759 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → ((𝑒 + 𝑓) + 𝑥) = ((𝑒 + 𝑥) + 𝑓)) |
| 81 | 68, 70, 80 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑒 + 𝑥) + 𝑓)) |
| 82 | 81 | adantr 480 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑒 + 𝑥) + 𝑓)) |
| 83 | 46, 48, 52, 53, 82 | 2rspcedvdw 3636 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)) |
| 84 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑒 → (𝑖 + 𝑗) = (𝑒 + 𝑗)) |
| 85 | 84 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑒 → ((𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗) ↔ (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑒 + 𝑗))) |
| 86 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑓 + 𝑥) → (𝑒 + 𝑗) = (𝑒 + (𝑓 + 𝑥))) |
| 87 | 86 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑓 + 𝑥) → ((𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑒 + 𝑗) ↔ (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑒 + (𝑓 + 𝑥)))) |
| 88 | | simp-4r 784 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐹) → 𝑒 ∈ 𝐸) |
| 89 | 32 | ad6antr 736 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐹) → 𝐹 ∈ (SubMnd‘𝑀)) |
| 90 | | simpllr 776 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐹) → 𝑓 ∈ 𝐹) |
| 91 | | simpr 484 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ 𝐹) |
| 92 | 40, 89, 90, 91 | submcld 33040 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐹) → (𝑓 + 𝑥) ∈ 𝐹) |
| 93 | 38, 40, 54, 73, 76, 66 | mndassd 33028 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → ((𝑒 + 𝑓) + 𝑥) = (𝑒 + (𝑓 + 𝑥))) |
| 94 | 68, 70, 93 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑒 + (𝑓 + 𝑥))) |
| 95 | 94 | adantr 480 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐹) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑒 + (𝑓 + 𝑥))) |
| 96 | 85, 87, 88, 92, 95 | 2rspcedvdw 3636 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐹) → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)) |
| 97 | | elun 4153 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐸 ∪ 𝐹) ↔ (𝑥 ∈ 𝐸 ∨ 𝑥 ∈ 𝐹)) |
| 98 | 97 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐸 ∪ 𝐹) → (𝑥 ∈ 𝐸 ∨ 𝑥 ∈ 𝐹)) |
| 99 | 98 | ad4antlr 733 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑥 ∈ 𝐸 ∨ 𝑥 ∈ 𝐹)) |
| 100 | 83, 96, 99 | mpjaodan 961 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)) |
| 101 | 100 | r19.29ffa 32490 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)) |
| 102 | 101 | ex 412 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑤) = (𝑒 + 𝑓) → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗))) |
| 103 | 102 | expl 457 |
. . . . 5
⊢ (𝜑 → ((𝑤 ∈ Word (𝐸 ∪ 𝐹) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑤) = (𝑒 + 𝑓) → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)))) |
| 104 | 103 | com12 32 |
. . . 4
⊢ ((𝑤 ∈ Word (𝐸 ∪ 𝐹) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) → (𝜑 → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑤) = (𝑒 + 𝑓) → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)))) |
| 105 | 104 | a2d 29 |
. . 3
⊢ ((𝑤 ∈ Word (𝐸 ∪ 𝐹) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) → ((𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝜑 → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)))) |
| 106 | 5, 9, 19, 23, 44, 105 | wrdind 14760 |
. 2
⊢ (𝑊 ∈ Word (𝐸 ∪ 𝐹) → (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑊) = (𝑒 + 𝑓))) |
| 107 | 1, 106 | mpcom 38 |
1
⊢ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑊) = (𝑒 + 𝑓)) |