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 19551 |
. . 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 19562 |
. 2
β’ (π β πΈ:πβΆπ΅) |
17 | | eqid 2737 |
. . . . . . . . . . 11
β’
(freeMndβ(πΌ
Γ 2o)) = (freeMndβ(πΌ Γ 2o)) |
18 | 6, 17, 14 | frgpval 19547 |
. . . . . . . . . 10
β’ (πΌ β π β πΊ = ((freeMndβ(πΌ Γ 2o))
/s βΌ )) |
19 | 5, 18 | syl 17 |
. . . . . . . . 9
β’ (π β πΊ = ((freeMndβ(πΌ Γ 2o))
/s βΌ )) |
20 | | 2on 8431 |
. . . . . . . . . . . . 13
β’
2o β On |
21 | | xpexg 7689 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ 2o β On) β
(πΌ Γ 2o)
β V) |
22 | 5, 20, 21 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β (πΌ Γ 2o) β
V) |
23 | | wrdexg 14419 |
. . . . . . . . . . . 12
β’ ((πΌ Γ 2o) β V
β Word (πΌ Γ
2o) β V) |
24 | | fvi 6922 |
. . . . . . . . . . . 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 18669 |
. . . . . . . . . . 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 6861 |
. . . . . . . . . 10
β’ βΌ β
V |
32 | 31 | a1i 11 |
. . . . . . . . 9
β’ (π β βΌ β
V) |
33 | | fvexd 6862 |
. . . . . . . . 9
β’ (π β (freeMndβ(πΌ Γ 2o)) β
V) |
34 | 19, 30, 32, 33 | qusbas 17434 |
. . . . . . . 8
β’ (π β (π / βΌ ) =
(BaseβπΊ)) |
35 | 1, 34 | eqtr4id 2796 |
. . . . . . 7
β’ (π β π = (π / βΌ )) |
36 | | eqimss 4005 |
. . . . . . 7
β’ (π = (π / βΌ ) β π β (π / βΌ )) |
37 | 35, 36 | syl 17 |
. . . . . 6
β’ (π β π β (π / βΌ )) |
38 | 37 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β π β (π / βΌ )) |
39 | 38 | sselda 3949 |
. . . 4
β’ (((π β§ π β π) β§ π β π) β π β (π / βΌ )) |
40 | | eqid 2737 |
. . . . 5
β’ (π / βΌ ) = (π / βΌ ) |
41 | | oveq2 7370 |
. . . . . . 7
β’ ([π’] βΌ = π β (π(+gβπΊ)[π’] βΌ ) = (π(+gβπΊ)π)) |
42 | 41 | fveq2d 6851 |
. . . . . 6
β’ ([π’] βΌ = π β (πΈβ(π(+gβπΊ)[π’] βΌ )) = (πΈβ(π(+gβπΊ)π))) |
43 | | fveq2 6847 |
. . . . . . 7
β’ ([π’] βΌ = π β (πΈβ[π’] βΌ ) = (πΈβπ)) |
44 | 43 | oveq2d 7378 |
. . . . . 6
β’ ([π’] βΌ = π β ((πΈβπ)(+gβπ»)(πΈβ[π’] βΌ )) = ((πΈβπ)(+gβπ»)(πΈβπ))) |
45 | 42, 44 | eqeq12d 2753 |
. . . . 5
β’ ([π’] βΌ = π β ((πΈβ(π(+gβπΊ)[π’] βΌ )) = ((πΈβπ)(+gβπ»)(πΈβ[π’] βΌ )) β (πΈβ(π(+gβπΊ)π)) = ((πΈβπ)(+gβπ»)(πΈβπ)))) |
46 | 37 | sselda 3949 |
. . . . . . . 8
β’ ((π β§ π β π) β π β (π / βΌ )) |
47 | 46 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π’ β π) β§ π β π) β π β (π / βΌ )) |
48 | | fvoveq1 7385 |
. . . . . . . . 9
β’ ([π‘] βΌ = π β (πΈβ([π‘] βΌ
(+gβπΊ)[π’] βΌ )) = (πΈβ(π(+gβπΊ)[π’] βΌ
))) |
49 | | fveq2 6847 |
. . . . . . . . . 10
β’ ([π‘] βΌ = π β (πΈβ[π‘] βΌ ) = (πΈβπ)) |
50 | 49 | oveq1d 7377 |
. . . . . . . . 9
β’ ([π‘] βΌ = π β ((πΈβ[π‘] βΌ
)(+gβπ»)(πΈβ[π’] βΌ )) = ((πΈβπ)(+gβπ»)(πΈβ[π’] βΌ
))) |
51 | 48, 50 | eqeq12d 2753 |
. . . . . . . 8
β’ ([π‘] βΌ = π β ((πΈβ([π‘] βΌ
(+gβπΊ)[π’] βΌ )) = ((πΈβ[π‘] βΌ
)(+gβπ»)(πΈβ[π’] βΌ )) β (πΈβ(π(+gβπΊ)[π’] βΌ )) = ((πΈβπ)(+gβπ»)(πΈβ[π’] βΌ
)))) |
52 | | fviss 6923 |
. . . . . . . . . . . . . . . 16
β’ ( I
βWord (πΌ Γ
2o)) β Word (πΌ Γ 2o) |
53 | 13, 52 | eqsstri 3983 |
. . . . . . . . . . . . . . 15
β’ π β Word (πΌ Γ 2o) |
54 | 53 | sseli 3945 |
. . . . . . . . . . . . . 14
β’ (π‘ β π β π‘ β Word (πΌ Γ 2o)) |
55 | 53 | sseli 3945 |
. . . . . . . . . . . . . 14
β’ (π’ β π β π’ β Word (πΌ Γ 2o)) |
56 | | ccatcl 14469 |
. . . . . . . . . . . . . 14
β’ ((π‘ β Word (πΌ Γ 2o) β§ π’ β Word (πΌ Γ 2o)) β (π‘ ++ π’) β Word (πΌ Γ 2o)) |
57 | 54, 55, 56 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π‘ β π β§ π’ β π) β (π‘ ++ π’) β Word (πΌ Γ 2o)) |
58 | 13 | efgrcl 19504 |
. . . . . . . . . . . . . . 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 19563 |
. . . . . . . . . . . 12
β’ ((π β§ (π‘ ++ π’) β π) β (πΈβ[(π‘ ++ π’)] βΌ ) = (π» Ξ£g
(π β (π‘ ++ π’)))) |
63 | 61, 62 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β π β§ π’ β π)) β (πΈβ[(π‘ ++ π’)] βΌ ) = (π» Ξ£g
(π β (π‘ ++ π’)))) |
64 | 54 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ ((π β§ (π‘ β π β§ π’ β π)) β π‘ β Word (πΌ Γ 2o)) |
65 | 55 | ad2antll 728 |
. . . . . . . . . . . . 13
β’ ((π β§ (π‘ β π β§ π’ β π)) β π’ β Word (πΌ Γ 2o)) |
66 | 2, 10, 11, 9, 5, 12 | frgpuptf 19559 |
. . . . . . . . . . . . . 14
β’ (π β π:(πΌ Γ 2o)βΆπ΅) |
67 | 66 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π‘ β π β§ π’ β π)) β π:(πΌ Γ 2o)βΆπ΅) |
68 | | ccatco 14731 |
. . . . . . . . . . . . 13
β’ ((π‘ β Word (πΌ Γ 2o) β§ π’ β Word (πΌ Γ 2o) β§ π:(πΌ Γ 2o)βΆπ΅) β (π β (π‘ ++ π’)) = ((π β π‘) ++ (π β π’))) |
69 | 64, 65, 67, 68 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ (π‘ β π β§ π’ β π)) β (π β (π‘ ++ π’)) = ((π β π‘) ++ (π β π’))) |
70 | 69 | oveq2d 7378 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β π β§ π’ β π)) β (π» Ξ£g (π β (π‘ ++ π’))) = (π» Ξ£g ((π β π‘) ++ (π β π’)))) |
71 | 9 | grpmndd 18767 |
. . . . . . . . . . . . 13
β’ (π β π» β Mnd) |
72 | 71 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π‘ β π β§ π’ β π)) β π» β Mnd) |
73 | | wrdco 14727 |
. . . . . . . . . . . . . 14
β’ ((π‘ β Word (πΌ Γ 2o) β§ π:(πΌ Γ 2o)βΆπ΅) β (π β π‘) β Word π΅) |
74 | 54, 66, 73 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β π) β (π β π‘) β Word π΅) |
75 | 74 | adantrr 716 |
. . . . . . . . . . . 12
β’ ((π β§ (π‘ β π β§ π’ β π)) β (π β π‘) β Word π΅) |
76 | | wrdco 14727 |
. . . . . . . . . . . . 13
β’ ((π’ β Word (πΌ Γ 2o) β§ π:(πΌ Γ 2o)βΆπ΅) β (π β π’) β Word π΅) |
77 | 65, 67, 76 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ (π‘ β π β§ π’ β π)) β (π β π’) β Word π΅) |
78 | 2, 4 | gsumccat 18658 |
. . . . . . . . . . . 12
β’ ((π» β Mnd β§ (π β π‘) β Word π΅ β§ (π β π’) β Word π΅) β (π» Ξ£g ((π β π‘) ++ (π β π’))) = ((π» Ξ£g (π β π‘))(+gβπ»)(π» Ξ£g (π β π’)))) |
79 | 72, 75, 77, 78 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β π β§ π’ β π)) β (π» Ξ£g ((π β π‘) ++ (π β π’))) = ((π» Ξ£g (π β π‘))(+gβπ»)(π» Ξ£g (π β π’)))) |
80 | 63, 70, 79 | 3eqtrd 2781 |
. . . . . . . . . 10
β’ ((π β§ (π‘ β π β§ π’ β π)) β (πΈβ[(π‘ ++ π’)] βΌ ) = ((π» Ξ£g
(π β π‘))(+gβπ»)(π» Ξ£g (π β π’)))) |
81 | 13, 6, 14, 3 | frgpadd 19552 |
. . . . . . . . . . . 12
β’ ((π‘ β π β§ π’ β π) β ([π‘] βΌ
(+gβπΊ)[π’] βΌ ) = [(π‘ ++ π’)] βΌ ) |
82 | 81 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β π β§ π’ β π)) β ([π‘] βΌ
(+gβπΊ)[π’] βΌ ) = [(π‘ ++ π’)] βΌ ) |
83 | 82 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π β§ (π‘ β π β§ π’ β π)) β (πΈβ([π‘] βΌ
(+gβπΊ)[π’] βΌ )) = (πΈβ[(π‘ ++ π’)] βΌ )) |
84 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 19563 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β (πΈβ[π‘] βΌ ) = (π» Ξ£g
(π β π‘))) |
85 | 84 | adantrr 716 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β π β§ π’ β π)) β (πΈβ[π‘] βΌ ) = (π» Ξ£g
(π β π‘))) |
86 | 2, 10, 11, 9, 5, 12, 13, 14, 6, 1, 15 | frgpupval 19563 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β π) β (πΈβ[π’] βΌ ) = (π» Ξ£g
(π β π’))) |
87 | 86 | adantrl 715 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β π β§ π’ β π)) β (πΈβ[π’] βΌ ) = (π» Ξ£g
(π β π’))) |
88 | 85, 87 | oveq12d 7380 |
. . . . . . . . . 10
β’ ((π β§ (π‘ β π β§ π’ β π)) β ((πΈβ[π‘] βΌ
)(+gβπ»)(πΈβ[π’] βΌ )) = ((π» Ξ£g
(π β π‘))(+gβπ»)(π» Ξ£g (π β π’)))) |
89 | 80, 83, 88 | 3eqtr4d 2787 |
. . . . . . . . 9
β’ ((π β§ (π‘ β π β§ π’ β π)) β (πΈβ([π‘] βΌ
(+gβπΊ)[π’] βΌ )) = ((πΈβ[π‘] βΌ
)(+gβπ»)(πΈβ[π’] βΌ
))) |
90 | 89 | anass1rs 654 |
. . . . . . . 8
β’ (((π β§ π’ β π) β§ π‘ β π) β (πΈβ([π‘] βΌ
(+gβπΊ)[π’] βΌ )) = ((πΈβ[π‘] βΌ
)(+gβπ»)(πΈβ[π’] βΌ
))) |
91 | 40, 51, 90 | ectocld 8730 |
. . . . . . 7
β’ (((π β§ π’ β π) β§ π β (π / βΌ )) β (πΈβ(π(+gβπΊ)[π’] βΌ )) = ((πΈβπ)(+gβπ»)(πΈβ[π’] βΌ
))) |
92 | 47, 91 | syldan 592 |
. . . . . 6
β’ (((π β§ π’ β π) β§ π β π) β (πΈβ(π(+gβπΊ)[π’] βΌ )) = ((πΈβπ)(+gβπ»)(πΈβ[π’] βΌ
))) |
93 | 92 | an32s 651 |
. . . . 5
β’ (((π β§ π β π) β§ π’ β π) β (πΈβ(π(+gβπΊ)[π’] βΌ )) = ((πΈβπ)(+gβπ»)(πΈβ[π’] βΌ
))) |
94 | 40, 45, 93 | ectocld 8730 |
. . . 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 19024 |
1
β’ (π β πΈ β (πΊ GrpHom π»)) |