Step | Hyp | Ref
| Expression |
1 | | frgpup.w |
. . . . . . 7
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | frgpup.r |
. . . . . . 7
⊢ ∼ = (
~FG ‘𝐼) |
3 | 1, 2 | efgval 18130 |
. . . . . 6
⊢ ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))} |
4 | | coeq2 5280 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑣 → (𝑇 ∘ 𝑢) = (𝑇 ∘ 𝑣)) |
5 | 4 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) |
6 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
{〈𝑢, 𝑣〉 ∣ (𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} = {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} |
7 | 5, 6 | eqer 7777 |
. . . . . . . . . . 11
⊢
{〈𝑢, 𝑣〉 ∣ (𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} Er V |
8 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} Er V) |
9 | | ssv 3625 |
. . . . . . . . . . 11
⊢ 𝑊 ⊆ V |
10 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ⊆ V) |
11 | 8, 10 | erinxp 7821 |
. . . . . . . . 9
⊢ (𝜑 → ({〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊) |
12 | | df-xp 5120 |
. . . . . . . . . . . . 13
⊢ (𝑊 × 𝑊) = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊)} |
13 | 12 | ineq1i 3810 |
. . . . . . . . . . . 12
⊢ ((𝑊 × 𝑊) ∩ {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) = ({〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊)} ∩ {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) |
14 | | incom 3805 |
. . . . . . . . . . . 12
⊢ ((𝑊 × 𝑊) ∩ {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) = ({〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) |
15 | | inopab 5252 |
. . . . . . . . . . . 12
⊢
({〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊)} ∩ {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} |
16 | 13, 14, 15 | 3eqtr3i 2652 |
. . . . . . . . . . 11
⊢
({〈𝑢, 𝑣〉 ∣ (𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} |
17 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑢 ∈ V |
18 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑣 ∈ V |
19 | 17, 18 | prss 4351 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ↔ {𝑢, 𝑣} ⊆ 𝑊) |
20 | 19 | anbi1i 731 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) ↔ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))) |
21 | 20 | opabbii 4717 |
. . . . . . . . . . 11
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} |
22 | 16, 21 | eqtri 2644 |
. . . . . . . . . 10
⊢
({〈𝑢, 𝑣〉 ∣ (𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} |
23 | | ereq1 7749 |
. . . . . . . . . 10
⊢
(({〈𝑢, 𝑣〉 ∣ (𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (({〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊 ↔ {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . 9
⊢
(({〈𝑢, 𝑣〉 ∣ (𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊 ↔ {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊) |
25 | 11, 24 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊) |
26 | | simplrl 800 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑥 ∈ 𝑊) |
27 | | fviss 6256 |
. . . . . . . . . . . . . . . 16
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
28 | 1, 27 | eqsstri 3635 |
. . . . . . . . . . . . . . 15
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
29 | 28, 26 | sseldi 3601 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑥 ∈ Word (𝐼 ×
2𝑜)) |
30 | | opelxpi 5148 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) →
〈𝑎, 𝑏〉 ∈ (𝐼 ×
2𝑜)) |
31 | 30 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
〈𝑎, 𝑏〉 ∈ (𝐼 ×
2𝑜)) |
32 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑎 ∈ 𝐼) |
33 | | 2oconcl 7583 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ 2𝑜
→ (1𝑜 ∖ 𝑏) ∈
2𝑜) |
34 | 33 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
(1𝑜 ∖ 𝑏) ∈
2𝑜) |
35 | | opelxpi 5148 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝐼 ∧ (1𝑜 ∖ 𝑏) ∈ 2𝑜)
→ 〈𝑎,
(1𝑜 ∖ 𝑏)〉 ∈ (𝐼 ×
2𝑜)) |
36 | 32, 34, 35 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
〈𝑎,
(1𝑜 ∖ 𝑏)〉 ∈ (𝐼 ×
2𝑜)) |
37 | 31, 36 | s2cld 13616 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉 ∈ Word
(𝐼 ×
2𝑜)) |
38 | | splcl 13503 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word (𝐼 × 2𝑜) ∧
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉 ∈ Word
(𝐼 ×
2𝑜)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
∈ Word (𝐼 ×
2𝑜)) |
39 | 29, 37, 38 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
∈ Word (𝐼 ×
2𝑜)) |
40 | 1 | efgrcl 18128 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
41 | 26, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
42 | 41 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑊 = Word (𝐼 ×
2𝑜)) |
43 | 39, 42 | eleqtrrd 2704 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
∈ 𝑊) |
44 | 26, 43 | jca 554 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
∈ 𝑊)) |
45 | | swrdcl 13419 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) →
(𝑥 substr 〈0, 𝑛〉) ∈ Word (𝐼 ×
2𝑜)) |
46 | 29, 45 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 substr 〈0, 𝑛〉) ∈ Word (𝐼 ×
2𝑜)) |
47 | | frgpup.b |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐵 = (Base‘𝐻) |
48 | | frgpup.n |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑁 = (invg‘𝐻) |
49 | | frgpup.t |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) |
50 | | frgpup.h |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐻 ∈ Grp) |
51 | | frgpup.i |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
52 | | frgpup.a |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:𝐼⟶𝐵) |
53 | 47, 48, 49, 50, 51, 52 | frgpuptf 18183 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇:(𝐼 × 2𝑜)⟶𝐵) |
54 | 53 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑇:(𝐼 × 2𝑜)⟶𝐵) |
55 | | ccatco 13581 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 substr 〈0, 𝑛〉) ∈ Word (𝐼 × 2𝑜)
∧ 〈“〈𝑎,
𝑏〉〈𝑎, (1𝑜 ∖
𝑏)〉”〉
∈ Word (𝐼 ×
2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) = ((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉))) |
56 | 46, 37, 54, 55 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) = ((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉))) |
57 | 56 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
(𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉))) = (𝐻 Σg
((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)))) |
58 | 50 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝐻 ∈ Grp) |
59 | | grpmnd 17429 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻 ∈ Grp → 𝐻 ∈ Mnd) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝐻 ∈ Mnd) |
61 | | wrdco 13577 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 substr 〈0, 𝑛〉) ∈ Word (𝐼 × 2𝑜)
∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ∈ Word 𝐵) |
62 | 46, 54, 61 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ∈ Word 𝐵) |
63 | | wrdco 13577 |
. . . . . . . . . . . . . . . . 17
⊢
((〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉 ∈ Word
(𝐼 ×
2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ∈
Word 𝐵) |
64 | 37, 54, 63 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ∈
Word 𝐵) |
65 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘𝐻) = (+g‘𝐻) |
66 | 47, 65 | gsumccat 17378 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ∈ Word 𝐵 ∧ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ∈
Word 𝐵) → (𝐻 Σg
((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉))) =
((𝐻
Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)))) |
67 | 60, 62, 64, 66 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉))) =
((𝐻
Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)))) |
68 | 54, 31, 36 | s2co 13665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) =
〈“(𝑇‘〈𝑎, 𝑏〉)(𝑇‘〈𝑎, (1𝑜 ∖ 𝑏)〉)”〉) |
69 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎𝑇𝑏) = (𝑇‘〈𝑎, 𝑏〉) |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑎𝑇𝑏) = (𝑇‘〈𝑎, 𝑏〉)) |
71 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎(𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)𝑏) = ((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘〈𝑎, 𝑏〉) |
72 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
73 | 72 | efgmval 18125 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → (𝑎(𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)𝑏) = 〈𝑎, (1𝑜 ∖ 𝑏)〉) |
74 | 71, 73 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘〈𝑎, 𝑏〉) = 〈𝑎, (1𝑜 ∖ 𝑏)〉) |
75 | 74 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘〈𝑎, 𝑏〉) = 〈𝑎, (1𝑜 ∖ 𝑏)〉) |
76 | 75 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘〈𝑎, 𝑏〉)) = (𝑇‘〈𝑎, (1𝑜 ∖ 𝑏)〉)) |
77 | 47, 48, 49, 50, 51, 52, 72 | frgpuptinv 18184 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 〈𝑎, 𝑏〉 ∈ (𝐼 × 2𝑜)) →
(𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘〈𝑎, 𝑏〉)) = (𝑁‘(𝑇‘〈𝑎, 𝑏〉))) |
78 | 30, 77 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘〈𝑎, 𝑏〉)) = (𝑁‘(𝑇‘〈𝑎, 𝑏〉))) |
79 | 78 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘〈𝑎, 𝑏〉)) = (𝑁‘(𝑇‘〈𝑎, 𝑏〉))) |
80 | 76, 79 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘〈𝑎, (1𝑜 ∖ 𝑏)〉) = (𝑁‘(𝑇‘〈𝑎, 𝑏〉))) |
81 | 69 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑇‘〈𝑎, 𝑏〉)) |
82 | 80, 81 | syl6reqr 2675 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑁‘(𝑎𝑇𝑏)) = (𝑇‘〈𝑎, (1𝑜 ∖ 𝑏)〉)) |
83 | 70, 82 | s2eqd 13608 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
〈“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”〉 = 〈“(𝑇‘〈𝑎, 𝑏〉)(𝑇‘〈𝑎, (1𝑜 ∖ 𝑏)〉)”〉) |
84 | 68, 83 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) =
〈“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”〉) |
85 | 84 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
(𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) = (𝐻 Σg
〈“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”〉)) |
86 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑏 ∈
2𝑜) |
87 | 54, 32, 86 | fovrnd 6806 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑎𝑇𝑏) ∈ 𝐵) |
88 | 47, 48 | grpinvcl 17467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) |
89 | 58, 87, 88 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) |
90 | 47, 65 | gsumws2 17379 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐻 ∈ Mnd ∧ (𝑎𝑇𝑏) ∈ 𝐵 ∧ (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) → (𝐻 Σg
〈“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”〉) = ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏)))) |
91 | 60, 87, 89, 90 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
〈“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”〉) = ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏)))) |
92 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0g‘𝐻) = (0g‘𝐻) |
93 | 47, 65, 92, 48 | grprinv 17469 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g‘𝐻)) |
94 | 58, 87, 93 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g‘𝐻)) |
95 | 85, 91, 94 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
(𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) =
(0g‘𝐻)) |
96 | 95 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
((𝐻
Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉))) =
((𝐻
Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))(+g‘𝐻)(0g‘𝐻))) |
97 | 47 | gsumwcl 17377 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ∈ Word 𝐵) → (𝐻 Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉))) ∈ 𝐵) |
98 | 60, 62, 97 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
(𝑇 ∘ (𝑥 substr 〈0, 𝑛〉))) ∈ 𝐵) |
99 | 47, 65, 92 | grprid 17453 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 ∈ Grp ∧ (𝐻 Σg
(𝑇 ∘ (𝑥 substr 〈0, 𝑛〉))) ∈ 𝐵) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))(+g‘𝐻)(0g‘𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))) |
100 | 58, 98, 99 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
((𝐻
Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))(+g‘𝐻)(0g‘𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))) |
101 | 96, 100 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
((𝐻
Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉))) = (𝐻 Σg
(𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))) |
102 | 57, 67, 101 | 3eqtrrd 2661 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
(𝑇 ∘ (𝑥 substr 〈0, 𝑛〉))) = (𝐻 Σg (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)))) |
103 | 102 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
((𝐻
Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉))))) |
104 | | swrdcl 13419 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) →
(𝑥 substr 〈𝑛, (#‘𝑥)〉) ∈ Word (𝐼 ×
2𝑜)) |
105 | 29, 104 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 substr 〈𝑛, (#‘𝑥)〉) ∈ Word (𝐼 ×
2𝑜)) |
106 | | wrdco 13577 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 substr 〈𝑛, (#‘𝑥)〉) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)) ∈ Word 𝐵) |
107 | 105, 54, 106 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)) ∈ Word 𝐵) |
108 | 47, 65 | gsumccat 17378 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉))))) |
109 | 60, 62, 107, 108 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉))))) |
110 | | ccatcl 13359 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 substr 〈0, 𝑛〉) ∈ Word (𝐼 × 2𝑜)
∧ 〈“〈𝑎,
𝑏〉〈𝑎, (1𝑜 ∖
𝑏)〉”〉
∈ Word (𝐼 ×
2𝑜)) → ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ∈
Word (𝐼 ×
2𝑜)) |
111 | 46, 37, 110 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
((𝑥 substr 〈0, 𝑛〉) ++
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ∈
Word (𝐼 ×
2𝑜)) |
112 | | wrdco 13577 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 substr 〈0, 𝑛〉) ++
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ∈
Word (𝐼 ×
2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) ∈
Word 𝐵) |
113 | 111, 54, 112 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) ∈
Word 𝐵) |
114 | 47, 65 | gsumccat 17378 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) ∈
Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉))))) |
115 | 60, 113, 107, 114 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
((𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉))))) |
116 | 103, 109,
115 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉))))) |
117 | | simplrr 801 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑛 ∈ (0...(#‘𝑥))) |
118 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (0...(#‘𝑥)) → 𝑛 ∈
(ℤ≥‘0)) |
119 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑛)) |
120 | 117, 118,
119 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 0
∈ (0...𝑛)) |
121 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) →
(#‘𝑥) ∈
ℕ0) |
122 | 29, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
(#‘𝑥) ∈
ℕ0) |
123 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) |
124 | 122, 123 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
(#‘𝑥) ∈
(ℤ≥‘0)) |
125 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑥) ∈
(ℤ≥‘0) → (#‘𝑥) ∈ (0...(#‘𝑥))) |
126 | 124, 125 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
(#‘𝑥) ∈
(0...(#‘𝑥))) |
127 | | ccatswrd 13456 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ Word (𝐼 × 2𝑜) ∧ (0
∈ (0...𝑛) ∧ 𝑛 ∈ (0...(#‘𝑥)) ∧ (#‘𝑥) ∈ (0...(#‘𝑥)))) → ((𝑥 substr 〈0, 𝑛〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉)) = (𝑥 substr 〈0, (#‘𝑥)〉)) |
128 | 29, 120, 117, 126, 127 | syl13anc 1328 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
((𝑥 substr 〈0, 𝑛〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉)) = (𝑥 substr 〈0, (#‘𝑥)〉)) |
129 | | swrdid 13428 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) →
(𝑥 substr 〈0,
(#‘𝑥)〉) = 𝑥) |
130 | 29, 129 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 substr 〈0, (#‘𝑥)〉) = 𝑥) |
131 | 128, 130 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) →
((𝑥 substr 〈0, 𝑛〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉)) = 𝑥) |
132 | 131 | coeq2d 5284 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉))) = (𝑇 ∘ 𝑥)) |
133 | | ccatco 13581 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 substr 〈0, 𝑛〉) ∈ Word (𝐼 × 2𝑜)
∧ (𝑥 substr 〈𝑛, (#‘𝑥)〉) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉))) = ((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) |
134 | 46, 105, 54, 133 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉))) = ((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) |
135 | 132, 134 | eqtr3d 2658 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ 𝑥) = ((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) |
136 | 135 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
(𝑇 ∘ 𝑥)) = (𝐻 Σg ((𝑇 ∘ (𝑥 substr 〈0, 𝑛〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉))))) |
137 | | splval 13502 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑊 ∧ (𝑛 ∈ (0...(#‘𝑥)) ∧ 𝑛 ∈ (0...(#‘𝑥)) ∧ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉 ∈ Word
(𝐼 ×
2𝑜))) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉) =
(((𝑥 substr 〈0, 𝑛〉) ++
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉))) |
138 | 26, 117, 117, 37, 137 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉) =
(((𝑥 substr 〈0, 𝑛〉) ++
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉))) |
139 | 138 | coeq2d 5284 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)) =
(𝑇 ∘ (((𝑥 substr 〈0, 𝑛〉) ++
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) |
140 | | ccatco 13581 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 substr 〈0, 𝑛〉) ++
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ∈
Word (𝐼 ×
2𝑜) ∧ (𝑥 substr 〈𝑛, (#‘𝑥)〉) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉))) = ((𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) |
141 | 111, 105,
54, 140 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ (((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉) ++ (𝑥 substr 〈𝑛, (#‘𝑥)〉))) = ((𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) |
142 | 139, 141 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)) =
((𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++
〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉)))) |
143 | 142 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
(𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))) =
(𝐻
Σg ((𝑇 ∘ ((𝑥 substr 〈0, 𝑛〉) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (#‘𝑥)〉))))) |
144 | 116, 136,
143 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg
(𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)))) |
145 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
146 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
∈ V |
147 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑊 ↔ 𝑥 ∈ 𝑊)) |
148 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
→ (𝑣 ∈ 𝑊 ↔ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
∈ 𝑊)) |
149 | 147, 148 | bi2anan9 917 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))
→ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ↔ (𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
∈ 𝑊))) |
150 | 19, 149 | syl5bbr 274 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))
→ ({𝑢, 𝑣} ⊆ 𝑊 ↔ (𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
∈ 𝑊))) |
151 | | coeq2 5280 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑥 → (𝑇 ∘ 𝑢) = (𝑇 ∘ 𝑥)) |
152 | 151 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑥 → (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑥))) |
153 | | coeq2 5280 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
→ (𝑇 ∘ 𝑣) = (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))) |
154 | 153 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
→ (𝐻
Σg (𝑇 ∘ 𝑣)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)))) |
155 | 152, 154 | eqeqan12d 2638 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))
→ ((𝐻
Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)) ↔ (𝐻 Σg (𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))))) |
156 | 150, 155 | anbi12d 747 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))
→ (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) ↔ ((𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
∈ 𝑊) ∧ (𝐻 Σg
(𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)))))) |
157 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} |
158 | 145, 146,
156, 157 | braba 4992 |
. . . . . . . . . . 11
⊢ (𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
↔ ((𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
∈ 𝑊) ∧ (𝐻 Σg
(𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))))) |
159 | 44, 144, 158 | sylanbrc 698 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)) |
160 | 159 | ralrimivva 2971 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)) |
161 | 160 | ralrimivva 2971 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)) |
162 | | fvex 6201 |
. . . . . . . . . . 11
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ∈ V |
163 | 1, 162 | eqeltri 2697 |
. . . . . . . . . 10
⊢ 𝑊 ∈ V |
164 | | erex 7766 |
. . . . . . . . . 10
⊢
({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 → (𝑊 ∈ V → {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ V)) |
165 | 25, 163, 164 | mpisyl 21 |
. . . . . . . . 9
⊢ (𝜑 → {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ V) |
166 | | ereq1 7749 |
. . . . . . . . . . 11
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (𝑟 Er 𝑊 ↔ {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊)) |
167 | | breq 4655 |
. . . . . . . . . . . . 13
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
↔ 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))) |
168 | 167 | 2ralbidv 2989 |
. . . . . . . . . . . 12
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
↔ ∀𝑎 ∈
𝐼 ∀𝑏 ∈ 2𝑜
𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))) |
169 | 168 | 2ralbidv 2989 |
. . . . . . . . . . 11
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)
↔ ∀𝑥 ∈
𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))) |
170 | 166, 169 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → ((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))
↔ ({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)))) |
171 | 170 | elabg 3351 |
. . . . . . . . 9
⊢
({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ V → ({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))}
↔ ({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)))) |
172 | 165, 171 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))}
↔ ({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉)))) |
173 | 25, 161, 172 | mpbir2and 957 |
. . . . . . 7
⊢ (𝜑 → {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))}) |
174 | | intss1 4492 |
. . . . . . 7
⊢
({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))}
→ ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))}
⊆ {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}) |
175 | 173, 174 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1𝑜 ∖ 𝑏)〉”〉〉))}
⊆ {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}) |
176 | 3, 175 | syl5eqss 3649 |
. . . . 5
⊢ (𝜑 → ∼ ⊆
{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}) |
177 | 176 | ssbrd 4696 |
. . . 4
⊢ (𝜑 → (𝐴 ∼ 𝐶 → 𝐴{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶)) |
178 | 177 | imp 445 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → 𝐴{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶) |
179 | 1, 2 | efger 18131 |
. . . . . 6
⊢ ∼ Er
𝑊 |
180 | | errel 7751 |
. . . . . 6
⊢ ( ∼ Er
𝑊 → Rel ∼
) |
181 | 179, 180 | mp1i 13 |
. . . . 5
⊢ (𝜑 → Rel ∼ ) |
182 | | brrelex12 5155 |
. . . . 5
⊢ ((Rel
∼
∧ 𝐴 ∼ 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
183 | 181, 182 | sylan 488 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
184 | | preq12 4270 |
. . . . . . 7
⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → {𝑢, 𝑣} = {𝐴, 𝐶}) |
185 | 184 | sseq1d 3632 |
. . . . . 6
⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ {𝐴, 𝐶} ⊆ 𝑊)) |
186 | | coeq2 5280 |
. . . . . . . 8
⊢ (𝑢 = 𝐴 → (𝑇 ∘ 𝑢) = (𝑇 ∘ 𝐴)) |
187 | 186 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑢 = 𝐴 → (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝐴))) |
188 | | coeq2 5280 |
. . . . . . . 8
⊢ (𝑣 = 𝐶 → (𝑇 ∘ 𝑣) = (𝑇 ∘ 𝐶)) |
189 | 188 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑣 = 𝐶 → (𝐻 Σg (𝑇 ∘ 𝑣)) = (𝐻 Σg (𝑇 ∘ 𝐶))) |
190 | 187, 189 | eqeqan12d 2638 |
. . . . . 6
⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → ((𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)) ↔ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶)))) |
191 | 185, 190 | anbi12d 747 |
. . . . 5
⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))))) |
192 | 191, 157 | brabga 4989 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))))) |
193 | 183, 192 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐴{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))))) |
194 | 178, 193 | mpbid 222 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶)))) |
195 | 194 | simprd 479 |
1
⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))) |