Step | Hyp | Ref
| Expression |
1 | | 2on 7568 |
. . . . 5
⊢
2𝑜 ∈ On |
2 | | xpexg 6960 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 2𝑜 ∈ On)
→ (𝐼 ×
2𝑜) ∈ V) |
3 | 1, 2 | mpan2 707 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → (𝐼 × 2𝑜) ∈
V) |
4 | | frgpmhm.m |
. . . . 5
⊢ 𝑀 = (freeMnd‘(𝐼 ×
2𝑜)) |
5 | 4 | frmdmnd 17396 |
. . . 4
⊢ ((𝐼 × 2𝑜)
∈ V → 𝑀 ∈
Mnd) |
6 | 3, 5 | syl 17 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd) |
7 | | frgpmhm.g |
. . . . 5
⊢ 𝐺 = (freeGrp‘𝐼) |
8 | 7 | frgpgrp 18175 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp) |
9 | | grpmnd 17429 |
. . . 4
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Mnd) |
11 | 6, 10 | jca 554 |
. 2
⊢ (𝐼 ∈ 𝑉 → (𝑀 ∈ Mnd ∧ 𝐺 ∈ Mnd)) |
12 | | frgpmhm.w |
. . . . . . . . . 10
⊢ 𝑊 = (Base‘𝑀) |
13 | 4, 12 | frmdbas 17389 |
. . . . . . . . 9
⊢ ((𝐼 × 2𝑜)
∈ V → 𝑊 = Word
(𝐼 ×
2𝑜)) |
14 | | wrdexg 13315 |
. . . . . . . . . 10
⊢ ((𝐼 × 2𝑜)
∈ V → Word (𝐼
× 2𝑜) ∈ V) |
15 | | fvi 6255 |
. . . . . . . . . 10
⊢ (Word
(𝐼 ×
2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word
(𝐼 ×
2𝑜)) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ ((𝐼 × 2𝑜)
∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word
(𝐼 ×
2𝑜)) |
17 | 13, 16 | eqtr4d 2659 |
. . . . . . . 8
⊢ ((𝐼 × 2𝑜)
∈ V → 𝑊 = ( I
‘Word (𝐼 ×
2𝑜))) |
18 | 3, 17 | syl 17 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → 𝑊 = ( I ‘Word (𝐼 ×
2𝑜))) |
19 | 18 | eleq2d 2687 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ( I ‘Word (𝐼 ×
2𝑜)))) |
20 | 19 | biimpa 501 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊) → 𝑥 ∈ ( I ‘Word (𝐼 ×
2𝑜))) |
21 | | frgpmhm.r |
. . . . . 6
⊢ ∼ = (
~FG ‘𝐼) |
22 | | eqid 2622 |
. . . . . 6
⊢ ( I
‘Word (𝐼 ×
2𝑜)) = ( I ‘Word (𝐼 ×
2𝑜)) |
23 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
24 | 7, 21, 22, 23 | frgpeccl 18174 |
. . . . 5
⊢ (𝑥 ∈ ( I ‘Word (𝐼 × 2𝑜))
→ [𝑥] ∼ ∈
(Base‘𝐺)) |
25 | 20, 24 | syl 17 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊) → [𝑥] ∼ ∈
(Base‘𝐺)) |
26 | | frgpmhm.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑊 ↦ [𝑥] ∼ ) |
27 | 25, 26 | fmptd 6385 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐹:𝑊⟶(Base‘𝐺)) |
28 | 22, 21 | efger 18131 |
. . . . . . . 8
⊢ ∼ Er ( I
‘Word (𝐼 ×
2𝑜)) |
29 | | ereq2 7750 |
. . . . . . . . 9
⊢ (𝑊 = ( I ‘Word (𝐼 × 2𝑜))
→ ( ∼ Er 𝑊 ↔ ∼ Er ( I ‘Word
(𝐼 ×
2𝑜)))) |
30 | 18, 29 | syl 17 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → ( ∼ Er 𝑊 ↔ ∼ Er ( I ‘Word
(𝐼 ×
2𝑜)))) |
31 | 28, 30 | mpbiri 248 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → ∼ Er 𝑊) |
32 | 31 | adantr 481 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ∼ Er 𝑊) |
33 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝑀)
∈ V |
34 | 12, 33 | eqeltri 2697 |
. . . . . . 7
⊢ 𝑊 ∈ V |
35 | 34 | a1i 11 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → 𝑊 ∈ V) |
36 | 32, 35, 26 | divsfval 16207 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘(𝑎 ++ 𝑏)) = [(𝑎 ++ 𝑏)] ∼ ) |
37 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘𝑀) = (+g‘𝑀) |
38 | 4, 12, 37 | frmdadd 17392 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ++ 𝑏)) |
39 | 38 | adantl 482 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ++ 𝑏)) |
40 | 39 | fveq2d 6195 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘(𝑎(+g‘𝑀)𝑏)) = (𝐹‘(𝑎 ++ 𝑏))) |
41 | 32, 35, 26 | divsfval 16207 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘𝑎) = [𝑎] ∼ ) |
42 | 32, 35, 26 | divsfval 16207 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘𝑏) = [𝑏] ∼ ) |
43 | 41, 42 | oveq12d 6668 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) = ([𝑎] ∼
(+g‘𝐺)[𝑏] ∼ )) |
44 | 18 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (𝑎 ∈ 𝑊 ↔ 𝑎 ∈ ( I ‘Word (𝐼 ×
2𝑜)))) |
45 | 18 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (𝑏 ∈ 𝑊 ↔ 𝑏 ∈ ( I ‘Word (𝐼 ×
2𝑜)))) |
46 | 44, 45 | anbi12d 747 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ↔ (𝑎 ∈ ( I ‘Word (𝐼 × 2𝑜)) ∧ 𝑏 ∈ ( I ‘Word (𝐼 ×
2𝑜))))) |
47 | 46 | biimpa 501 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝑎 ∈ ( I ‘Word (𝐼 × 2𝑜)) ∧ 𝑏 ∈ ( I ‘Word (𝐼 ×
2𝑜)))) |
48 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
49 | 22, 7, 21, 48 | frgpadd 18176 |
. . . . . . 7
⊢ ((𝑎 ∈ ( I ‘Word (𝐼 × 2𝑜))
∧ 𝑏 ∈ ( I
‘Word (𝐼 ×
2𝑜))) → ([𝑎] ∼
(+g‘𝐺)[𝑏] ∼ ) = [(𝑎 ++ 𝑏)] ∼ ) |
50 | 47, 49 | syl 17 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ([𝑎] ∼
(+g‘𝐺)[𝑏] ∼ ) = [(𝑎 ++ 𝑏)] ∼ ) |
51 | 43, 50 | eqtrd 2656 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) = [(𝑎 ++ 𝑏)] ∼ ) |
52 | 36, 40, 51 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏))) |
53 | 52 | ralrimivva 2971 |
. . 3
⊢ (𝐼 ∈ 𝑉 → ∀𝑎 ∈ 𝑊 ∀𝑏 ∈ 𝑊 (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏))) |
54 | 34 | a1i 11 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → 𝑊 ∈ V) |
55 | 31, 54, 26 | divsfval 16207 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → (𝐹‘∅) = [∅] ∼
) |
56 | 7, 21 | frgp0 18173 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (𝐺 ∈ Grp ∧ [∅] ∼ =
(0g‘𝐺))) |
57 | 56 | simprd 479 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → [∅] ∼ =
(0g‘𝐺)) |
58 | 55, 57 | eqtrd 2656 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (𝐹‘∅) = (0g‘𝐺)) |
59 | 27, 53, 58 | 3jca 1242 |
. 2
⊢ (𝐼 ∈ 𝑉 → (𝐹:𝑊⟶(Base‘𝐺) ∧ ∀𝑎 ∈ 𝑊 ∀𝑏 ∈ 𝑊 (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) ∧ (𝐹‘∅) = (0g‘𝐺))) |
60 | 4 | frmd0 17397 |
. . 3
⊢ ∅ =
(0g‘𝑀) |
61 | | eqid 2622 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
62 | 12, 23, 37, 48, 60, 61 | ismhm 17337 |
. 2
⊢ (𝐹 ∈ (𝑀 MndHom 𝐺) ↔ ((𝑀 ∈ Mnd ∧ 𝐺 ∈ Mnd) ∧ (𝐹:𝑊⟶(Base‘𝐺) ∧ ∀𝑎 ∈ 𝑊 ∀𝑏 ∈ 𝑊 (𝐹‘(𝑎(+g‘𝑀)𝑏)) = ((𝐹‘𝑎)(+g‘𝐺)(𝐹‘𝑏)) ∧ (𝐹‘∅) = (0g‘𝐺)))) |
63 | 11, 59, 62 | sylanbrc 698 |
1
⊢ (𝐼 ∈ 𝑉 → 𝐹 ∈ (𝑀 MndHom 𝐺)) |