Step | Hyp | Ref
| Expression |
1 | | frgp0.m |
. . 3
β’ πΊ = (freeGrpβπΌ) |
2 | | eqid 2732 |
. . 3
β’
(freeMndβ(πΌ
Γ 2o)) = (freeMndβ(πΌ Γ 2o)) |
3 | | frgp0.r |
. . 3
β’ βΌ = (
~FG βπΌ) |
4 | 1, 2, 3 | frgpval 19620 |
. 2
β’ (πΌ β π β πΊ = ((freeMndβ(πΌ Γ 2o))
/s βΌ )) |
5 | | 2on 8476 |
. . . . 5
β’
2o β On |
6 | | xpexg 7733 |
. . . . 5
β’ ((πΌ β π β§ 2o β On) β
(πΌ Γ 2o)
β V) |
7 | 5, 6 | mpan2 689 |
. . . 4
β’ (πΌ β π β (πΌ Γ 2o) β
V) |
8 | | eqid 2732 |
. . . . 5
β’
(Baseβ(freeMndβ(πΌ Γ 2o))) =
(Baseβ(freeMndβ(πΌ Γ 2o))) |
9 | 2, 8 | frmdbas 18729 |
. . . 4
β’ ((πΌ Γ 2o) β V
β (Baseβ(freeMndβ(πΌ Γ 2o))) = Word (πΌ Γ
2o)) |
10 | 7, 9 | syl 17 |
. . 3
β’ (πΌ β π β (Baseβ(freeMndβ(πΌ Γ 2o))) = Word
(πΌ Γ
2o)) |
11 | 10 | eqcomd 2738 |
. 2
β’ (πΌ β π β Word (πΌ Γ 2o) =
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
12 | | eqidd 2733 |
. 2
β’ (πΌ β π β
(+gβ(freeMndβ(πΌ Γ 2o))) =
(+gβ(freeMndβ(πΌ Γ 2o)))) |
13 | | eqid 2732 |
. . . 4
β’ ( I
βWord (πΌ Γ
2o)) = ( I βWord (πΌ Γ 2o)) |
14 | 13, 3 | efger 19580 |
. . 3
β’ βΌ Er ( I
βWord (πΌ Γ
2o)) |
15 | | wrdexg 14470 |
. . . . 5
β’ ((πΌ Γ 2o) β V
β Word (πΌ Γ
2o) β V) |
16 | | fvi 6964 |
. . . . 5
β’ (Word
(πΌ Γ 2o)
β V β ( I βWord (πΌ Γ 2o)) = Word (πΌ Γ
2o)) |
17 | 7, 15, 16 | 3syl 18 |
. . . 4
β’ (πΌ β π β ( I βWord (πΌ Γ 2o)) = Word (πΌ Γ
2o)) |
18 | | ereq2 8707 |
. . . 4
β’ (( I
βWord (πΌ Γ
2o)) = Word (πΌ
Γ 2o) β ( βΌ Er ( I βWord
(πΌ Γ 2o))
β βΌ Er Word (πΌ Γ
2o))) |
19 | 17, 18 | syl 17 |
. . 3
β’ (πΌ β π β ( βΌ Er ( I βWord
(πΌ Γ 2o))
β βΌ Er Word (πΌ Γ
2o))) |
20 | 14, 19 | mpbii 232 |
. 2
β’ (πΌ β π β βΌ Er Word (πΌ Γ
2o)) |
21 | | fvexd 6903 |
. 2
β’ (πΌ β π β (freeMndβ(πΌ Γ 2o)) β
V) |
22 | | eqid 2732 |
. . . 4
β’
(+gβ(freeMndβ(πΌ Γ 2o))) =
(+gβ(freeMndβ(πΌ Γ 2o))) |
23 | 1, 2, 3, 22 | frgpcpbl 19621 |
. . 3
β’ ((π βΌ π β§ π βΌ π) β (π(+gβ(freeMndβ(πΌ Γ 2o)))π) βΌ (π(+gβ(freeMndβ(πΌ Γ 2o)))π)) |
24 | 23 | a1i 11 |
. 2
β’ (πΌ β π β ((π βΌ π β§ π βΌ π) β (π(+gβ(freeMndβ(πΌ Γ 2o)))π) βΌ (π(+gβ(freeMndβ(πΌ Γ 2o)))π))) |
25 | 2 | frmdmnd 18736 |
. . . . . 6
β’ ((πΌ Γ 2o) β V
β (freeMndβ(πΌ
Γ 2o)) β Mnd) |
26 | 7, 25 | syl 17 |
. . . . 5
β’ (πΌ β π β (freeMndβ(πΌ Γ 2o)) β
Mnd) |
27 | 26 | 3ad2ant1 1133 |
. . . 4
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o)) β
(freeMndβ(πΌ Γ
2o)) β Mnd) |
28 | | simp2 1137 |
. . . . 5
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o)) β π₯ β Word (πΌ Γ 2o)) |
29 | 11 | 3ad2ant1 1133 |
. . . . 5
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o)) β Word (πΌ Γ 2o) =
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
30 | 28, 29 | eleqtrd 2835 |
. . . 4
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o)) β π₯ β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
31 | | simp3 1138 |
. . . . 5
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o)) β π¦ β Word (πΌ Γ 2o)) |
32 | 31, 29 | eleqtrd 2835 |
. . . 4
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o)) β π¦ β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
33 | 8, 22 | mndcl 18629 |
. . . 4
β’
(((freeMndβ(πΌ
Γ 2o)) β Mnd β§ π₯ β (Baseβ(freeMndβ(πΌ Γ 2o))) β§
π¦ β
(Baseβ(freeMndβ(πΌ Γ 2o)))) β (π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦) β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
34 | 27, 30, 32, 33 | syl3anc 1371 |
. . 3
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o)) β (π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦) β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
35 | 34, 29 | eleqtrrd 2836 |
. 2
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o)) β (π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦) β Word (πΌ Γ 2o)) |
36 | 20 | adantr 481 |
. . . 4
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β βΌ Er
Word (πΌ Γ
2o)) |
37 | 26 | adantr 481 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β
(freeMndβ(πΌ Γ
2o)) β Mnd) |
38 | 34 | 3adant3r3 1184 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β (π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦) β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
39 | | simpr3 1196 |
. . . . . . 7
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β π§ β Word (πΌ Γ 2o)) |
40 | 11 | adantr 481 |
. . . . . . 7
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β Word (πΌ Γ 2o) =
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
41 | 39, 40 | eleqtrd 2835 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β π§ β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
42 | 8, 22 | mndcl 18629 |
. . . . . 6
β’
(((freeMndβ(πΌ
Γ 2o)) β Mnd β§ (π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦) β
(Baseβ(freeMndβ(πΌ Γ 2o))) β§ π§ β
(Baseβ(freeMndβ(πΌ Γ 2o)))) β ((π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦)(+gβ(freeMndβ(πΌ Γ 2o)))π§) β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
43 | 37, 38, 41, 42 | syl3anc 1371 |
. . . . 5
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β ((π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦)(+gβ(freeMndβ(πΌ Γ 2o)))π§) β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
44 | 43, 40 | eleqtrrd 2836 |
. . . 4
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β ((π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦)(+gβ(freeMndβ(πΌ Γ 2o)))π§) β Word (πΌ Γ 2o)) |
45 | 36, 44 | erref 8719 |
. . 3
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β ((π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦)(+gβ(freeMndβ(πΌ Γ 2o)))π§) βΌ ((π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦)(+gβ(freeMndβ(πΌ Γ 2o)))π§)) |
46 | 30 | 3adant3r3 1184 |
. . . 4
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β π₯ β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
47 | 32 | 3adant3r3 1184 |
. . . 4
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β π¦ β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
48 | 8, 22 | mndass 18630 |
. . . 4
β’
(((freeMndβ(πΌ
Γ 2o)) β Mnd β§ (π₯ β (Baseβ(freeMndβ(πΌ Γ 2o))) β§
π¦ β
(Baseβ(freeMndβ(πΌ Γ 2o))) β§ π§ β
(Baseβ(freeMndβ(πΌ Γ 2o))))) β ((π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦)(+gβ(freeMndβ(πΌ Γ 2o)))π§) = (π₯(+gβ(freeMndβ(πΌ Γ 2o)))(π¦(+gβ(freeMndβ(πΌ Γ 2o)))π§))) |
49 | 37, 46, 47, 41, 48 | syl13anc 1372 |
. . 3
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β ((π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦)(+gβ(freeMndβ(πΌ Γ 2o)))π§) = (π₯(+gβ(freeMndβ(πΌ Γ 2o)))(π¦(+gβ(freeMndβ(πΌ Γ 2o)))π§))) |
50 | 45, 49 | breqtrd 5173 |
. 2
β’ ((πΌ β π β§ (π₯ β Word (πΌ Γ 2o) β§ π¦ β Word (πΌ Γ 2o) β§ π§ β Word (πΌ Γ 2o))) β ((π₯(+gβ(freeMndβ(πΌ Γ 2o)))π¦)(+gβ(freeMndβ(πΌ Γ 2o)))π§) βΌ (π₯(+gβ(freeMndβ(πΌ Γ 2o)))(π¦(+gβ(freeMndβ(πΌ Γ 2o)))π§))) |
51 | | wrd0 14485 |
. . 3
β’ β
β Word (πΌ Γ
2o) |
52 | 51 | a1i 11 |
. 2
β’ (πΌ β π β β
β Word (πΌ Γ
2o)) |
53 | 51, 11 | eleqtrid 2839 |
. . . . . 6
β’ (πΌ β π β β
β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
54 | 53 | adantr 481 |
. . . . 5
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β β
β (Baseβ(freeMndβ(πΌ Γ 2o)))) |
55 | 11 | eleq2d 2819 |
. . . . . 6
β’ (πΌ β π β (π₯ β Word (πΌ Γ 2o) β π₯ β
(Baseβ(freeMndβ(πΌ Γ 2o))))) |
56 | 55 | biimpa 477 |
. . . . 5
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β π₯ β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
57 | 2, 8, 22 | frmdadd 18732 |
. . . . 5
β’ ((β
β (Baseβ(freeMndβ(πΌ Γ 2o))) β§ π₯ β
(Baseβ(freeMndβ(πΌ Γ 2o)))) β
(β
(+gβ(freeMndβ(πΌ Γ 2o)))π₯) = (β
++ π₯)) |
58 | 54, 56, 57 | syl2anc 584 |
. . . 4
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β
(β
(+gβ(freeMndβ(πΌ Γ 2o)))π₯) = (β
++ π₯)) |
59 | | ccatlid 14532 |
. . . . 5
β’ (π₯ β Word (πΌ Γ 2o) β (β
++
π₯) = π₯) |
60 | 59 | adantl 482 |
. . . 4
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β (β
++
π₯) = π₯) |
61 | 58, 60 | eqtrd 2772 |
. . 3
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β
(β
(+gβ(freeMndβ(πΌ Γ 2o)))π₯) = π₯) |
62 | 20 | adantr 481 |
. . . 4
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β βΌ Er
Word (πΌ Γ
2o)) |
63 | | simpr 485 |
. . . 4
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β π₯ β Word (πΌ Γ 2o)) |
64 | 62, 63 | erref 8719 |
. . 3
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β π₯ βΌ π₯) |
65 | 61, 64 | eqbrtrd 5169 |
. 2
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β
(β
(+gβ(freeMndβ(πΌ Γ 2o)))π₯) βΌ π₯) |
66 | | revcl 14707 |
. . . 4
β’ (π₯ β Word (πΌ Γ 2o) β
(reverseβπ₯) β
Word (πΌ Γ
2o)) |
67 | 66 | adantl 482 |
. . 3
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β
(reverseβπ₯) β
Word (πΌ Γ
2o)) |
68 | | eqid 2732 |
. . . . 5
β’ (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
69 | 68 | efgmf 19575 |
. . . 4
β’ (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©):(πΌ Γ 2o)βΆ(πΌ Γ
2o) |
70 | 69 | a1i 11 |
. . 3
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©):(πΌ Γ 2o)βΆ(πΌ Γ
2o)) |
71 | | wrdco 14778 |
. . 3
β’
(((reverseβπ₯)
β Word (πΌ Γ
2o) β§ (π¦
β πΌ, π§ β 2o β¦
β¨π¦, (1o
β π§)β©):(πΌ Γ
2o)βΆ(πΌ
Γ 2o)) β ((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯)) β
Word (πΌ Γ
2o)) |
72 | 67, 70, 71 | syl2anc 584 |
. 2
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β ((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯)) β
Word (πΌ Γ
2o)) |
73 | 11 | adantr 481 |
. . . . 5
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β Word (πΌ Γ 2o) =
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
74 | 72, 73 | eleqtrd 2835 |
. . . 4
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β ((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯)) β
(Baseβ(freeMndβ(πΌ Γ 2o)))) |
75 | 2, 8, 22 | frmdadd 18732 |
. . . 4
β’ ((((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯)) β
(Baseβ(freeMndβ(πΌ Γ 2o))) β§ π₯ β
(Baseβ(freeMndβ(πΌ Γ 2o)))) β (((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯))(+gβ(freeMndβ(πΌ Γ 2o)))π₯) = (((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯)) ++ π₯)) |
76 | 74, 56, 75 | syl2anc 584 |
. . 3
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β (((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯))(+gβ(freeMndβ(πΌ Γ 2o)))π₯) = (((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯)) ++ π₯)) |
77 | 17 | eleq2d 2819 |
. . . . 5
β’ (πΌ β π β (π₯ β ( I βWord (πΌ Γ 2o)) β π₯ β Word (πΌ Γ 2o))) |
78 | 77 | biimpar 478 |
. . . 4
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β π₯ β ( I βWord (πΌ Γ
2o))) |
79 | | eqid 2732 |
. . . . 5
β’ (π£ β ( I βWord (πΌ Γ 2o)) β¦
(π β
(0...(β―βπ£)),
π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)βπ€)ββ©β©))) = (π£ β ( I βWord (πΌ Γ 2o)) β¦
(π β
(0...(β―βπ£)),
π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)βπ€)ββ©β©))) |
80 | 13, 3, 68, 79 | efginvrel1 19590 |
. . . 4
β’ (π₯ β ( I βWord (πΌ Γ 2o)) β
(((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯)) ++ π₯) βΌ
β
) |
81 | 78, 80 | syl 17 |
. . 3
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β (((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯)) ++ π₯) βΌ
β
) |
82 | 76, 81 | eqbrtrd 5169 |
. 2
β’ ((πΌ β π β§ π₯ β Word (πΌ Γ 2o)) β (((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β
(reverseβπ₯))(+gβ(freeMndβ(πΌ Γ 2o)))π₯) βΌ
β
) |
83 | 4, 11, 12, 20, 21, 24, 35, 50, 52, 65, 72, 82 | qusgrp2 18937 |
1
β’ (πΌ β π β (πΊ β Grp β§ [β
] βΌ =
(0gβπΊ))) |