Step | Hyp | Ref
| Expression |
1 | | gsumwun.w |
. 2
⊢ (𝜑 → 𝑊 ∈ Word (𝐸 ∪ 𝐹)) |
2 | | oveq2 7438 |
. . . . . 6
⊢ (𝑣 = ∅ → (𝑀 Σg
𝑣) = (𝑀 Σg
∅)) |
3 | 2 | eqeq1d 2736 |
. . . . 5
⊢ (𝑣 = ∅ → ((𝑀 Σg
𝑣) = (𝑒 + 𝑓) ↔ (𝑀 Σg ∅) =
(𝑒 + 𝑓))) |
4 | 3 | 2rexbidv 3219 |
. . . 4
⊢ (𝑣 = ∅ → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg ∅) =
(𝑒 + 𝑓))) |
5 | 4 | imbi2d 340 |
. . 3
⊢ (𝑣 = ∅ → ((𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓)) ↔ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg ∅) =
(𝑒 + 𝑓)))) |
6 | | oveq2 7438 |
. . . . . 6
⊢ (𝑣 = 𝑤 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑤)) |
7 | 6 | eqeq1d 2736 |
. . . . 5
⊢ (𝑣 = 𝑤 → ((𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ (𝑀 Σg 𝑤) = (𝑒 + 𝑓))) |
8 | 7 | 2rexbidv 3219 |
. . . 4
⊢ (𝑣 = 𝑤 → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑤) = (𝑒 + 𝑓))) |
9 | 8 | imbi2d 340 |
. . 3
⊢ (𝑣 = 𝑤 → ((𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓)) ↔ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑤) = (𝑒 + 𝑓)))) |
10 | | oveq1 7437 |
. . . . . . 7
⊢ (𝑒 = 𝑖 → (𝑒 + 𝑓) = (𝑖 + 𝑓)) |
11 | 10 | eqeq2d 2745 |
. . . . . 6
⊢ (𝑒 = 𝑖 → ((𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ (𝑀 Σg 𝑣) = (𝑖 + 𝑓))) |
12 | | oveq2 7438 |
. . . . . . 7
⊢ (𝑓 = 𝑗 → (𝑖 + 𝑓) = (𝑖 + 𝑗)) |
13 | 12 | eqeq2d 2745 |
. . . . . 6
⊢ (𝑓 = 𝑗 → ((𝑀 Σg 𝑣) = (𝑖 + 𝑓) ↔ (𝑀 Σg 𝑣) = (𝑖 + 𝑗))) |
14 | 11, 13 | cbvrex2vw 3239 |
. . . . 5
⊢
(∃𝑒 ∈
𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑖 + 𝑗)) |
15 | | oveq2 7438 |
. . . . . . 7
⊢ (𝑣 = (𝑤 ++ 〈“𝑥”〉) → (𝑀 Σg 𝑣) = (𝑀 Σg (𝑤 ++ 〈“𝑥”〉))) |
16 | 15 | eqeq1d 2736 |
. . . . . 6
⊢ (𝑣 = (𝑤 ++ 〈“𝑥”〉) → ((𝑀 Σg 𝑣) = (𝑖 + 𝑗) ↔ (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗))) |
17 | 16 | 2rexbidv 3219 |
. . . . 5
⊢ (𝑣 = (𝑤 ++ 〈“𝑥”〉) → (∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑖 + 𝑗) ↔ ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗))) |
18 | 14, 17 | bitrid 283 |
. . . 4
⊢ (𝑣 = (𝑤 ++ 〈“𝑥”〉) → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗))) |
19 | 18 | imbi2d 340 |
. . 3
⊢ (𝑣 = (𝑤 ++ 〈“𝑥”〉) → ((𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓)) ↔ (𝜑 → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)))) |
20 | | oveq2 7438 |
. . . . . 6
⊢ (𝑣 = 𝑊 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑊)) |
21 | 20 | eqeq1d 2736 |
. . . . 5
⊢ (𝑣 = 𝑊 → ((𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ (𝑀 Σg 𝑊) = (𝑒 + 𝑓))) |
22 | 21 | 2rexbidv 3219 |
. . . 4
⊢ (𝑣 = 𝑊 → (∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓) ↔ ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑊) = (𝑒 + 𝑓))) |
23 | 22 | imbi2d 340 |
. . 3
⊢ (𝑣 = 𝑊 → ((𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑣) = (𝑒 + 𝑓)) ↔ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑊) = (𝑒 + 𝑓)))) |
24 | | oveq1 7437 |
. . . . 5
⊢ (𝑒 = (0g‘𝑀) → (𝑒 + 𝑓) = ((0g‘𝑀) + 𝑓)) |
25 | 24 | eqeq2d 2745 |
. . . 4
⊢ (𝑒 = (0g‘𝑀) → ((𝑀 Σg ∅) =
(𝑒 + 𝑓) ↔ (𝑀 Σg ∅) =
((0g‘𝑀)
+ 𝑓))) |
26 | | oveq2 7438 |
. . . . 5
⊢ (𝑓 = (0g‘𝑀) →
((0g‘𝑀)
+ 𝑓) = ((0g‘𝑀) + (0g‘𝑀))) |
27 | 26 | eqeq2d 2745 |
. . . 4
⊢ (𝑓 = (0g‘𝑀) → ((𝑀 Σg ∅) =
((0g‘𝑀)
+ 𝑓) ↔ (𝑀 Σg ∅) =
((0g‘𝑀)
+
(0g‘𝑀)))) |
28 | | gsumwun.e |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (SubMnd‘𝑀)) |
29 | | eqid 2734 |
. . . . . 6
⊢
(0g‘𝑀) = (0g‘𝑀) |
30 | 29 | subm0cl 18836 |
. . . . 5
⊢ (𝐸 ∈ (SubMnd‘𝑀) →
(0g‘𝑀)
∈ 𝐸) |
31 | 28, 30 | syl 17 |
. . . 4
⊢ (𝜑 → (0g‘𝑀) ∈ 𝐸) |
32 | | gsumwun.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (SubMnd‘𝑀)) |
33 | 29 | subm0cl 18836 |
. . . . 5
⊢ (𝐹 ∈ (SubMnd‘𝑀) →
(0g‘𝑀)
∈ 𝐹) |
34 | 32, 33 | syl 17 |
. . . 4
⊢ (𝜑 → (0g‘𝑀) ∈ 𝐹) |
35 | 29 | gsum0 18709 |
. . . . 5
⊢ (𝑀 Σg
∅) = (0g‘𝑀) |
36 | | gsumwun.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ CMnd) |
37 | 36 | cmnmndd 19836 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ Mnd) |
38 | | eqid 2734 |
. . . . . . 7
⊢
(Base‘𝑀) =
(Base‘𝑀) |
39 | 38, 29 | mndidcl 18774 |
. . . . . 6
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ (Base‘𝑀)) |
40 | | gsumwun.p |
. . . . . . 7
⊢ + =
(+g‘𝑀) |
41 | 38, 40, 29 | mndlid 18779 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧
(0g‘𝑀)
∈ (Base‘𝑀))
→ ((0g‘𝑀) + (0g‘𝑀)) = (0g‘𝑀)) |
42 | 37, 39, 41 | syl2anc2 585 |
. . . . 5
⊢ (𝜑 →
((0g‘𝑀)
+
(0g‘𝑀)) =
(0g‘𝑀)) |
43 | 35, 42 | eqtr4id 2793 |
. . . 4
⊢ (𝜑 → (𝑀 Σg ∅) =
((0g‘𝑀)
+
(0g‘𝑀))) |
44 | 25, 27, 31, 34, 43 | 2rspcedvdw 3635 |
. . 3
⊢ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg ∅) =
(𝑒 + 𝑓)) |
45 | | oveq1 7437 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑒 + 𝑥) → (𝑖 + 𝑗) = ((𝑒 + 𝑥) + 𝑗)) |
46 | 45 | eqeq2d 2745 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑒 + 𝑥) → ((𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗) ↔ (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑒 + 𝑥) + 𝑗))) |
47 | | oveq2 7438 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑓 → ((𝑒 + 𝑥) + 𝑗) = ((𝑒 + 𝑥) + 𝑓)) |
48 | 47 | eqeq2d 2745 |
. . . . . . . . . 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 33022 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → (𝑒 + 𝑥) ∈ 𝐸) |
53 | | simpllr 776 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → 𝑓 ∈ 𝐹) |
54 | 37 | ad5antr 734 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑀 ∈ Mnd) |
55 | 38 | submss 18834 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸 ∈ (SubMnd‘𝑀) → 𝐸 ⊆ (Base‘𝑀)) |
56 | 28, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐸 ⊆ (Base‘𝑀)) |
57 | 38 | submss 18834 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (SubMnd‘𝑀) → 𝐹 ⊆ (Base‘𝑀)) |
58 | 32, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ⊆ (Base‘𝑀)) |
59 | 56, 58 | unssd 4201 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 ∪ 𝐹) ⊆ (Base‘𝑀)) |
60 | | sswrd 14556 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸 ∪ 𝐹) ⊆ (Base‘𝑀) → Word (𝐸 ∪ 𝐹) ⊆ Word (Base‘𝑀)) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Word (𝐸 ∪ 𝐹) ⊆ Word (Base‘𝑀)) |
62 | 61 | sselda 3994 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → 𝑤 ∈ Word (Base‘𝑀)) |
63 | 62 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑤 ∈ Word (Base‘𝑀)) |
64 | 59 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) → (𝐸 ∪ 𝐹) ⊆ (Base‘𝑀)) |
65 | 64 | sselda 3994 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) → 𝑥 ∈ (Base‘𝑀)) |
66 | 65 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑥 ∈ (Base‘𝑀)) |
67 | 38, 40 | gsumccatsn 18868 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word (Base‘𝑀) ∧ 𝑥 ∈ (Base‘𝑀)) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑀 Σg
𝑤) + 𝑥)) |
68 | 54, 63, 66, 67 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑀 Σg
𝑤) + 𝑥)) |
69 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) |
70 | 69 | oveq1d 7445 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → ((𝑀 Σg 𝑤) + 𝑥) = ((𝑒 + 𝑓) + 𝑥)) |
71 | 56 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) → 𝐸 ⊆ (Base‘𝑀)) |
72 | 71 | sselda 3994 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) → 𝑒 ∈ (Base‘𝑀)) |
73 | 72 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑒 ∈ (Base‘𝑀)) |
74 | 58 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) → 𝐹 ⊆ (Base‘𝑀)) |
75 | 74 | sselda 3994 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) → 𝑓 ∈ (Base‘𝑀)) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑓 ∈ (Base‘𝑀)) |
77 | 36 | ad5antr 734 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → 𝑀 ∈ CMnd) |
78 | 38, 40 | cmncom 19830 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ CMnd ∧ 𝑓 ∈ (Base‘𝑀) ∧ 𝑥 ∈ (Base‘𝑀)) → (𝑓 + 𝑥) = (𝑥 + 𝑓)) |
79 | 77, 76, 66, 78 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑓 + 𝑥) = (𝑥 + 𝑓)) |
80 | 38, 40, 54, 73, 76, 66, 79 | mnd32g 18771 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → ((𝑒 + 𝑓) + 𝑥) = ((𝑒 + 𝑥) + 𝑓)) |
81 | 68, 70, 80 | 3eqtrd 2778 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑒 + 𝑥) + 𝑓)) |
82 | 81 | adantr 480 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = ((𝑒 + 𝑥) + 𝑓)) |
83 | 46, 48, 52, 53, 82 | 2rspcedvdw 3635 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐸) → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)) |
84 | | oveq1 7437 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑒 → (𝑖 + 𝑗) = (𝑒 + 𝑗)) |
85 | 84 | eqeq2d 2745 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑒 → ((𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗) ↔ (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑒 + 𝑗))) |
86 | | oveq2 7438 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑓 + 𝑥) → (𝑒 + 𝑗) = (𝑒 + (𝑓 + 𝑥))) |
87 | 86 | eqeq2d 2745 |
. . . . . . . . . 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 33022 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐹) → (𝑓 + 𝑥) ∈ 𝐹) |
93 | 38, 40, 54, 73, 76, 66 | mndassd 33010 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → ((𝑒 + 𝑓) + 𝑥) = (𝑒 + (𝑓 + 𝑥))) |
94 | 68, 70, 93 | 3eqtrd 2778 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑒 + (𝑓 + 𝑥))) |
95 | 94 | adantr 480 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐹) → (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑒 + (𝑓 + 𝑥))) |
96 | 85, 87, 88, 92, 95 | 2rspcedvdw 3635 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) ∧ 𝑥 ∈ 𝐹) → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)) |
97 | | elun 4162 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐸 ∪ 𝐹) ↔ (𝑥 ∈ 𝐸 ∨ 𝑥 ∈ 𝐹)) |
98 | 97 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐸 ∪ 𝐹) → (𝑥 ∈ 𝐸 ∨ 𝑥 ∈ 𝐹)) |
99 | 98 | ad4antlr 733 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → (𝑥 ∈ 𝐸 ∨ 𝑥 ∈ 𝐹)) |
100 | 83, 96, 99 | mpjaodan 960 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑤 ∈ Word (𝐸 ∪ 𝐹)) ∧ 𝑥 ∈ (𝐸 ∪ 𝐹)) ∧ 𝑒 ∈ 𝐸) ∧ 𝑓 ∈ 𝐹) ∧ (𝑀 Σg 𝑤) = (𝑒 + 𝑓)) → ∃𝑖 ∈ 𝐸 ∃𝑗 ∈ 𝐹 (𝑀 Σg (𝑤 ++ 〈“𝑥”〉)) = (𝑖 + 𝑗)) |
101 | 100 | r19.29ffa 32499 |
. . . . . . 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 14756 |
. 2
⊢ (𝑊 ∈ Word (𝐸 ∪ 𝐹) → (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑊) = (𝑒 + 𝑓))) |
107 | 1, 106 | mpcom 38 |
1
⊢ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑊) = (𝑒 + 𝑓)) |