Step | Hyp | Ref
| Expression |
1 | | eqidd 2738 |
. 2
β’ (πΌ β π β (Baseβπ) = (Baseβπ)) |
2 | | eqidd 2738 |
. 2
β’ (πΌ β π β (+gβπ) = (+gβπ)) |
3 | | frmdmnd.m |
. . . . . 6
β’ π = (freeMndβπΌ) |
4 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
5 | | eqid 2737 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
6 | 3, 4, 5 | frmdadd 18666 |
. . . . 5
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(+gβπ)π¦) = (π₯ ++ π¦)) |
7 | 3, 4 | frmdelbas 18664 |
. . . . . 6
β’ (π₯ β (Baseβπ) β π₯ β Word πΌ) |
8 | 3, 4 | frmdelbas 18664 |
. . . . . 6
β’ (π¦ β (Baseβπ) β π¦ β Word πΌ) |
9 | | ccatcl 14463 |
. . . . . 6
β’ ((π₯ β Word πΌ β§ π¦ β Word πΌ) β (π₯ ++ π¦) β Word πΌ) |
10 | 7, 8, 9 | syl2an 597 |
. . . . 5
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯ ++ π¦) β Word πΌ) |
11 | 6, 10 | eqeltrd 2838 |
. . . 4
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(+gβπ)π¦) β Word πΌ) |
12 | 11 | 3adant1 1131 |
. . 3
β’ ((πΌ β π β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(+gβπ)π¦) β Word πΌ) |
13 | 3, 4 | frmdbas 18663 |
. . . 4
β’ (πΌ β π β (Baseβπ) = Word πΌ) |
14 | 13 | 3ad2ant1 1134 |
. . 3
β’ ((πΌ β π β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (Baseβπ) = Word πΌ) |
15 | 12, 14 | eleqtrrd 2841 |
. 2
β’ ((πΌ β π β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(+gβπ)π¦) β (Baseβπ)) |
16 | | simpr1 1195 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π₯ β (Baseβπ)) |
17 | 16, 7 | syl 17 |
. . . . 5
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π₯ β Word πΌ) |
18 | | simpr2 1196 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π¦ β (Baseβπ)) |
19 | 18, 8 | syl 17 |
. . . . 5
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π¦ β Word πΌ) |
20 | | simpr3 1197 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π§ β (Baseβπ)) |
21 | 3, 4 | frmdelbas 18664 |
. . . . . 6
β’ (π§ β (Baseβπ) β π§ β Word πΌ) |
22 | 20, 21 | syl 17 |
. . . . 5
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π§ β Word πΌ) |
23 | | ccatass 14477 |
. . . . 5
β’ ((π₯ β Word πΌ β§ π¦ β Word πΌ β§ π§ β Word πΌ) β ((π₯ ++ π¦) ++ π§) = (π₯ ++ (π¦ ++ π§))) |
24 | 17, 19, 22, 23 | syl3anc 1372 |
. . . 4
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯ ++ π¦) ++ π§) = (π₯ ++ (π¦ ++ π§))) |
25 | 16, 18, 10 | syl2anc 585 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯ ++ π¦) β Word πΌ) |
26 | 13 | adantr 482 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (Baseβπ) = Word πΌ) |
27 | 25, 26 | eleqtrrd 2841 |
. . . . 5
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯ ++ π¦) β (Baseβπ)) |
28 | 3, 4, 5 | frmdadd 18666 |
. . . . 5
β’ (((π₯ ++ π¦) β (Baseβπ) β§ π§ β (Baseβπ)) β ((π₯ ++ π¦)(+gβπ)π§) = ((π₯ ++ π¦) ++ π§)) |
29 | 27, 20, 28 | syl2anc 585 |
. . . 4
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯ ++ π¦)(+gβπ)π§) = ((π₯ ++ π¦) ++ π§)) |
30 | | ccatcl 14463 |
. . . . . . 7
β’ ((π¦ β Word πΌ β§ π§ β Word πΌ) β (π¦ ++ π§) β Word πΌ) |
31 | 19, 22, 30 | syl2anc 585 |
. . . . . 6
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π¦ ++ π§) β Word πΌ) |
32 | 31, 26 | eleqtrrd 2841 |
. . . . 5
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π¦ ++ π§) β (Baseβπ)) |
33 | 3, 4, 5 | frmdadd 18666 |
. . . . 5
β’ ((π₯ β (Baseβπ) β§ (π¦ ++ π§) β (Baseβπ)) β (π₯(+gβπ)(π¦ ++ π§)) = (π₯ ++ (π¦ ++ π§))) |
34 | 16, 32, 33 | syl2anc 585 |
. . . 4
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(+gβπ)(π¦ ++ π§)) = (π₯ ++ (π¦ ++ π§))) |
35 | 24, 29, 34 | 3eqtr4d 2787 |
. . 3
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯ ++ π¦)(+gβπ)π§) = (π₯(+gβπ)(π¦ ++ π§))) |
36 | 16, 18, 6 | syl2anc 585 |
. . . 4
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(+gβπ)π¦) = (π₯ ++ π¦)) |
37 | 36 | oveq1d 7373 |
. . 3
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(+gβπ)π¦)(+gβπ)π§) = ((π₯ ++ π¦)(+gβπ)π§)) |
38 | 3, 4, 5 | frmdadd 18666 |
. . . . 5
β’ ((π¦ β (Baseβπ) β§ π§ β (Baseβπ)) β (π¦(+gβπ)π§) = (π¦ ++ π§)) |
39 | 18, 20, 38 | syl2anc 585 |
. . . 4
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π¦(+gβπ)π§) = (π¦ ++ π§)) |
40 | 39 | oveq2d 7374 |
. . 3
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π₯(+gβπ)(π¦(+gβπ)π§)) = (π₯(+gβπ)(π¦ ++ π§))) |
41 | 35, 37, 40 | 3eqtr4d 2787 |
. 2
β’ ((πΌ β π β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π₯(+gβπ)π¦)(+gβπ)π§) = (π₯(+gβπ)(π¦(+gβπ)π§))) |
42 | | wrd0 14428 |
. . 3
β’ β
β Word πΌ |
43 | 42, 13 | eleqtrrid 2845 |
. 2
β’ (πΌ β π β β
β (Baseβπ)) |
44 | 3, 4, 5 | frmdadd 18666 |
. . . 4
β’ ((β
β (Baseβπ) β§
π₯ β (Baseβπ)) β
(β
(+gβπ)π₯) = (β
++ π₯)) |
45 | 43, 44 | sylan 581 |
. . 3
β’ ((πΌ β π β§ π₯ β (Baseβπ)) β (β
(+gβπ)π₯) = (β
++ π₯)) |
46 | 7 | adantl 483 |
. . . 4
β’ ((πΌ β π β§ π₯ β (Baseβπ)) β π₯ β Word πΌ) |
47 | | ccatlid 14475 |
. . . 4
β’ (π₯ β Word πΌ β (β
++ π₯) = π₯) |
48 | 46, 47 | syl 17 |
. . 3
β’ ((πΌ β π β§ π₯ β (Baseβπ)) β (β
++ π₯) = π₯) |
49 | 45, 48 | eqtrd 2777 |
. 2
β’ ((πΌ β π β§ π₯ β (Baseβπ)) β (β
(+gβπ)π₯) = π₯) |
50 | 3, 4, 5 | frmdadd 18666 |
. . . . 5
β’ ((π₯ β (Baseβπ) β§ β
β
(Baseβπ)) β
(π₯(+gβπ)β
) = (π₯ ++ β
)) |
51 | 50 | ancoms 460 |
. . . 4
β’ ((β
β (Baseβπ) β§
π₯ β (Baseβπ)) β (π₯(+gβπ)β
) = (π₯ ++ β
)) |
52 | 43, 51 | sylan 581 |
. . 3
β’ ((πΌ β π β§ π₯ β (Baseβπ)) β (π₯(+gβπ)β
) = (π₯ ++ β
)) |
53 | | ccatrid 14476 |
. . . 4
β’ (π₯ β Word πΌ β (π₯ ++ β
) = π₯) |
54 | 46, 53 | syl 17 |
. . 3
β’ ((πΌ β π β§ π₯ β (Baseβπ)) β (π₯ ++ β
) = π₯) |
55 | 52, 54 | eqtrd 2777 |
. 2
β’ ((πΌ β π β§ π₯ β (Baseβπ)) β (π₯(+gβπ)β
) = π₯) |
56 | 1, 2, 15, 41, 43, 49, 55 | ismndd 18579 |
1
β’ (πΌ β π β π β Mnd) |