Step | Hyp | Ref
| Expression |
1 | | frgpup.x |
. 2
⊢ 𝑋 = (Base‘𝐺) |
2 | | frgpup.b |
. 2
⊢ 𝐵 = (Base‘𝐻) |
3 | | eqid 2610 |
. 2
⊢
(+g‘𝐺) = (+g‘𝐺) |
4 | | eqid 2610 |
. 2
⊢
(+g‘𝐻) = (+g‘𝐻) |
5 | | frgpup.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
6 | | frgpup.g |
. . . 4
⊢ 𝐺 = (freeGrp‘𝐼) |
7 | 6 | frgpgrp 17998 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp) |
8 | 5, 7 | syl 17 |
. 2
⊢ (𝜑 → 𝐺 ∈ Grp) |
9 | | frgpup.h |
. 2
⊢ (𝜑 → 𝐻 ∈ Grp) |
10 | | frgpup.n |
. . 3
⊢ 𝑁 = (invg‘𝐻) |
11 | | frgpup.t |
. . 3
⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) |
12 | | frgpup.a |
. . 3
⊢ (𝜑 → 𝐹:𝐼⟶𝐵) |
13 | | frgpup.w |
. . 3
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
14 | | frgpup.r |
. . 3
⊢ ∼ = (
~FG ‘𝐼) |
15 | | frgpup.e |
. . 3
⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg
(𝑇 ∘ 𝑔))〉) |
16 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupf 18009 |
. 2
⊢ (𝜑 → 𝐸:𝑋⟶𝐵) |
17 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(freeMnd‘(𝐼
× 2𝑜)) = (freeMnd‘(𝐼 ×
2𝑜)) |
18 | 6, 17, 14 | frgpval 17994 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑉 → 𝐺 = ((freeMnd‘(𝐼 × 2𝑜))
/s ∼ )) |
19 | 5, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 = ((freeMnd‘(𝐼 × 2𝑜))
/s ∼ )) |
20 | | 2on 7455 |
. . . . . . . . . . . . 13
⊢
2𝑜 ∈ On |
21 | | xpexg 6858 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 2𝑜 ∈ On)
→ (𝐼 ×
2𝑜) ∈ V) |
22 | 5, 20, 21 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 × 2𝑜) ∈
V) |
23 | | wrdexg 13170 |
. . . . . . . . . . . 12
⊢ ((𝐼 × 2𝑜)
∈ V → Word (𝐼
× 2𝑜) ∈ V) |
24 | | fvi 6165 |
. . . . . . . . . . . 12
⊢ (Word
(𝐼 ×
2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word
(𝐼 ×
2𝑜)) |
25 | 22, 23, 24 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ( I ‘Word (𝐼 × 2𝑜))
= Word (𝐼 ×
2𝑜)) |
26 | 13, 25 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 = Word (𝐼 ×
2𝑜)) |
27 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘(freeMnd‘(𝐼 × 2𝑜))) =
(Base‘(freeMnd‘(𝐼 ×
2𝑜))) |
28 | 17, 27 | frmdbas 17212 |
. . . . . . . . . . 11
⊢ ((𝐼 × 2𝑜)
∈ V → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word
(𝐼 ×
2𝑜)) |
29 | 22, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word
(𝐼 ×
2𝑜)) |
30 | 26, 29 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 = (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
31 | | fvex 6113 |
. . . . . . . . . . 11
⊢ (
~FG ‘𝐼) ∈ V |
32 | 14, 31 | eqeltri 2684 |
. . . . . . . . . 10
⊢ ∼ ∈
V |
33 | 32 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ∼ ∈
V) |
34 | | fvex 6113 |
. . . . . . . . . 10
⊢
(freeMnd‘(𝐼
× 2𝑜)) ∈ V |
35 | 34 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (freeMnd‘(𝐼 × 2𝑜))
∈ V) |
36 | 19, 30, 33, 35 | qusbas 16028 |
. . . . . . . 8
⊢ (𝜑 → (𝑊 / ∼ ) =
(Base‘𝐺)) |
37 | 36, 1 | syl6reqr 2663 |
. . . . . . 7
⊢ (𝜑 → 𝑋 = (𝑊 / ∼ )) |
38 | | eqimss 3620 |
. . . . . . 7
⊢ (𝑋 = (𝑊 / ∼ ) → 𝑋 ⊆ (𝑊 / ∼ )) |
39 | 37, 38 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ (𝑊 / ∼ )) |
40 | 39 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑋) → 𝑋 ⊆ (𝑊 / ∼ )) |
41 | 40 | sselda 3568 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋) → 𝑐 ∈ (𝑊 / ∼ )) |
42 | | eqid 2610 |
. . . . 5
⊢ (𝑊 / ∼ ) = (𝑊 / ∼ ) |
43 | | oveq2 6557 |
. . . . . . 7
⊢ ([𝑢] ∼ = 𝑐 → (𝑎(+g‘𝐺)[𝑢] ∼ ) = (𝑎(+g‘𝐺)𝑐)) |
44 | 43 | fveq2d 6107 |
. . . . . 6
⊢ ([𝑢] ∼ = 𝑐 → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = (𝐸‘(𝑎(+g‘𝐺)𝑐))) |
45 | | fveq2 6103 |
. . . . . . 7
⊢ ([𝑢] ∼ = 𝑐 → (𝐸‘[𝑢] ∼ ) = (𝐸‘𝑐)) |
46 | 45 | oveq2d 6565 |
. . . . . 6
⊢ ([𝑢] ∼ = 𝑐 → ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) |
47 | 44, 46 | eqeq12d 2625 |
. . . . 5
⊢ ([𝑢] ∼ = 𝑐 → ((𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) ↔ (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐)))) |
48 | 39 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑊 / ∼ )) |
49 | 48 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑊 / ∼ )) |
50 | | oveq1 6556 |
. . . . . . . . . 10
⊢ ([𝑡] ∼ = 𝑎 → ([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ ) = (𝑎(+g‘𝐺)[𝑢] ∼ )) |
51 | 50 | fveq2d 6107 |
. . . . . . . . 9
⊢ ([𝑡] ∼ = 𝑎 → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼
))) |
52 | | fveq2 6103 |
. . . . . . . . . 10
⊢ ([𝑡] ∼ = 𝑎 → (𝐸‘[𝑡] ∼ ) = (𝐸‘𝑎)) |
53 | 52 | oveq1d 6564 |
. . . . . . . . 9
⊢ ([𝑡] ∼ = 𝑎 → ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
54 | 51, 53 | eqeq12d 2625 |
. . . . . . . 8
⊢ ([𝑡] ∼ = 𝑎 → ((𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) ↔ (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
)))) |
55 | | fviss 6166 |
. . . . . . . . . . . . . . . 16
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
56 | 13, 55 | eqsstri 3598 |
. . . . . . . . . . . . . . 15
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
57 | 56 | sseli 3564 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝑊 → 𝑡 ∈ Word (𝐼 ×
2𝑜)) |
58 | 56 | sseli 3564 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ 𝑊 → 𝑢 ∈ Word (𝐼 ×
2𝑜)) |
59 | | ccatcl 13212 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ 𝑢 ∈ Word (𝐼 × 2𝑜)) →
(𝑡 ++ 𝑢) ∈ Word (𝐼 ×
2𝑜)) |
60 | 57, 58, 59 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → (𝑡 ++ 𝑢) ∈ Word (𝐼 ×
2𝑜)) |
61 | 13 | efgrcl 17951 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
63 | 62 | simprd 478 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → 𝑊 = Word (𝐼 ×
2𝑜)) |
64 | 60, 63 | eleqtrrd 2691 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → (𝑡 ++ 𝑢) ∈ 𝑊) |
65 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 18010 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ++ 𝑢) ∈ 𝑊) → (𝐸‘[(𝑡 ++ 𝑢)] ∼ ) = (𝐻 Σg
(𝑇 ∘ (𝑡 ++ 𝑢)))) |
66 | 64, 65 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[(𝑡 ++ 𝑢)] ∼ ) = (𝐻 Σg
(𝑇 ∘ (𝑡 ++ 𝑢)))) |
67 | 57 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝑡 ∈ Word (𝐼 ×
2𝑜)) |
68 | 58 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝑢 ∈ Word (𝐼 ×
2𝑜)) |
69 | 2, 10, 11, 9, 5, 12 | frgpuptf 18006 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇:(𝐼 × 2𝑜)⟶𝐵) |
70 | 69 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝑇:(𝐼 × 2𝑜)⟶𝐵) |
71 | | ccatco 13432 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ 𝑢 ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (𝑡 ++ 𝑢)) = ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) |
72 | 67, 68, 70, 71 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝑇 ∘ (𝑡 ++ 𝑢)) = ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) |
73 | 72 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐻 Σg (𝑇 ∘ (𝑡 ++ 𝑢))) = (𝐻 Σg ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢)))) |
74 | | grpmnd 17252 |
. . . . . . . . . . . . . 14
⊢ (𝐻 ∈ Grp → 𝐻 ∈ Mnd) |
75 | 9, 74 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ∈ Mnd) |
76 | 75 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → 𝐻 ∈ Mnd) |
77 | | wrdco 13428 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ 𝑡) ∈ Word 𝐵) |
78 | 57, 69, 77 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑇 ∘ 𝑡) ∈ Word 𝐵) |
79 | 78 | adantrr 749 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝑇 ∘ 𝑡) ∈ Word 𝐵) |
80 | | wrdco 13428 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ 𝑢) ∈ Word 𝐵) |
81 | 68, 70, 80 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝑇 ∘ 𝑢) ∈ Word 𝐵) |
82 | 2, 4 | gsumccat 17201 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ 𝑡) ∈ Word 𝐵 ∧ (𝑇 ∘ 𝑢) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) = ((𝐻 Σg (𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) |
83 | 76, 79, 81, 82 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐻 Σg ((𝑇 ∘ 𝑡) ++ (𝑇 ∘ 𝑢))) = ((𝐻 Σg (𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) |
84 | 66, 73, 83 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[(𝑡 ++ 𝑢)] ∼ ) = ((𝐻 Σg
(𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) |
85 | 13, 6, 14, 3 | frgpadd 17999 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊) → ([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ ) = [(𝑡 ++ 𝑢)] ∼ ) |
86 | 85 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → ([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ ) = [(𝑡 ++ 𝑢)] ∼ ) |
87 | 86 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = (𝐸‘[(𝑡 ++ 𝑢)] ∼ )) |
88 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 18010 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐸‘[𝑡] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑡))) |
89 | 88 | adantrr 749 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[𝑡] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑡))) |
90 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 18010 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑊) → (𝐸‘[𝑢] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑢))) |
91 | 90 | adantrl 748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘[𝑢] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑢))) |
92 | 89, 91 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼ )) = ((𝐻 Σg
(𝑇 ∘ 𝑡))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ 𝑢)))) |
93 | 84, 87, 92 | 3eqtr4d 2654 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊)) → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
94 | 93 | anass1rs 845 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑡 ∈ 𝑊) → (𝐸‘([𝑡] ∼
(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘[𝑡] ∼
)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
95 | 42, 54, 94 | ectocld 7701 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑎 ∈ (𝑊 / ∼ )) → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
96 | 49, 95 | syldan 486 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑊) ∧ 𝑎 ∈ 𝑋) → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
97 | 96 | an32s 842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑢 ∈ 𝑊) → (𝐸‘(𝑎(+g‘𝐺)[𝑢] ∼ )) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘[𝑢] ∼
))) |
98 | 42, 47, 97 | ectocld 7701 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑐 ∈ (𝑊 / ∼ )) → (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) |
99 | 41, 98 | syldan 486 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋) → (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) |
100 | 99 | anasss 677 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐸‘(𝑎(+g‘𝐺)𝑐)) = ((𝐸‘𝑎)(+g‘𝐻)(𝐸‘𝑐))) |
101 | 1, 2, 3, 4, 8, 9, 16, 100 | isghmd 17492 |
1
⊢ (𝜑 → 𝐸 ∈ (𝐺 GrpHom 𝐻)) |