| Step | Hyp | Ref
| Expression |
| 1 | | frgp0.m |
. . 3
⊢ 𝐺 = (freeGrp‘𝐼) |
| 2 | | eqid 2737 |
. . 3
⊢
(freeMnd‘(𝐼
× 2o)) = (freeMnd‘(𝐼 × 2o)) |
| 3 | | frgp0.r |
. . 3
⊢ ∼ = (
~FG ‘𝐼) |
| 4 | 1, 2, 3 | frgpval 19776 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝐺 = ((freeMnd‘(𝐼 × 2o))
/s ∼ )) |
| 5 | | 2on 8520 |
. . . . 5
⊢
2o ∈ On |
| 6 | | xpexg 7770 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 2o ∈ On) →
(𝐼 × 2o)
∈ V) |
| 7 | 5, 6 | mpan2 691 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → (𝐼 × 2o) ∈
V) |
| 8 | | eqid 2737 |
. . . . 5
⊢
(Base‘(freeMnd‘(𝐼 × 2o))) =
(Base‘(freeMnd‘(𝐼 × 2o))) |
| 9 | 2, 8 | frmdbas 18865 |
. . . 4
⊢ ((𝐼 × 2o) ∈ V
→ (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 ×
2o)) |
| 10 | 7, 9 | syl 17 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (Base‘(freeMnd‘(𝐼 × 2o))) = Word
(𝐼 ×
2o)) |
| 11 | 10 | eqcomd 2743 |
. 2
⊢ (𝐼 ∈ 𝑉 → Word (𝐼 × 2o) =
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 12 | | eqidd 2738 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(+g‘(freeMnd‘(𝐼 × 2o))) =
(+g‘(freeMnd‘(𝐼 × 2o)))) |
| 13 | | eqid 2737 |
. . . 4
⊢ ( I
‘Word (𝐼 ×
2o)) = ( I ‘Word (𝐼 × 2o)) |
| 14 | 13, 3 | efger 19736 |
. . 3
⊢ ∼ Er ( I
‘Word (𝐼 ×
2o)) |
| 15 | | wrdexg 14562 |
. . . . 5
⊢ ((𝐼 × 2o) ∈ V
→ Word (𝐼 ×
2o) ∈ V) |
| 16 | | fvi 6985 |
. . . . 5
⊢ (Word
(𝐼 × 2o)
∈ V → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 ×
2o)) |
| 17 | 7, 15, 16 | 3syl 18 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 ×
2o)) |
| 18 | | ereq2 8753 |
. . . 4
⊢ (( I
‘Word (𝐼 ×
2o)) = Word (𝐼
× 2o) → ( ∼ Er ( I ‘Word
(𝐼 × 2o))
↔ ∼ Er Word (𝐼 ×
2o))) |
| 19 | 17, 18 | syl 17 |
. . 3
⊢ (𝐼 ∈ 𝑉 → ( ∼ Er ( I ‘Word
(𝐼 × 2o))
↔ ∼ Er Word (𝐼 ×
2o))) |
| 20 | 14, 19 | mpbii 233 |
. 2
⊢ (𝐼 ∈ 𝑉 → ∼ Er Word (𝐼 ×
2o)) |
| 21 | | fvexd 6921 |
. 2
⊢ (𝐼 ∈ 𝑉 → (freeMnd‘(𝐼 × 2o)) ∈
V) |
| 22 | | eqid 2737 |
. . . 4
⊢
(+g‘(freeMnd‘(𝐼 × 2o))) =
(+g‘(freeMnd‘(𝐼 × 2o))) |
| 23 | 1, 2, 3, 22 | frgpcpbl 19777 |
. . 3
⊢ ((𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑) → (𝑎(+g‘(freeMnd‘(𝐼 × 2o)))𝑐) ∼ (𝑏(+g‘(freeMnd‘(𝐼 × 2o)))𝑑)) |
| 24 | 23 | a1i 11 |
. 2
⊢ (𝐼 ∈ 𝑉 → ((𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑) → (𝑎(+g‘(freeMnd‘(𝐼 × 2o)))𝑐) ∼ (𝑏(+g‘(freeMnd‘(𝐼 × 2o)))𝑑))) |
| 25 | 2 | frmdmnd 18872 |
. . . . . 6
⊢ ((𝐼 × 2o) ∈ V
→ (freeMnd‘(𝐼
× 2o)) ∈ Mnd) |
| 26 | 7, 25 | syl 17 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (freeMnd‘(𝐼 × 2o)) ∈
Mnd) |
| 27 | 26 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o)) →
(freeMnd‘(𝐼 ×
2o)) ∈ Mnd) |
| 28 | | simp2 1138 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o)) → 𝑥 ∈ Word (𝐼 × 2o)) |
| 29 | 11 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o)) → Word (𝐼 × 2o) =
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 30 | 28, 29 | eleqtrd 2843 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o)) → 𝑥 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 31 | | simp3 1139 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o)) → 𝑦 ∈ Word (𝐼 × 2o)) |
| 32 | 31, 29 | eleqtrd 2843 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o)) → 𝑦 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 33 | 8, 22 | mndcl 18755 |
. . . 4
⊢
(((freeMnd‘(𝐼
× 2o)) ∈ Mnd ∧ 𝑥 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ∧
𝑦 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) → (𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦) ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 34 | 27, 30, 32, 33 | syl3anc 1373 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o)) → (𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦) ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 35 | 34, 29 | eleqtrrd 2844 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o)) → (𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦) ∈ Word (𝐼 × 2o)) |
| 36 | 20 | adantr 480 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → ∼ Er
Word (𝐼 ×
2o)) |
| 37 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) →
(freeMnd‘(𝐼 ×
2o)) ∈ Mnd) |
| 38 | 34 | 3adant3r3 1185 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → (𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦) ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 39 | | simpr3 1197 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → 𝑧 ∈ Word (𝐼 × 2o)) |
| 40 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → Word (𝐼 × 2o) =
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 41 | 39, 40 | eleqtrd 2843 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → 𝑧 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 42 | 8, 22 | mndcl 18755 |
. . . . . 6
⊢
(((freeMnd‘(𝐼
× 2o)) ∈ Mnd ∧ (𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦) ∈
(Base‘(freeMnd‘(𝐼 × 2o))) ∧ 𝑧 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦)(+g‘(freeMnd‘(𝐼 × 2o)))𝑧) ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 43 | 37, 38, 41, 42 | syl3anc 1373 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦)(+g‘(freeMnd‘(𝐼 × 2o)))𝑧) ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 44 | 43, 40 | eleqtrrd 2844 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦)(+g‘(freeMnd‘(𝐼 × 2o)))𝑧) ∈ Word (𝐼 × 2o)) |
| 45 | 36, 44 | erref 8765 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦)(+g‘(freeMnd‘(𝐼 × 2o)))𝑧) ∼ ((𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦)(+g‘(freeMnd‘(𝐼 × 2o)))𝑧)) |
| 46 | 30 | 3adant3r3 1185 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → 𝑥 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 47 | 32 | 3adant3r3 1185 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → 𝑦 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 48 | 8, 22 | mndass 18756 |
. . . 4
⊢
(((freeMnd‘(𝐼
× 2o)) ∈ Mnd ∧ (𝑥 ∈ (Base‘(freeMnd‘(𝐼 × 2o))) ∧
𝑦 ∈
(Base‘(freeMnd‘(𝐼 × 2o))) ∧ 𝑧 ∈
(Base‘(freeMnd‘(𝐼 × 2o))))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦)(+g‘(freeMnd‘(𝐼 × 2o)))𝑧) = (𝑥(+g‘(freeMnd‘(𝐼 × 2o)))(𝑦(+g‘(freeMnd‘(𝐼 × 2o)))𝑧))) |
| 49 | 37, 46, 47, 41, 48 | syl13anc 1374 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦)(+g‘(freeMnd‘(𝐼 × 2o)))𝑧) = (𝑥(+g‘(freeMnd‘(𝐼 × 2o)))(𝑦(+g‘(freeMnd‘(𝐼 × 2o)))𝑧))) |
| 50 | 45, 49 | breqtrd 5169 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑦 ∈ Word (𝐼 × 2o) ∧ 𝑧 ∈ Word (𝐼 × 2o))) → ((𝑥(+g‘(freeMnd‘(𝐼 × 2o)))𝑦)(+g‘(freeMnd‘(𝐼 × 2o)))𝑧) ∼ (𝑥(+g‘(freeMnd‘(𝐼 × 2o)))(𝑦(+g‘(freeMnd‘(𝐼 × 2o)))𝑧))) |
| 51 | | wrd0 14577 |
. . 3
⊢ ∅
∈ Word (𝐼 ×
2o) |
| 52 | 51 | a1i 11 |
. 2
⊢ (𝐼 ∈ 𝑉 → ∅ ∈ Word (𝐼 ×
2o)) |
| 53 | 51, 11 | eleqtrid 2847 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → ∅ ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 54 | 53 | adantr 480 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → ∅
∈ (Base‘(freeMnd‘(𝐼 × 2o)))) |
| 55 | 11 | eleq2d 2827 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ Word (𝐼 × 2o) ↔ 𝑥 ∈
(Base‘(freeMnd‘(𝐼 × 2o))))) |
| 56 | 55 | biimpa 476 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → 𝑥 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 57 | 2, 8, 22 | frmdadd 18868 |
. . . . 5
⊢ ((∅
∈ (Base‘(freeMnd‘(𝐼 × 2o))) ∧ 𝑥 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) →
(∅(+g‘(freeMnd‘(𝐼 × 2o)))𝑥) = (∅ ++ 𝑥)) |
| 58 | 54, 56, 57 | syl2anc 584 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) →
(∅(+g‘(freeMnd‘(𝐼 × 2o)))𝑥) = (∅ ++ 𝑥)) |
| 59 | | ccatlid 14624 |
. . . . 5
⊢ (𝑥 ∈ Word (𝐼 × 2o) → (∅ ++
𝑥) = 𝑥) |
| 60 | 59 | adantl 481 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → (∅ ++
𝑥) = 𝑥) |
| 61 | 58, 60 | eqtrd 2777 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) →
(∅(+g‘(freeMnd‘(𝐼 × 2o)))𝑥) = 𝑥) |
| 62 | 20 | adantr 480 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → ∼ Er
Word (𝐼 ×
2o)) |
| 63 | | simpr 484 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → 𝑥 ∈ Word (𝐼 × 2o)) |
| 64 | 62, 63 | erref 8765 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → 𝑥 ∼ 𝑥) |
| 65 | 61, 64 | eqbrtrd 5165 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) →
(∅(+g‘(freeMnd‘(𝐼 × 2o)))𝑥) ∼ 𝑥) |
| 66 | | revcl 14799 |
. . . 4
⊢ (𝑥 ∈ Word (𝐼 × 2o) →
(reverse‘𝑥) ∈
Word (𝐼 ×
2o)) |
| 67 | 66 | adantl 481 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) →
(reverse‘𝑥) ∈
Word (𝐼 ×
2o)) |
| 68 | | eqid 2737 |
. . . . 5
⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) |
| 69 | 68 | efgmf 19731 |
. . . 4
⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉):(𝐼 × 2o)⟶(𝐼 ×
2o) |
| 70 | 69 | a1i 11 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉):(𝐼 × 2o)⟶(𝐼 ×
2o)) |
| 71 | | wrdco 14870 |
. . 3
⊢
(((reverse‘𝑥)
∈ Word (𝐼 ×
2o) ∧ (𝑦
∈ 𝐼, 𝑧 ∈ 2o ↦
〈𝑦, (1o
∖ 𝑧)〉):(𝐼 ×
2o)⟶(𝐼
× 2o)) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥)) ∈
Word (𝐼 ×
2o)) |
| 72 | 67, 70, 71 | syl2anc 584 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥)) ∈
Word (𝐼 ×
2o)) |
| 73 | 11 | adantr 480 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → Word (𝐼 × 2o) =
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 74 | 72, 73 | eleqtrd 2843 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥)) ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) |
| 75 | 2, 8, 22 | frmdadd 18868 |
. . . 4
⊢ ((((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥)) ∈
(Base‘(freeMnd‘(𝐼 × 2o))) ∧ 𝑥 ∈
(Base‘(freeMnd‘(𝐼 × 2o)))) → (((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥))(+g‘(freeMnd‘(𝐼 × 2o)))𝑥) = (((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥)) ++ 𝑥)) |
| 76 | 74, 56, 75 | syl2anc 584 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → (((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥))(+g‘(freeMnd‘(𝐼 × 2o)))𝑥) = (((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥)) ++ 𝑥)) |
| 77 | 17 | eleq2d 2827 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ ( I ‘Word (𝐼 × 2o)) ↔ 𝑥 ∈ Word (𝐼 × 2o))) |
| 78 | 77 | biimpar 477 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → 𝑥 ∈ ( I ‘Word (𝐼 ×
2o))) |
| 79 | | eqid 2737 |
. . . . 5
⊢ (𝑣 ∈ ( I ‘Word (𝐼 × 2o)) ↦
(𝑛 ∈
(0...(♯‘𝑣)),
𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)‘𝑤)”〉〉))) = (𝑣 ∈ ( I ‘Word (𝐼 × 2o)) ↦
(𝑛 ∈
(0...(♯‘𝑣)),
𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉)‘𝑤)”〉〉))) |
| 80 | 13, 3, 68, 79 | efginvrel1 19746 |
. . . 4
⊢ (𝑥 ∈ ( I ‘Word (𝐼 × 2o)) →
(((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥)) ++ 𝑥) ∼
∅) |
| 81 | 78, 80 | syl 17 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → (((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥)) ++ 𝑥) ∼
∅) |
| 82 | 76, 81 | eqbrtrd 5165 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2o)) → (((𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ∘
(reverse‘𝑥))(+g‘(freeMnd‘(𝐼 × 2o)))𝑥) ∼
∅) |
| 83 | 4, 11, 12, 20, 21, 24, 35, 50, 52, 65, 72, 82 | qusgrp2 19076 |
1
⊢ (𝐼 ∈ 𝑉 → (𝐺 ∈ Grp ∧ [∅] ∼ =
(0g‘𝐺))) |