Step | Hyp | Ref
| Expression |
1 | | frgpup.x |
. 2
⊢ 𝑋 = (Base‘𝐺) |
2 | | frgpup.b |
. 2
⊢ 𝐵 = (Base‘𝐻) |
3 | | eqid 2737 |
. 2
⊢
(+g‘𝐺) = (+g‘𝐺) |
4 | | eqid 2737 |
. 2
⊢
(+g‘𝐻) = (+g‘𝐻) |
5 | | frgpup.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
6 | | frgpup.g |
. . . 4
⊢ 𝐺 = (freeGrp‘𝐼) |
7 | 6 | frgpgrp 19468 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp) |
8 | 5, 7 | syl 17 |
. 2
⊢ (𝜑 → 𝐺 ∈ Grp) |
9 | | frgpup.h |
. 2
⊢ (𝜑 → 𝐻 ∈ Grp) |
10 | | frgpup.n |
. . 3
⊢ 𝑁 = (invg‘𝐻) |
11 | | frgpup.t |
. . 3
⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) |
12 | | frgpup.a |
. . 3
⊢ (𝜑 → 𝐹:𝐼⟶𝐵) |
13 | | frgpup.w |
. . 3
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) |
14 | | frgpup.r |
. . 3
⊢ ∼ = (
~FG ‘𝐼) |
15 | | frgpup.e |
. . 3
⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg
(𝑇 ∘ 𝑔))〉) |
16 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupf 19479 |
. 2
⊢ (𝜑 → 𝐸:𝑋⟶𝐵) |
17 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(freeMnd‘(𝐼
× 2o)) = (freeMnd‘(𝐼 × 2o)) |
18 | 6, 17, 14 | frgpval 19464 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑉 → 𝐺 = ((freeMnd‘(𝐼 × 2o))
/s ∼ )) |
19 | 5, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 = ((freeMnd‘(𝐼 × 2o))
/s ∼ )) |
20 | | 2on 8390 |
. . . . . . . . . . . . 13
⊢
2o ∈ On |
21 | | xpexg 7671 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 2o ∈ On) →
(𝐼 × 2o)
∈ V) |
22 | 5, 20, 21 | sylancl 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 × 2o) ∈
V) |
23 | | wrdexg 14336 |
. . . . . . . . . . . 12
⊢ ((𝐼 × 2o) ∈ V
→ Word (𝐼 ×
2o) ∈ V) |
24 | | fvi 6909 |
. . . . . . . . . . . 12
⊢ (Word
(𝐼 × 2o)
∈ V → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 ×
2o)) |
25 | 22, 23, 24 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ( I ‘Word (𝐼 × 2o)) = Word
(𝐼 ×
2o)) |
26 | 13, 25 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 = Word (𝐼 × 2o)) |
27 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘(freeMnd‘(𝐼 × 2o))) =
(Base‘(freeMnd‘(𝐼 × 2o))) |
28 | 17, 27 | frmdbas 18592 |
. . . . . . . . . . 11
⊢ ((𝐼 × 2o) ∈ V
→ (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 ×
2o)) |
29 | 22, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 ×
2o)) |
30 | 26, 29 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 = (Base‘(freeMnd‘(𝐼 ×
2o)))) |
31 | 14 | fvexi 6848 |
. . . . . . . . . 10
⊢ ∼ ∈
V |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ∼ ∈
V) |
33 | | fvexd 6849 |
. . . . . . . . 9
⊢ (𝜑 → (freeMnd‘(𝐼 × 2o)) ∈
V) |
34 | 19, 30, 32, 33 | qusbas 17358 |
. . . . . . . 8
⊢ (𝜑 → (𝑊 / ∼ ) =
(Base‘𝐺)) |
35 | 1, 34 | eqtr4id 2796 |
. . . . . . 7
⊢ (𝜑 → 𝑋 = (𝑊 / ∼ )) |
36 | | eqimss 3995 |
. . . . . . 7
⊢ (𝑋 = (𝑊 / ∼ ) → 𝑋 ⊆ (𝑊 / ∼ )) |
37 | 35, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ (𝑊 / ∼ )) |
38 | 37 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑋) → 𝑋 ⊆ (𝑊 / ∼ )) |
39 | 38 | sselda 3939 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋) → 𝑐 ∈ (𝑊 / ∼ )) |
40 | | eqid 2737 |
. . . . 5
⊢ (𝑊 / ∼ ) = (𝑊 / ∼ ) |
41 | | oveq2 7354 |
. . . . . . 7
⊢ ([𝑢] ∼ = 𝑐 → (𝑎(+g‘𝐺)[𝑢] ∼ ) = (𝑎(+g‘𝐺)𝑐)) |
42 | 41 | fveq2d 6838 |
. . . . . 6
⊢ ([𝑢] ∼ = 𝑐 → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = (𝐸‘(𝑎(+g‘𝐺)𝑐))) |
43 | | fveq2 6834 |
. . . . . . 7
⊢ ([𝑢] ∼ = 𝑐 → (𝐸‘[𝑢] ∼ ) = (𝐸‘𝑐)) |
44 | 43 | oveq2d 7362 |
. . . . . 6
⊢ ([𝑢] ∼ = 𝑐 → ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) |
45 | 42, 44 | eqeq12d 2753 |
. . . . 5
⊢ ([𝑢] ∼ = 𝑐 → ((𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) ↔ (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐)))) |
46 | 37 | sselda 3939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑊 / ∼ )) |
47 | 46 | adantlr 713 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑊 / ∼ )) |
48 | | fvoveq1 7369 |
. . . . . . . . 9
⊢ ([𝑡] ∼ = 𝑎 → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼
))) |
49 | | fveq2 6834 |
. . . . . . . . . 10
⊢ ([𝑡] ∼ = 𝑎 → (𝐸‘[𝑡] ∼ ) = (𝐸‘𝑎)) |
50 | 49 | oveq1d 7361 |
. . . . . . . . 9
⊢ ([𝑡] ∼ = 𝑎 → ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
51 | 48, 50 | eqeq12d 2753 |
. . . . . . . 8
⊢ ([𝑡] ∼ = 𝑎 → ((𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) ↔ (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
)))) |
52 | | fviss 6910 |
. . . . . . . . . . . . . . . 16
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) |
53 | 13, 52 | eqsstri 3973 |
. . . . . . . . . . . . . . 15
⊢ 𝑊 ⊆ Word (𝐼 × 2o) |
54 | 53 | sseli 3935 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝑊 → 𝑡 ∈ Word (𝐼 × 2o)) |
55 | 53 | sseli 3935 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ 𝑊 → 𝑢 ∈ Word (𝐼 × 2o)) |
56 | | ccatcl 14386 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Word (𝐼 × 2o) ∧ 𝑢 ∈ Word (𝐼 × 2o)) → (𝑡 ++ 𝑢) ∈ Word (𝐼 × 2o)) |
57 | 54, 55, 56 | syl2an 597 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → (𝑡 ++ 𝑢) ∈ Word (𝐼 × 2o)) |
58 | 13 | efgrcl 19421 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) |
60 | 59 | simprd 497 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → 𝑊 = Word (𝐼 × 2o)) |
61 | 57, 60 | eleqtrrd 2841 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → (𝑡 ++ 𝑢) ∈ 𝑊) |
62 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 19480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ++ 𝑢) ∈ 𝑊) → (𝐸‘[(𝑡 ++ 𝑢)] ∼ ) = (𝐻 Σg
(𝑇 ∘ (𝑡 ++ 𝑢)))) |
63 | 61, 62 | sylan2 594 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[(𝑡 ++ 𝑢)] ∼ ) = (𝐻 Σg
(𝑇 ∘ (𝑡 ++ 𝑢)))) |
64 | 54 | ad2antrl 726 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝑡 ∈ Word (𝐼 × 2o)) |
65 | 55 | ad2antll 727 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝑢 ∈ Word (𝐼 × 2o)) |
66 | 2, 10, 11, 9, 5, 12 | frgpuptf 19476 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇:(𝐼 × 2o)⟶𝐵) |
67 | 66 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝑇:(𝐼 × 2o)⟶𝐵) |
68 | | ccatco 14652 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ Word (𝐼 × 2o) ∧ 𝑢 ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (𝑡 ++ 𝑢)) = ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) |
69 | 64, 65, 67, 68 | syl3anc 1371 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝑇 ∘ (𝑡 ++ 𝑢)) = ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) |
70 | 69 | oveq2d 7362 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐻 Σg (𝑇 ∘ (𝑡 ++ 𝑢))) = (𝐻 Σg ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢)))) |
71 | 9 | grpmndd 18690 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ∈ Mnd) |
72 | 71 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝐻 ∈ Mnd) |
73 | | wrdco 14648 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ 𝑡) ∈ Word 𝐵) |
74 | 54, 66, 73 | syl2anr 598 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑇 ∘ 𝑡) ∈ Word 𝐵) |
75 | 74 | adantrr 715 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝑇 ∘ 𝑡) ∈ Word 𝐵) |
76 | | wrdco 14648 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ 𝑢) ∈ Word 𝐵) |
77 | 65, 67, 76 | syl2anc 585 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝑇 ∘ 𝑢) ∈ Word 𝐵) |
78 | 2, 4 | gsumccat 18581 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ 𝑡) ∈ Word 𝐵 ∧ (𝑇 ∘ 𝑢) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) = ((𝐻 Σg (𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) |
79 | 72, 75, 77, 78 | syl3anc 1371 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐻 Σg ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) = ((𝐻 Σg (𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) |
80 | 63, 70, 79 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[(𝑡 ++ 𝑢)] ∼ ) = ((𝐻 Σg
(𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) |
81 | 13, 6, 14, 3 | frgpadd 19469 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → ([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ ) = [(𝑡 ++ 𝑢)] ∼ ) |
82 | 81 | adantl 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → ([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ ) = [(𝑡 ++ 𝑢)] ∼ ) |
83 | 82 | fveq2d 6838 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = (𝐸‘[(𝑡 ++ 𝑢)] ∼ )) |
84 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 19480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐸‘[𝑡] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑡))) |
85 | 84 | adantrr 715 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[𝑡] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑡))) |
86 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 19480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑊) → (𝐸‘[𝑢] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑢))) |
87 | 86 | adantrl 714 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[𝑢] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑢))) |
88 | 85, 87 | oveq12d 7364 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) = ((𝐻 Σg
(𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) |
89 | 80, 83, 88 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
90 | 89 | anass1rs 653 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑡 ∈ 𝑊) → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
91 | 40, 51, 90 | ectocld 8653 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑎 ∈ (𝑊 / ∼ )) → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
92 | 47, 91 | syldan 592 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑎 ∈ 𝑋) → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
93 | 92 | an32s 650 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑢 ∈ 𝑊) → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
94 | 40, 45, 93 | ectocld 8653 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑐 ∈ (𝑊 / ∼ )) → (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) |
95 | 39, 94 | syldan 592 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋) → (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) |
96 | 95 | anasss 468 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) |
97 | 1, 2, 3, 4, 8, 9, 16, 96 | isghmd 18944 |
1
⊢ (𝜑 → 𝐸 ∈ (𝐺 GrpHom 𝐻)) |