| Step | Hyp | Ref
| Expression |
| 1 | | frgpup.w |
. . . . . . 7
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) |
| 2 | | frgpup.r |
. . . . . . 7
⊢ ∼ = (
~FG ‘𝐼) |
| 3 | 1, 2 | efgval 19735 |
. . . . . 6
⊢ ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))} |
| 4 | | coeq2 5869 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑣 → (𝑇 ∘ 𝑢) = (𝑇 ∘ 𝑣)) |
| 5 | 4 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) |
| 6 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
{〈𝑢, 𝑣〉 ∣ (𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} = {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} |
| 7 | 5, 6 | eqer 8781 |
. . . . . . . . . . 11
⊢
{〈𝑢, 𝑣〉 ∣ (𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} Er V |
| 8 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} Er V) |
| 9 | | ssv 4008 |
. . . . . . . . . . 11
⊢ 𝑊 ⊆ V |
| 10 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ⊆ V) |
| 11 | 8, 10 | erinxp 8831 |
. . . . . . . . 9
⊢ (𝜑 → ({〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊) |
| 12 | | df-xp 5691 |
. . . . . . . . . . . . 13
⊢ (𝑊 × 𝑊) = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊)} |
| 13 | 12 | ineq1i 4216 |
. . . . . . . . . . . 12
⊢ ((𝑊 × 𝑊) ∩ {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) = ({〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊)} ∩ {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) |
| 14 | | incom 4209 |
. . . . . . . . . . . 12
⊢ ((𝑊 × 𝑊) ∩ {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) = ({〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) |
| 15 | | inopab 5839 |
. . . . . . . . . . . 12
⊢
({〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊)} ∩ {〈𝑢, 𝑣〉 ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} |
| 16 | 13, 14, 15 | 3eqtr3i 2773 |
. . . . . . . . . . 11
⊢
({〈𝑢, 𝑣〉 ∣ (𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} |
| 17 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑢 ∈ V |
| 18 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑣 ∈ V |
| 19 | 17, 18 | prss 4820 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ↔ {𝑢, 𝑣} ⊆ 𝑊) |
| 20 | 19 | anbi1i 624 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) ↔ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))) |
| 21 | 20 | opabbii 5210 |
. . . . . . . . . . 11
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} |
| 22 | 16, 21 | eqtri 2765 |
. . . . . . . . . 10
⊢
({〈𝑢, 𝑣〉 ∣ (𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} |
| 23 | | ereq1 8752 |
. . . . . . . . . 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 218 |
. . . . . . . 8
⊢ (𝜑 → {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊) |
| 26 | | simplrl 777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 𝑥 ∈ 𝑊) |
| 27 | | fviss 6986 |
. . . . . . . . . . . . . . 15
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) |
| 28 | 1, 27 | eqsstri 4030 |
. . . . . . . . . . . . . 14
⊢ 𝑊 ⊆ Word (𝐼 × 2o) |
| 29 | 28, 26 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 𝑥 ∈ Word (𝐼 × 2o)) |
| 30 | | opelxpi 5722 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → 〈𝑎, 𝑏〉 ∈ (𝐼 × 2o)) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 〈𝑎, 𝑏〉 ∈ (𝐼 × 2o)) |
| 32 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 𝑎 ∈ 𝐼) |
| 33 | | 2oconcl 8541 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ 2o →
(1o ∖ 𝑏)
∈ 2o) |
| 34 | 33 | ad2antll 729 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (1o
∖ 𝑏) ∈
2o) |
| 35 | 32, 34 | opelxpd 5724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 〈𝑎, (1o ∖ 𝑏)〉 ∈ (𝐼 ×
2o)) |
| 36 | 31, 35 | s2cld 14910 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) →
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉 ∈ Word (𝐼 ×
2o)) |
| 37 | | splcl 14790 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Word (𝐼 × 2o) ∧
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉 ∈ Word (𝐼 × 2o)) →
(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ∈ Word
(𝐼 ×
2o)) |
| 38 | 29, 36, 37 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ∈ Word
(𝐼 ×
2o)) |
| 39 | 1 | efgrcl 19733 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) |
| 40 | 26, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) |
| 41 | 40 | simprd 495 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 𝑊 = Word (𝐼 × 2o)) |
| 42 | 38, 41 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ∈ 𝑊) |
| 43 | | pfxcl 14715 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ Word (𝐼 × 2o) → (𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o)) |
| 44 | 29, 43 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o)) |
| 45 | | frgpup.b |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐵 = (Base‘𝐻) |
| 46 | | frgpup.n |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑁 = (invg‘𝐻) |
| 47 | | frgpup.t |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) |
| 48 | | frgpup.h |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐻 ∈ Grp) |
| 49 | | frgpup.i |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
| 50 | | frgpup.a |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:𝐼⟶𝐵) |
| 51 | 45, 46, 47, 48, 49, 50 | frgpuptf 19788 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇:(𝐼 × 2o)⟶𝐵) |
| 52 | 51 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 𝑇:(𝐼 × 2o)⟶𝐵) |
| 53 | | ccatco 14874 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉 ∈ Word (𝐼 × 2o) ∧
𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉))) |
| 54 | 44, 36, 52, 53 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉))) |
| 55 | 54 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
(𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉))) = (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)))) |
| 56 | 48 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 𝐻 ∈ Grp) |
| 57 | 56 | grpmndd 18964 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 𝐻 ∈ Mnd) |
| 58 | | wrdco 14870 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵) |
| 59 | 44, 52, 58 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵) |
| 60 | | wrdco 14870 |
. . . . . . . . . . . . . . . . 17
⊢
((〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉 ∈ Word (𝐼 × 2o) ∧
𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ∈ Word 𝐵) |
| 61 | 36, 52, 60 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ∈ Word 𝐵) |
| 62 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘𝐻) = (+g‘𝐻) |
| 63 | 45, 62 | gsumccat 18854 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵 ∧ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)))) |
| 64 | 57, 59, 61, 63 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)))) |
| 65 | 52, 31, 35 | s2co 14959 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) = 〈“(𝑇‘〈𝑎, 𝑏〉)(𝑇‘〈𝑎, (1o ∖ 𝑏)〉)”〉) |
| 66 | | df-ov 7434 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎𝑇𝑏) = (𝑇‘〈𝑎, 𝑏〉) |
| 67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑎𝑇𝑏) = (𝑇‘〈𝑎, 𝑏〉)) |
| 68 | 66 | fveq2i 6909 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑇‘〈𝑎, 𝑏〉)) |
| 69 | | df-ov 7434 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎(𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)𝑏) = ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)‘〈𝑎, 𝑏〉) |
| 70 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) |
| 71 | 70 | efgmval 19730 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑎(𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)𝑏) = 〈𝑎, (1o ∖ 𝑏)〉) |
| 72 | 69, 71 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)‘〈𝑎, 𝑏〉) = 〈𝑎, (1o ∖ 𝑏)〉) |
| 73 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)‘〈𝑎, 𝑏〉) = 〈𝑎, (1o ∖ 𝑏)〉) |
| 74 | 73 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)‘〈𝑎, 𝑏〉)) = (𝑇‘〈𝑎, (1o ∖ 𝑏)〉)) |
| 75 | 45, 46, 47, 48, 49, 50, 70 | frgpuptinv 19789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 〈𝑎, 𝑏〉 ∈ (𝐼 × 2o)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)‘〈𝑎, 𝑏〉)) = (𝑁‘(𝑇‘〈𝑎, 𝑏〉))) |
| 76 | 30, 75 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)‘〈𝑎, 𝑏〉)) = (𝑁‘(𝑇‘〈𝑎, 𝑏〉))) |
| 77 | 76 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)‘〈𝑎, 𝑏〉)) = (𝑁‘(𝑇‘〈𝑎, 𝑏〉))) |
| 78 | 74, 77 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇‘〈𝑎, (1o ∖ 𝑏)〉) = (𝑁‘(𝑇‘〈𝑎, 𝑏〉))) |
| 79 | 68, 78 | eqtr4id 2796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑁‘(𝑎𝑇𝑏)) = (𝑇‘〈𝑎, (1o ∖ 𝑏)〉)) |
| 80 | 67, 79 | s2eqd 14902 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) →
〈“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”〉 = 〈“(𝑇‘〈𝑎, 𝑏〉)(𝑇‘〈𝑎, (1o ∖ 𝑏)〉)”〉) |
| 81 | 65, 80 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) = 〈“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”〉) |
| 82 | 81 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
(𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) = (𝐻 Σg
〈“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”〉)) |
| 83 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 𝑏 ∈
2o) |
| 84 | 52, 32, 83 | fovcdmd 7605 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑎𝑇𝑏) ∈ 𝐵) |
| 85 | 45, 46 | grpinvcl 19005 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) |
| 86 | 56, 84, 85 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) |
| 87 | 45, 62 | gsumws2 18855 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐻 ∈ Mnd ∧ (𝑎𝑇𝑏) ∈ 𝐵 ∧ (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) → (𝐻 Σg
〈“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”〉) = ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏)))) |
| 88 | 57, 84, 86, 87 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
〈“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”〉) = ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏)))) |
| 89 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0g‘𝐻) = (0g‘𝐻) |
| 90 | 45, 62, 89, 46 | grprinv 19008 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g‘𝐻)) |
| 91 | 56, 84, 90 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g‘𝐻)) |
| 92 | 82, 88, 91 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
(𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) =
(0g‘𝐻)) |
| 93 | 92 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → ((𝐻 Σg
(𝑇 ∘ (𝑥 prefix 𝑛)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g‘𝐻)(0g‘𝐻))) |
| 94 | 45 | gsumwcl 18852 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵) → (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵) |
| 95 | 57, 59, 94 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
(𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵) |
| 96 | 45, 62, 89 | grprid 18986 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 ∈ Grp ∧ (𝐻 Σg
(𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g‘𝐻)(0g‘𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))) |
| 97 | 56, 95, 96 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → ((𝐻 Σg
(𝑇 ∘ (𝑥 prefix 𝑛)))(+g‘𝐻)(0g‘𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))) |
| 98 | 93, 97 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → ((𝐻 Σg
(𝑇 ∘ (𝑥 prefix 𝑛)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉))) = (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))) |
| 99 | 55, 64, 98 | 3eqtrrd 2782 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
(𝑇 ∘ (𝑥 prefix 𝑛))) = (𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)))) |
| 100 | 99 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → ((𝐻 Σg
(𝑇 ∘ (𝑥 prefix 𝑛)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))))) |
| 101 | | swrdcl 14683 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Word (𝐼 × 2o) → (𝑥 substr 〈𝑛, (♯‘𝑥)〉) ∈ Word (𝐼 × 2o)) |
| 102 | 29, 101 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑥 substr 〈𝑛, (♯‘𝑥)〉) ∈ Word (𝐼 × 2o)) |
| 103 | | wrdco 14870 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 substr 〈𝑛, (♯‘𝑥)〉) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)) ∈ Word 𝐵) |
| 104 | 102, 52, 103 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)) ∈ Word 𝐵) |
| 105 | 45, 62 | gsumccat 18854 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))))) |
| 106 | 57, 59, 104, 105 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))))) |
| 107 | | ccatcl 14612 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉 ∈ Word (𝐼 × 2o)) →
((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ∈ Word (𝐼 ×
2o)) |
| 108 | 44, 36, 107 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ∈ Word (𝐼 ×
2o)) |
| 109 | | wrdco 14870 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ∈ Word (𝐼 × 2o) ∧
𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) ∈ Word 𝐵) |
| 110 | 108, 52, 109 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) ∈ Word 𝐵) |
| 111 | 45, 62 | gsumccat 18854 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))))) |
| 112 | 57, 110, 104, 111 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
((𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))))) |
| 113 | 100, 106,
112 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))))) |
| 114 | | simplrr 778 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 𝑛 ∈
(0...(♯‘𝑥))) |
| 115 | | lencl 14571 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ Word (𝐼 × 2o) →
(♯‘𝑥) ∈
ℕ0) |
| 116 | 29, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) →
(♯‘𝑥) ∈
ℕ0) |
| 117 | | nn0uz 12920 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) |
| 118 | 116, 117 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) →
(♯‘𝑥) ∈
(ℤ≥‘0)) |
| 119 | | eluzfz2 13572 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑥)
∈ (ℤ≥‘0) → (♯‘𝑥) ∈
(0...(♯‘𝑥))) |
| 120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) →
(♯‘𝑥) ∈
(0...(♯‘𝑥))) |
| 121 | | ccatpfx 14739 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑛 ∈
(0...(♯‘𝑥))
∧ (♯‘𝑥)
∈ (0...(♯‘𝑥))) → ((𝑥 prefix 𝑛) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)) = (𝑥 prefix (♯‘𝑥))) |
| 122 | 29, 114, 120, 121 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → ((𝑥 prefix 𝑛) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)) = (𝑥 prefix (♯‘𝑥))) |
| 123 | | pfxid 14722 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ Word (𝐼 × 2o) → (𝑥 prefix (♯‘𝑥)) = 𝑥) |
| 124 | 29, 123 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑥 prefix (♯‘𝑥)) = 𝑥) |
| 125 | 122, 124 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → ((𝑥 prefix 𝑛) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)) = 𝑥) |
| 126 | 125 | coeq2d 5873 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))) = (𝑇 ∘ 𝑥)) |
| 127 | | ccatco 14874 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧ (𝑥 substr 〈𝑛, (♯‘𝑥)〉) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) |
| 128 | 44, 102, 52, 127 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) |
| 129 | 126, 128 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘ 𝑥) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) |
| 130 | 129 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
(𝑇 ∘ 𝑥)) = (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))))) |
| 131 | | splval 14789 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑊 ∧ (𝑛 ∈ (0...(♯‘𝑥)) ∧ 𝑛 ∈ (0...(♯‘𝑥)) ∧
〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉 ∈ Word (𝐼 × 2o))) →
(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) = (((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))) |
| 132 | 26, 114, 114, 36, 131 | syl13anc 1374 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) = (((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))) |
| 133 | 132 | coeq2d 5873 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) = (𝑇 ∘ (((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) |
| 134 | | ccatco 14874 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ∈ Word (𝐼 × 2o) ∧
(𝑥 substr 〈𝑛, (♯‘𝑥)〉) ∈ Word (𝐼 × 2o) ∧
𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) |
| 135 | 108, 102,
52, 134 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘ (((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉) ++ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) |
| 136 | 133, 135 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉)))) |
| 137 | 136 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
(𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))) = (𝐻 Σg
((𝑇 ∘ ((𝑥 prefix 𝑛) ++ 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉)) ++ (𝑇 ∘ (𝑥 substr 〈𝑛, (♯‘𝑥)〉))))) |
| 138 | 113, 130,
137 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → (𝐻 Σg
(𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)))) |
| 139 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
| 140 | | ovex 7464 |
. . . . . . . . . . . 12
⊢ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ∈
V |
| 141 | | eleq1 2829 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑊 ↔ 𝑥 ∈ 𝑊)) |
| 142 | | eleq1 2829 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) → (𝑣 ∈ 𝑊 ↔ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ∈ 𝑊)) |
| 143 | 141, 142 | bi2anan9 638 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) → ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ↔ (𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ∈ 𝑊))) |
| 144 | 19, 143 | bitr3id 285 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ (𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ∈ 𝑊))) |
| 145 | | coeq2 5869 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑥 → (𝑇 ∘ 𝑢) = (𝑇 ∘ 𝑥)) |
| 146 | 145 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑥 → (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑥))) |
| 147 | | coeq2 5869 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) → (𝑇 ∘ 𝑣) = (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))) |
| 148 | 147 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) → (𝐻 Σg
(𝑇 ∘ 𝑣)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)))) |
| 149 | 146, 148 | eqeqan12d 2751 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) → ((𝐻 Σg
(𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)) ↔ (𝐻 Σg (𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))))) |
| 150 | 144, 149 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) ↔ ((𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)))))) |
| 151 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} |
| 152 | 139, 140,
150, 151 | braba 5542 |
. . . . . . . . . . 11
⊢ (𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ↔ ((𝑥 ∈ 𝑊 ∧ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))))) |
| 153 | 26, 42, 138, 152 | syl21anbrc 1345 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o)) → 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) |
| 154 | 153 | ralrimivva 3202 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(♯‘𝑥)))) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) |
| 155 | 154 | ralrimivva 3202 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) |
| 156 | 1 | fvexi 6920 |
. . . . . . . . . 10
⊢ 𝑊 ∈ V |
| 157 | | erex 8769 |
. . . . . . . . . 10
⊢
({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 → (𝑊 ∈ V → {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ V)) |
| 158 | 25, 156, 157 | mpisyl 21 |
. . . . . . . . 9
⊢ (𝜑 → {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ V) |
| 159 | | ereq1 8752 |
. . . . . . . . . . 11
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (𝑟 Er 𝑊 ↔ {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊)) |
| 160 | | breq 5145 |
. . . . . . . . . . . . 13
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ↔ 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))) |
| 161 | 160 | 2ralbidv 3221 |
. . . . . . . . . . . 12
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ↔
∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))) |
| 162 | 161 | 2ralbidv 3221 |
. . . . . . . . . . 11
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉) ↔
∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))) |
| 163 | 159, 162 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → ((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)) ↔
({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)))) |
| 164 | 163 | elabg 3676 |
. . . . . . . . 9
⊢
({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ V → ({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))} ↔
({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)))) |
| 165 | 158, 164 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))} ↔
({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉)))) |
| 166 | 25, 155, 165 | mpbir2and 713 |
. . . . . . 7
⊢ (𝜑 → {〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))}) |
| 167 | | intss1 4963 |
. . . . . . 7
⊢
({〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))} → ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))} ⊆
{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}) |
| 168 | 166, 167 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∩ {𝑟
∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑎, 𝑏〉〈𝑎, (1o ∖ 𝑏)〉”〉〉))} ⊆
{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}) |
| 169 | 3, 168 | eqsstrid 4022 |
. . . . 5
⊢ (𝜑 → ∼ ⊆
{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}) |
| 170 | 169 | ssbrd 5186 |
. . . 4
⊢ (𝜑 → (𝐴 ∼ 𝐶 → 𝐴{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶)) |
| 171 | 170 | imp 406 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → 𝐴{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶) |
| 172 | 1, 2 | efger 19736 |
. . . . . 6
⊢ ∼ Er
𝑊 |
| 173 | | errel 8754 |
. . . . . 6
⊢ ( ∼ Er
𝑊 → Rel ∼
) |
| 174 | 172, 173 | mp1i 13 |
. . . . 5
⊢ (𝜑 → Rel ∼ ) |
| 175 | | brrelex12 5737 |
. . . . 5
⊢ ((Rel
∼
∧ 𝐴 ∼ 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
| 176 | 174, 175 | sylan 580 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
| 177 | | preq12 4735 |
. . . . . . 7
⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → {𝑢, 𝑣} = {𝐴, 𝐶}) |
| 178 | 177 | sseq1d 4015 |
. . . . . 6
⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ {𝐴, 𝐶} ⊆ 𝑊)) |
| 179 | | coeq2 5869 |
. . . . . . . 8
⊢ (𝑢 = 𝐴 → (𝑇 ∘ 𝑢) = (𝑇 ∘ 𝐴)) |
| 180 | 179 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑢 = 𝐴 → (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝐴))) |
| 181 | | coeq2 5869 |
. . . . . . . 8
⊢ (𝑣 = 𝐶 → (𝑇 ∘ 𝑣) = (𝑇 ∘ 𝐶)) |
| 182 | 181 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑣 = 𝐶 → (𝐻 Σg (𝑇 ∘ 𝑣)) = (𝐻 Σg (𝑇 ∘ 𝐶))) |
| 183 | 180, 182 | eqeqan12d 2751 |
. . . . . 6
⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → ((𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)) ↔ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶)))) |
| 184 | 178, 183 | anbi12d 632 |
. . . . 5
⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))))) |
| 185 | 184, 151 | brabga 5539 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))))) |
| 186 | 176, 185 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐴{〈𝑢, 𝑣〉 ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))))) |
| 187 | 171, 186 | mpbid 232 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶)))) |
| 188 | 187 | simprd 495 |
1
⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))) |