Step | Hyp | Ref
| Expression |
1 | | frmdplusg.p |
. . . 4
β’ + =
(+gβπ) |
2 | | frmdbas.m |
. . . . . 6
β’ π = (freeMndβπΌ) |
3 | | frmdbas.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
4 | 2, 3 | frmdbas 18667 |
. . . . . 6
β’ (πΌ β V β π΅ = Word πΌ) |
5 | | eqid 2733 |
. . . . . 6
β’ ( ++
βΎ (π΅ Γ π΅)) = ( ++ βΎ (π΅ Γ π΅)) |
6 | 2, 4, 5 | frmdval 18666 |
. . . . 5
β’ (πΌ β V β π = {β¨(Baseβndx),
π΅β©,
β¨(+gβndx), ( ++ βΎ (π΅ Γ π΅))β©}) |
7 | 6 | fveq2d 6847 |
. . . 4
β’ (πΌ β V β
(+gβπ) =
(+gβ{β¨(Baseβndx), π΅β©, β¨(+gβndx), (
++ βΎ (π΅ Γ π΅))β©})) |
8 | 1, 7 | eqtrid 2785 |
. . 3
β’ (πΌ β V β + =
(+gβ{β¨(Baseβndx), π΅β©, β¨(+gβndx), (
++ βΎ (π΅ Γ π΅))β©})) |
9 | | wrdexg 14418 |
. . . 4
β’ (πΌ β V β Word πΌ β V) |
10 | | ccatfn 14466 |
. . . . . . 7
β’ ++ Fn (V
Γ V) |
11 | | xpss 5650 |
. . . . . . 7
β’ (π΅ Γ π΅) β (V Γ V) |
12 | | fnssres 6625 |
. . . . . . 7
β’ (( ++ Fn
(V Γ V) β§ (π΅
Γ π΅) β (V
Γ V)) β ( ++ βΎ (π΅ Γ π΅)) Fn (π΅ Γ π΅)) |
13 | 10, 11, 12 | mp2an 691 |
. . . . . 6
β’ ( ++
βΎ (π΅ Γ π΅)) Fn (π΅ Γ π΅) |
14 | | ovres 7521 |
. . . . . . . 8
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯( ++ βΎ (π΅ Γ π΅))π¦) = (π₯ ++ π¦)) |
15 | 2, 3 | frmdelbas 18668 |
. . . . . . . . 9
β’ (π₯ β π΅ β π₯ β Word πΌ) |
16 | 2, 3 | frmdelbas 18668 |
. . . . . . . . 9
β’ (π¦ β π΅ β π¦ β Word πΌ) |
17 | | ccatcl 14468 |
. . . . . . . . 9
β’ ((π₯ β Word πΌ β§ π¦ β Word πΌ) β (π₯ ++ π¦) β Word πΌ) |
18 | 15, 16, 17 | syl2an 597 |
. . . . . . . 8
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ ++ π¦) β Word πΌ) |
19 | 14, 18 | eqeltrd 2834 |
. . . . . . 7
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯( ++ βΎ (π΅ Γ π΅))π¦) β Word πΌ) |
20 | 19 | rgen2 3191 |
. . . . . 6
β’
βπ₯ β
π΅ βπ¦ β π΅ (π₯( ++ βΎ (π΅ Γ π΅))π¦) β Word πΌ |
21 | | ffnov 7484 |
. . . . . 6
β’ (( ++
βΎ (π΅ Γ π΅)):(π΅ Γ π΅)βΆWord πΌ β (( ++ βΎ (π΅ Γ π΅)) Fn (π΅ Γ π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯( ++ βΎ (π΅ Γ π΅))π¦) β Word πΌ)) |
22 | 13, 20, 21 | mpbir2an 710 |
. . . . 5
β’ ( ++
βΎ (π΅ Γ π΅)):(π΅ Γ π΅)βΆWord πΌ |
23 | 3 | fvexi 6857 |
. . . . . 6
β’ π΅ β V |
24 | 23, 23 | xpex 7688 |
. . . . 5
β’ (π΅ Γ π΅) β V |
25 | | fex2 7871 |
. . . . 5
β’ ((( ++
βΎ (π΅ Γ π΅)):(π΅ Γ π΅)βΆWord πΌ β§ (π΅ Γ π΅) β V β§ Word πΌ β V) β ( ++ βΎ (π΅ Γ π΅)) β V) |
26 | 22, 24, 25 | mp3an12 1452 |
. . . 4
β’ (Word
πΌ β V β ( ++
βΎ (π΅ Γ π΅)) β V) |
27 | | eqid 2733 |
. . . . 5
β’
{β¨(Baseβndx), π΅β©, β¨(+gβndx), (
++ βΎ (π΅ Γ π΅))β©} =
{β¨(Baseβndx), π΅β©, β¨(+gβndx), (
++ βΎ (π΅ Γ π΅))β©} |
28 | 27 | grpplusg 17174 |
. . . 4
β’ (( ++
βΎ (π΅ Γ π΅)) β V β ( ++ βΎ
(π΅ Γ π΅)) =
(+gβ{β¨(Baseβndx), π΅β©, β¨(+gβndx), (
++ βΎ (π΅ Γ π΅))β©})) |
29 | 9, 26, 28 | 3syl 18 |
. . 3
β’ (πΌ β V β ( ++ βΎ
(π΅ Γ π΅)) =
(+gβ{β¨(Baseβndx), π΅β©, β¨(+gβndx), (
++ βΎ (π΅ Γ π΅))β©})) |
30 | 8, 29 | eqtr4d 2776 |
. 2
β’ (πΌ β V β + = ( ++
βΎ (π΅ Γ π΅))) |
31 | | fvprc 6835 |
. . . . . . 7
β’ (Β¬
πΌ β V β
(freeMndβπΌ) =
β
) |
32 | 2, 31 | eqtrid 2785 |
. . . . . 6
β’ (Β¬
πΌ β V β π = β
) |
33 | 32 | fveq2d 6847 |
. . . . 5
β’ (Β¬
πΌ β V β
(+gβπ) =
(+gββ
)) |
34 | 1, 33 | eqtrid 2785 |
. . . 4
β’ (Β¬
πΌ β V β + =
(+gββ
)) |
35 | | res0 5942 |
. . . . 5
β’ ( ++
βΎ β
) = β
|
36 | | plusgid 17165 |
. . . . . 6
β’
+g = Slot (+gβndx) |
37 | 36 | str0 17066 |
. . . . 5
β’ β
=
(+gββ
) |
38 | 35, 37 | eqtr2i 2762 |
. . . 4
β’
(+gββ
) = ( ++ βΎ β
) |
39 | 34, 38 | eqtrdi 2789 |
. . 3
β’ (Β¬
πΌ β V β + = ( ++
βΎ β
)) |
40 | 32 | fveq2d 6847 |
. . . . . . 7
β’ (Β¬
πΌ β V β
(Baseβπ) =
(Baseββ
)) |
41 | | base0 17093 |
. . . . . . 7
β’ β
=
(Baseββ
) |
42 | 40, 3, 41 | 3eqtr4g 2798 |
. . . . . 6
β’ (Β¬
πΌ β V β π΅ = β
) |
43 | 42 | xpeq2d 5664 |
. . . . 5
β’ (Β¬
πΌ β V β (π΅ Γ π΅) = (π΅ Γ β
)) |
44 | | xp0 6111 |
. . . . 5
β’ (π΅ Γ β
) =
β
|
45 | 43, 44 | eqtrdi 2789 |
. . . 4
β’ (Β¬
πΌ β V β (π΅ Γ π΅) = β
) |
46 | 45 | reseq2d 5938 |
. . 3
β’ (Β¬
πΌ β V β ( ++
βΎ (π΅ Γ π΅)) = ( ++ βΎ
β
)) |
47 | 39, 46 | eqtr4d 2776 |
. 2
β’ (Β¬
πΌ β V β + = ( ++
βΎ (π΅ Γ π΅))) |
48 | 30, 47 | pm2.61i 182 |
1
β’ + = ( ++
βΎ (π΅ Γ π΅)) |