Step | Hyp | Ref
| Expression |
1 | | 2on 8311 |
. . . 4
⊢
2o ∈ On |
2 | | xpexg 7600 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 2o ∈ On) →
(𝐼 × 2o)
∈ V) |
3 | 1, 2 | mpan2 688 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (𝐼 × 2o) ∈
V) |
4 | | frgpmhm.m |
. . . 4
⊢ 𝑀 = (freeMnd‘(𝐼 ×
2o)) |
5 | 4 | frmdmnd 18498 |
. . 3
⊢ ((𝐼 × 2o) ∈ V
→ 𝑀 ∈
Mnd) |
6 | 3, 5 | syl 17 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd) |
7 | | frgpmhm.g |
. . . 4
⊢ 𝐺 = (freeGrp‘𝐼) |
8 | 7 | frgpgrp 19368 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp) |
9 | 8 | grpmndd 18589 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Mnd) |
10 | | frgpmhm.w |
. . . . . . . . . 10
⊢ 𝑊 = (Base‘𝑀) |
11 | 4, 10 | frmdbas 18491 |
. . . . . . . . 9
⊢ ((𝐼 × 2o) ∈ V
→ 𝑊 = Word (𝐼 ×
2o)) |
12 | | wrdexg 14227 |
. . . . . . . . . 10
⊢ ((𝐼 × 2o) ∈ V
→ Word (𝐼 ×
2o) ∈ V) |
13 | | fvi 6844 |
. . . . . . . . . 10
⊢ (Word
(𝐼 × 2o)
∈ V → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 ×
2o)) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ ((𝐼 × 2o) ∈ V
→ ( I ‘Word (𝐼
× 2o)) = Word (𝐼 × 2o)) |
15 | 11, 14 | eqtr4d 2781 |
. . . . . . . 8
⊢ ((𝐼 × 2o) ∈ V
→ 𝑊 = ( I ‘Word
(𝐼 ×
2o))) |
16 | 3, 15 | syl 17 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → 𝑊 = ( I ‘Word (𝐼 × 2o))) |
17 | 16 | eleq2d 2824 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ( I ‘Word (𝐼 × 2o)))) |
18 | 17 | biimpa 477 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊) → 𝑥 ∈ ( I ‘Word (𝐼 × 2o))) |
19 | | frgpmhm.r |
. . . . . 6
⊢ ∼ = (
~FG ‘𝐼) |
20 | | eqid 2738 |
. . . . . 6
⊢ ( I
‘Word (𝐼 ×
2o)) = ( I ‘Word (𝐼 × 2o)) |
21 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
22 | 7, 19, 20, 21 | frgpeccl 19367 |
. . . . 5
⊢ (𝑥 ∈ ( I ‘Word (𝐼 × 2o)) →
[𝑥] ∼ ∈
(Base‘𝐺)) |
23 | 18, 22 | syl 17 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊) → [𝑥] ∼ ∈
(Base‘𝐺)) |
24 | | frgpmhm.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑊 ↦ [𝑥] ∼ ) |
25 | 23, 24 | fmptd 6988 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐹:𝑊⟶(Base‘𝐺)) |
26 | 20, 19 | efger 19324 |
. . . . . . . 8
⊢ ∼ Er ( I
‘Word (𝐼 ×
2o)) |
27 | | ereq2 8506 |
. . . . . . . . 9
⊢ (𝑊 = ( I ‘Word (𝐼 × 2o)) →
( ∼ Er 𝑊 ↔ ∼ Er ( I ‘Word
(𝐼 ×
2o)))) |
28 | 16, 27 | syl 17 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → ( ∼ Er 𝑊 ↔ ∼ Er ( I ‘Word
(𝐼 ×
2o)))) |
29 | 26, 28 | mpbiri 257 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → ∼ Er 𝑊) |
30 | 29 | adantr 481 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ∼ Er 𝑊) |
31 | 10 | fvexi 6788 |
. . . . . . 7
⊢ 𝑊 ∈ V |
32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → 𝑊 ∈ V) |
33 | 30, 32, 24 | divsfval 17258 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘(𝑎 ++ 𝑏)) = [(𝑎 ++ 𝑏)] ∼ ) |
34 | | eqid 2738 |
. . . . . . . 8
⊢
(+g‘𝑀) = (+g‘𝑀) |
35 | 4, 10, 34 | frmdadd 18494 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ++ 𝑏)) |
36 | 35 | adantl 482 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ++ 𝑏)) |
37 | 36 | fveq2d 6778 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘(𝑎(+g‘𝑀)𝑏)) = (𝐹‘(𝑎 ++ 𝑏))) |
38 | 30, 32, 24 | divsfval 17258 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘𝑎) = [𝑎] ∼ ) |
39 | 30, 32, 24 | divsfval 17258 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘𝑏) = [𝑏] ∼ ) |
40 | 38, 39 | oveq12d 7293 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) = ([𝑎] ∼
(+g‘𝐺)[𝑏] ∼ )) |
41 | 16 | eleq2d 2824 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (𝑎 ∈ 𝑊 ↔ 𝑎 ∈ ( I ‘Word (𝐼 × 2o)))) |
42 | 16 | eleq2d 2824 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (𝑏 ∈ 𝑊 ↔ 𝑏 ∈ ( I ‘Word (𝐼 × 2o)))) |
43 | 41, 42 | anbi12d 631 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ↔ (𝑎 ∈ ( I ‘Word (𝐼 × 2o)) ∧ 𝑏 ∈ ( I ‘Word (𝐼 ×
2o))))) |
44 | 43 | biimpa 477 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝑎 ∈ ( I ‘Word (𝐼 × 2o)) ∧ 𝑏 ∈ ( I ‘Word (𝐼 ×
2o)))) |
45 | | eqid 2738 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
46 | 20, 7, 19, 45 | frgpadd 19369 |
. . . . . . 7
⊢ ((𝑎 ∈ ( I ‘Word (𝐼 × 2o)) ∧
𝑏 ∈ ( I ‘Word
(𝐼 × 2o)))
→ ([𝑎] ∼
(+g‘𝐺)[𝑏] ∼ ) = [(𝑎 ++ 𝑏)] ∼ ) |
47 | 44, 46 | syl 17 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ([𝑎] ∼
(+g‘𝐺)[𝑏] ∼ ) = [(𝑎 ++ 𝑏)] ∼ ) |
48 | 40, 47 | eqtrd 2778 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) = [(𝑎 ++ 𝑏)] ∼ ) |
49 | 33, 37, 48 | 3eqtr4d 2788 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏))) |
50 | 49 | ralrimivva 3123 |
. . 3
⊢ (𝐼 ∈ 𝑉 → ∀𝑎 ∈ 𝑊 ∀𝑏 ∈ 𝑊 (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏))) |
51 | 31 | a1i 11 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → 𝑊 ∈ V) |
52 | 29, 51, 24 | divsfval 17258 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → (𝐹‘∅) = [∅] ∼
) |
53 | 7, 19 | frgp0 19366 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (𝐺 ∈ Grp ∧ [∅] ∼ =
(0g‘𝐺))) |
54 | 53 | simprd 496 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → [∅] ∼ =
(0g‘𝐺)) |
55 | 52, 54 | eqtrd 2778 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (𝐹‘∅) = (0g‘𝐺)) |
56 | 25, 50, 55 | 3jca 1127 |
. 2
⊢ (𝐼 ∈ 𝑉 → (𝐹:𝑊⟶(Base‘𝐺) ∧ ∀𝑎 ∈ 𝑊 ∀𝑏 ∈ 𝑊 (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) ∧ (𝐹‘∅) = (0g‘𝐺))) |
57 | 4 | frmd0 18499 |
. . 3
⊢ ∅ =
(0g‘𝑀) |
58 | | eqid 2738 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
59 | 10, 21, 34, 45, 57, 58 | ismhm 18432 |
. 2
⊢ (𝐹 ∈ (𝑀 MndHom 𝐺) ↔ ((𝑀 ∈ Mnd ∧ 𝐺 ∈ Mnd) ∧ (𝐹:𝑊⟶(Base‘𝐺) ∧ ∀𝑎 ∈ 𝑊 ∀𝑏 ∈ 𝑊 (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) ∧ (𝐹‘∅) = (0g‘𝐺)))) |
60 | 6, 9, 56, 59 | syl21anbrc 1343 |
1
⊢ (𝐼 ∈ 𝑉 → 𝐹 ∈ (𝑀 MndHom 𝐺)) |