Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’
(ExtStrCatβπ)
= (ExtStrCatβπ) |
2 | | funcrngcsetc.s |
. . . . . 6
β’ π = (SetCatβπ) |
3 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(ExtStrCatβπ)) = (Baseβ(ExtStrCatβπ)) |
4 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
5 | | funcrngcsetc.u |
. . . . . 6
β’ (π β π β WUni) |
6 | 1, 5 | estrcbas 18020 |
. . . . . . 7
β’ (π β π = (Baseβ(ExtStrCatβπ))) |
7 | 6 | mpteq1d 5204 |
. . . . . 6
β’ (π β (π₯ β π β¦ (Baseβπ₯)) = (π₯ β (Baseβ(ExtStrCatβπ)) β¦ (Baseβπ₯))) |
8 | | mpoeq12 7434 |
. . . . . . 7
β’ ((π =
(Baseβ(ExtStrCatβπ)) β§ π = (Baseβ(ExtStrCatβπ))) β (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯)))) = (π₯ β
(Baseβ(ExtStrCatβπ)), π¦ β (Baseβ(ExtStrCatβπ)) β¦ ( I βΎ
((Baseβπ¦)
βm (Baseβπ₯))))) |
9 | 6, 6, 8 | syl2anc 585 |
. . . . . 6
β’ (π β (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯)))) = (π₯ β
(Baseβ(ExtStrCatβπ)), π¦ β (Baseβ(ExtStrCatβπ)) β¦ ( I βΎ
((Baseβπ¦)
βm (Baseβπ₯))))) |
10 | 1, 2, 3, 4, 5, 7, 9 | funcestrcsetc 18045 |
. . . . 5
β’ (π β (π₯ β π β¦ (Baseβπ₯))((ExtStrCatβπ) Func π)(π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))) |
11 | | df-br 5110 |
. . . . 5
β’ ((π₯ β π β¦ (Baseβπ₯))((ExtStrCatβπ) Func π)(π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯)))) β
β¨(π₯ β π β¦ (Baseβπ₯)), (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))β©
β ((ExtStrCatβπ)
Func π)) |
12 | 10, 11 | sylib 217 |
. . . 4
β’ (π β β¨(π₯ β π β¦ (Baseβπ₯)), (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))β©
β ((ExtStrCatβπ)
Func π)) |
13 | | funcrngcsetc.r |
. . . . . . 7
β’ π
= (RngCatβπ) |
14 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
15 | 13, 14, 5 | rngcbas 46353 |
. . . . . 6
β’ (π β (Baseβπ
) = (π β© Rng)) |
16 | | incom 4165 |
. . . . . 6
β’ (π β© Rng) = (Rng β© π) |
17 | 15, 16 | eqtrdi 2789 |
. . . . 5
β’ (π β (Baseβπ
) = (Rng β© π)) |
18 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπ
) = (Hom
βπ
) |
19 | 13, 14, 5, 18 | rngchomfval 46354 |
. . . . 5
β’ (π β (Hom βπ
) = ( RngHomo βΎ
((Baseβπ
) Γ
(Baseβπ
)))) |
20 | 1, 5, 17, 19 | rnghmsubcsetc 46365 |
. . . 4
β’ (π β (Hom βπ
) β
(Subcatβ(ExtStrCatβπ))) |
21 | 12, 20 | funcres 17790 |
. . 3
β’ (π β (β¨(π₯ β π β¦ (Baseβπ₯)), (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))β©
βΎf (Hom βπ
)) β (((ExtStrCatβπ) βΎcat (Hom
βπ
)) Func π)) |
22 | | mptexg 7175 |
. . . . . 6
β’ (π β WUni β (π₯ β π β¦ (Baseβπ₯)) β V) |
23 | 5, 22 | syl 17 |
. . . . 5
β’ (π β (π₯ β π β¦ (Baseβπ₯)) β V) |
24 | | fvex 6859 |
. . . . . 6
β’ (Hom
βπ
) β
V |
25 | 24 | a1i 11 |
. . . . 5
β’ (π β (Hom βπ
) β V) |
26 | | mpoexga 8014 |
. . . . . 6
β’ ((π β WUni β§ π β WUni) β (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯)))) β
V) |
27 | 5, 5, 26 | syl2anc 585 |
. . . . 5
β’ (π β (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯)))) β
V) |
28 | 15, 19 | rnghmresfn 46351 |
. . . . 5
β’ (π β (Hom βπ
) Fn ((Baseβπ
) Γ (Baseβπ
))) |
29 | 23, 25, 27, 28 | resfval2 17787 |
. . . 4
β’ (π β (β¨(π₯ β π β¦ (Baseβπ₯)), (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))β©
βΎf (Hom βπ
)) = β¨((π₯ β π β¦ (Baseβπ₯)) βΎ (Baseβπ
)), (π β (Baseβπ
), π β (Baseβπ
) β¦ ((π(π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))π) βΎ (π(Hom βπ
)π)))β©) |
30 | | inss1 4192 |
. . . . . . . 8
β’ (π β© Rng) β π |
31 | 15, 30 | eqsstrdi 4002 |
. . . . . . 7
β’ (π β (Baseβπ
) β π) |
32 | 31 | resmptd 5998 |
. . . . . 6
β’ (π β ((π₯ β π β¦ (Baseβπ₯)) βΎ (Baseβπ
)) = (π₯ β (Baseβπ
) β¦ (Baseβπ₯))) |
33 | | funcrngcsetc.f |
. . . . . . 7
β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) |
34 | | funcrngcsetc.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ
) |
35 | 34 | a1i 11 |
. . . . . . . 8
β’ (π β π΅ = (Baseβπ
)) |
36 | 35 | mpteq1d 5204 |
. . . . . . 7
β’ (π β (π₯ β π΅ β¦ (Baseβπ₯)) = (π₯ β (Baseβπ
) β¦ (Baseβπ₯))) |
37 | 33, 36 | eqtr2d 2774 |
. . . . . 6
β’ (π β (π₯ β (Baseβπ
) β¦ (Baseβπ₯)) = πΉ) |
38 | 32, 37 | eqtrd 2773 |
. . . . 5
β’ (π β ((π₯ β π β¦ (Baseβπ₯)) βΎ (Baseβπ
)) = πΉ) |
39 | | funcrngcsetc.g |
. . . . . 6
β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RngHomo π¦)))) |
40 | | oveq1 7368 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ RngHomo π¦) = (π RngHomo π¦)) |
41 | 40 | reseq2d 5941 |
. . . . . . . 8
β’ (π₯ = π β ( I βΎ (π₯ RngHomo π¦)) = ( I βΎ (π RngHomo π¦))) |
42 | | oveq2 7369 |
. . . . . . . . 9
β’ (π¦ = π β (π RngHomo π¦) = (π RngHomo π)) |
43 | 42 | reseq2d 5941 |
. . . . . . . 8
β’ (π¦ = π β ( I βΎ (π RngHomo π¦)) = ( I βΎ (π RngHomo π))) |
44 | 41, 43 | cbvmpov 7456 |
. . . . . . 7
β’ (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RngHomo π¦))) = (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π))) |
45 | 44 | a1i 11 |
. . . . . 6
β’ (π β (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RngHomo π¦))) = (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))) |
46 | 34 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π΅) β π΅ = (Baseβπ
)) |
47 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯)))) = (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))) |
48 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π¦ = π β (Baseβπ¦) = (Baseβπ)) |
49 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (Baseβπ₯) = (Baseβπ)) |
50 | 48, 49 | oveqan12rd 7381 |
. . . . . . . . . . . 12
β’ ((π₯ = π β§ π¦ = π) β ((Baseβπ¦) βm (Baseβπ₯)) = ((Baseβπ) βm
(Baseβπ))) |
51 | 50 | reseq2d 5941 |
. . . . . . . . . . 11
β’ ((π₯ = π β§ π¦ = π) β ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) = ( I
βΎ ((Baseβπ)
βm (Baseβπ)))) |
52 | 51 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ (π₯ = π β§ π¦ = π)) β ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) = ( I
βΎ ((Baseβπ)
βm (Baseβπ)))) |
53 | 34, 31 | eqsstrid 3996 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β π) |
54 | 53 | sseld 3947 |
. . . . . . . . . . . . 13
β’ (π β (π β π΅ β π β π)) |
55 | 54 | com12 32 |
. . . . . . . . . . . 12
β’ (π β π΅ β (π β π β π)) |
56 | 55 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β π΅ β§ π β π΅) β (π β π β π)) |
57 | 56 | impcom 409 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π) |
58 | 53 | sseld 3947 |
. . . . . . . . . . . 12
β’ (π β (π β π΅ β π β π)) |
59 | 58 | adantld 492 |
. . . . . . . . . . 11
β’ (π β ((π β π΅ β§ π β π΅) β π β π)) |
60 | 59 | imp 408 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π) |
61 | | ovexd 7396 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((Baseβπ) βm (Baseβπ)) β V) |
62 | 61 | resiexd 7170 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β ( I βΎ ((Baseβπ) βm
(Baseβπ))) β
V) |
63 | 47, 52, 57, 60, 62 | ovmpod 7511 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))π) = ( I βΎ
((Baseβπ)
βm (Baseβπ)))) |
64 | 63 | reseq1d 5940 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((π(π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))π) βΎ (π(Hom βπ
)π)) = (( I βΎ ((Baseβπ) βm
(Baseβπ))) βΎ
(π(Hom βπ
)π))) |
65 | 5 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β WUni) |
66 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
67 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
68 | 13, 34, 65, 18, 66, 67 | rngchom 46355 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(Hom βπ
)π) = (π RngHomo π)) |
69 | 68 | reseq2d 5941 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (( I βΎ ((Baseβπ) βm
(Baseβπ))) βΎ
(π(Hom βπ
)π)) = (( I βΎ ((Baseβπ) βm
(Baseβπ))) βΎ
(π RngHomo π))) |
70 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
71 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
72 | 70, 71 | rnghmf 46287 |
. . . . . . . . . . 11
β’ (π β (π RngHomo π) β π:(Baseβπ)βΆ(Baseβπ)) |
73 | | fvex 6859 |
. . . . . . . . . . . . . 14
β’
(Baseβπ)
β V |
74 | | fvex 6859 |
. . . . . . . . . . . . . 14
β’
(Baseβπ)
β V |
75 | 73, 74 | pm3.2i 472 |
. . . . . . . . . . . . 13
β’
((Baseβπ)
β V β§ (Baseβπ) β V) |
76 | 75 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((Baseβπ) β V β§ (Baseβπ) β V)) |
77 | | elmapg 8784 |
. . . . . . . . . . . 12
β’
(((Baseβπ)
β V β§ (Baseβπ) β V) β (π β ((Baseβπ) βm (Baseβπ)) β π:(Baseβπ)βΆ(Baseβπ))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π β ((Baseβπ) βm (Baseβπ)) β π:(Baseβπ)βΆ(Baseβπ))) |
79 | 72, 78 | syl5ibr 246 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π β (π RngHomo π) β π β ((Baseβπ) βm (Baseβπ)))) |
80 | 79 | ssrdv 3954 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π RngHomo π) β ((Baseβπ) βm (Baseβπ))) |
81 | 80 | resabs1d 5972 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (( I βΎ ((Baseβπ) βm
(Baseβπ))) βΎ
(π RngHomo π)) = ( I βΎ (π RngHomo π))) |
82 | 64, 69, 81 | 3eqtrrd 2778 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β ( I βΎ (π RngHomo π)) = ((π(π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))π) βΎ (π(Hom βπ
)π))) |
83 | 35, 46, 82 | mpoeq123dva 7435 |
. . . . . 6
β’ (π β (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π))) = (π β (Baseβπ
), π β (Baseβπ
) β¦ ((π(π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))π) βΎ (π(Hom βπ
)π)))) |
84 | 39, 45, 83 | 3eqtrrd 2778 |
. . . . 5
β’ (π β (π β (Baseβπ
), π β (Baseβπ
) β¦ ((π(π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))π) βΎ (π(Hom βπ
)π))) = πΊ) |
85 | 38, 84 | opeq12d 4842 |
. . . 4
β’ (π β β¨((π₯ β π β¦ (Baseβπ₯)) βΎ (Baseβπ
)), (π β (Baseβπ
), π β (Baseβπ
) β¦ ((π(π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))π) βΎ (π(Hom βπ
)π)))β© = β¨πΉ, πΊβ©) |
86 | 29, 85 | eqtr2d 2774 |
. . 3
β’ (π β β¨πΉ, πΊβ© = (β¨(π₯ β π β¦ (Baseβπ₯)), (π₯ β π, π¦ β π β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))β©
βΎf (Hom βπ
))) |
87 | 13, 5, 15, 19 | rngcval 46350 |
. . . 4
β’ (π β π
= ((ExtStrCatβπ) βΎcat (Hom βπ
))) |
88 | 87 | oveq1d 7376 |
. . 3
β’ (π β (π
Func π) = (((ExtStrCatβπ) βΎcat (Hom βπ
)) Func π)) |
89 | 21, 86, 88 | 3eltr4d 2849 |
. 2
β’ (π β β¨πΉ, πΊβ© β (π
Func π)) |
90 | | df-br 5110 |
. 2
β’ (πΉ(π
Func π)πΊ β β¨πΉ, πΊβ© β (π
Func π)) |
91 | 89, 90 | sylibr 233 |
1
β’ (π β πΉ(π
Func π)πΊ) |