Step | Hyp | Ref
| Expression |
1 | | 2on 7914 |
. . . 4
⊢
2o ∈ On |
2 | | xpexg 7290 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 2o ∈ On) →
(𝐼 × 2o)
∈ V) |
3 | 1, 2 | mpan2 678 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (𝐼 × 2o) ∈
V) |
4 | | frgpmhm.m |
. . . 4
⊢ 𝑀 = (freeMnd‘(𝐼 ×
2o)) |
5 | 4 | frmdmnd 17865 |
. . 3
⊢ ((𝐼 × 2o) ∈ V
→ 𝑀 ∈
Mnd) |
6 | 3, 5 | syl 17 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd) |
7 | | frgpmhm.g |
. . . 4
⊢ 𝐺 = (freeGrp‘𝐼) |
8 | 7 | frgpgrp 18648 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp) |
9 | | grpmnd 17898 |
. . 3
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
10 | 8, 9 | syl 17 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Mnd) |
11 | | frgpmhm.w |
. . . . . . . . . 10
⊢ 𝑊 = (Base‘𝑀) |
12 | 4, 11 | frmdbas 17858 |
. . . . . . . . 9
⊢ ((𝐼 × 2o) ∈ V
→ 𝑊 = Word (𝐼 ×
2o)) |
13 | | wrdexg 13682 |
. . . . . . . . . 10
⊢ ((𝐼 × 2o) ∈ V
→ Word (𝐼 ×
2o) ∈ V) |
14 | | fvi 6568 |
. . . . . . . . . 10
⊢ (Word
(𝐼 × 2o)
∈ V → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 ×
2o)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ ((𝐼 × 2o) ∈ V
→ ( I ‘Word (𝐼
× 2o)) = Word (𝐼 × 2o)) |
16 | 12, 15 | eqtr4d 2817 |
. . . . . . . 8
⊢ ((𝐼 × 2o) ∈ V
→ 𝑊 = ( I ‘Word
(𝐼 ×
2o))) |
17 | 3, 16 | syl 17 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → 𝑊 = ( I ‘Word (𝐼 × 2o))) |
18 | 17 | eleq2d 2851 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ( I ‘Word (𝐼 × 2o)))) |
19 | 18 | biimpa 469 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊) → 𝑥 ∈ ( I ‘Word (𝐼 × 2o))) |
20 | | frgpmhm.r |
. . . . . 6
⊢ ∼ = (
~FG ‘𝐼) |
21 | | eqid 2778 |
. . . . . 6
⊢ ( I
‘Word (𝐼 ×
2o)) = ( I ‘Word (𝐼 × 2o)) |
22 | | eqid 2778 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
23 | 7, 20, 21, 22 | frgpeccl 18647 |
. . . . 5
⊢ (𝑥 ∈ ( I ‘Word (𝐼 × 2o)) →
[𝑥] ∼ ∈
(Base‘𝐺)) |
24 | 19, 23 | syl 17 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊) → [𝑥] ∼ ∈
(Base‘𝐺)) |
25 | | frgpmhm.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑊 ↦ [𝑥] ∼ ) |
26 | 24, 25 | fmptd 6701 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐹:𝑊⟶(Base‘𝐺)) |
27 | 21, 20 | efger 18602 |
. . . . . . . 8
⊢ ∼ Er ( I
‘Word (𝐼 ×
2o)) |
28 | | ereq2 8097 |
. . . . . . . . 9
⊢ (𝑊 = ( I ‘Word (𝐼 × 2o)) →
( ∼ Er 𝑊 ↔ ∼ Er ( I ‘Word
(𝐼 ×
2o)))) |
29 | 17, 28 | syl 17 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → ( ∼ Er 𝑊 ↔ ∼ Er ( I ‘Word
(𝐼 ×
2o)))) |
30 | 27, 29 | mpbiri 250 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → ∼ Er 𝑊) |
31 | 30 | adantr 473 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ∼ Er 𝑊) |
32 | 11 | fvexi 6513 |
. . . . . . 7
⊢ 𝑊 ∈ V |
33 | 32 | a1i 11 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → 𝑊 ∈ V) |
34 | 31, 33, 25 | divsfval 16676 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘(𝑎 ++ 𝑏)) = [(𝑎 ++ 𝑏)] ∼ ) |
35 | | eqid 2778 |
. . . . . . . 8
⊢
(+g‘𝑀) = (+g‘𝑀) |
36 | 4, 11, 35 | frmdadd 17861 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ++ 𝑏)) |
37 | 36 | adantl 474 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ++ 𝑏)) |
38 | 37 | fveq2d 6503 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘(𝑎(+g‘𝑀)𝑏)) = (𝐹‘(𝑎 ++ 𝑏))) |
39 | 31, 33, 25 | divsfval 16676 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘𝑎) = [𝑎] ∼ ) |
40 | 31, 33, 25 | divsfval 16676 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘𝑏) = [𝑏] ∼ ) |
41 | 39, 40 | oveq12d 6994 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) = ([𝑎] ∼
(+g‘𝐺)[𝑏] ∼ )) |
42 | 17 | eleq2d 2851 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (𝑎 ∈ 𝑊 ↔ 𝑎 ∈ ( I ‘Word (𝐼 × 2o)))) |
43 | 17 | eleq2d 2851 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (𝑏 ∈ 𝑊 ↔ 𝑏 ∈ ( I ‘Word (𝐼 × 2o)))) |
44 | 42, 43 | anbi12d 621 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ↔ (𝑎 ∈ ( I ‘Word (𝐼 × 2o)) ∧ 𝑏 ∈ ( I ‘Word (𝐼 ×
2o))))) |
45 | 44 | biimpa 469 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝑎 ∈ ( I ‘Word (𝐼 × 2o)) ∧ 𝑏 ∈ ( I ‘Word (𝐼 ×
2o)))) |
46 | | eqid 2778 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
47 | 21, 7, 20, 46 | frgpadd 18649 |
. . . . . . 7
⊢ ((𝑎 ∈ ( I ‘Word (𝐼 × 2o)) ∧
𝑏 ∈ ( I ‘Word
(𝐼 × 2o)))
→ ([𝑎] ∼
(+g‘𝐺)[𝑏] ∼ ) = [(𝑎 ++ 𝑏)] ∼ ) |
48 | 45, 47 | syl 17 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ([𝑎] ∼
(+g‘𝐺)[𝑏] ∼ ) = [(𝑎 ++ 𝑏)] ∼ ) |
49 | 41, 48 | eqtrd 2814 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) = [(𝑎 ++ 𝑏)] ∼ ) |
50 | 34, 38, 49 | 3eqtr4d 2824 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏))) |
51 | 50 | ralrimivva 3141 |
. . 3
⊢ (𝐼 ∈ 𝑉 → ∀𝑎 ∈ 𝑊 ∀𝑏 ∈ 𝑊 (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏))) |
52 | 32 | a1i 11 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → 𝑊 ∈ V) |
53 | 30, 52, 25 | divsfval 16676 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → (𝐹‘∅) = [∅] ∼
) |
54 | 7, 20 | frgp0 18646 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (𝐺 ∈ Grp ∧ [∅] ∼ =
(0g‘𝐺))) |
55 | 54 | simprd 488 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → [∅] ∼ =
(0g‘𝐺)) |
56 | 53, 55 | eqtrd 2814 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (𝐹‘∅) = (0g‘𝐺)) |
57 | 26, 51, 56 | 3jca 1108 |
. 2
⊢ (𝐼 ∈ 𝑉 → (𝐹:𝑊⟶(Base‘𝐺) ∧ ∀𝑎 ∈ 𝑊 ∀𝑏 ∈ 𝑊 (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) ∧ (𝐹‘∅) = (0g‘𝐺))) |
58 | 4 | frmd0 17866 |
. . 3
⊢ ∅ =
(0g‘𝑀) |
59 | | eqid 2778 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
60 | 11, 22, 35, 46, 58, 59 | ismhm 17805 |
. 2
⊢ (𝐹 ∈ (𝑀 MndHom 𝐺) ↔ ((𝑀 ∈ Mnd ∧ 𝐺 ∈ Mnd) ∧ (𝐹:𝑊⟶(Base‘𝐺) ∧ ∀𝑎 ∈ 𝑊 ∀𝑏 ∈ 𝑊 (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) ∧ (𝐹‘∅) = (0g‘𝐺)))) |
61 | 6, 10, 57, 60 | syl21anbrc 1324 |
1
⊢ (𝐼 ∈ 𝑉 → 𝐹 ∈ (𝑀 MndHom 𝐺)) |