Step | Hyp | Ref
| Expression |
1 | | funcrngcsetcALT.f |
. . . . . . 7
β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) |
2 | | fveq2 6839 |
. . . . . . . 8
β’ (π₯ = π’ β (Baseβπ₯) = (Baseβπ’)) |
3 | 2 | cbvmptv 5216 |
. . . . . . 7
β’ (π₯ β π΅ β¦ (Baseβπ₯)) = (π’ β π΅ β¦ (Baseβπ’)) |
4 | 1, 3 | eqtrdi 2793 |
. . . . . 6
β’ (π β πΉ = (π’ β π΅ β¦ (Baseβπ’))) |
5 | | coires1 6214 |
. . . . . . 7
β’ ((π’ β π β¦ (Baseβπ’)) β ( I βΎ π΅)) = ((π’ β π β¦ (Baseβπ’)) βΎ π΅) |
6 | | funcrngcsetcALT.r |
. . . . . . . . . . . 12
β’ π
= (RngCatβπ) |
7 | | funcrngcsetcALT.b |
. . . . . . . . . . . 12
β’ π΅ = (Baseβπ
) |
8 | | funcrngcsetcALT.u |
. . . . . . . . . . . 12
β’ (π β π β WUni) |
9 | 6, 7, 8 | rngcbas 46164 |
. . . . . . . . . . 11
β’ (π β π΅ = (π β© Rng)) |
10 | 9 | eleq2d 2823 |
. . . . . . . . . 10
β’ (π β (π₯ β π΅ β π₯ β (π β© Rng))) |
11 | | elin 3924 |
. . . . . . . . . . 11
β’ (π₯ β (π β© Rng) β (π₯ β π β§ π₯ β Rng)) |
12 | 11 | simplbi 498 |
. . . . . . . . . 10
β’ (π₯ β (π β© Rng) β π₯ β π) |
13 | 10, 12 | syl6bi 252 |
. . . . . . . . 9
β’ (π β (π₯ β π΅ β π₯ β π)) |
14 | 13 | ssrdv 3948 |
. . . . . . . 8
β’ (π β π΅ β π) |
15 | 14 | resmptd 5992 |
. . . . . . 7
β’ (π β ((π’ β π β¦ (Baseβπ’)) βΎ π΅) = (π’ β π΅ β¦ (Baseβπ’))) |
16 | 5, 15 | eqtr2id 2790 |
. . . . . 6
β’ (π β (π’ β π΅ β¦ (Baseβπ’)) = ((π’ β π β¦ (Baseβπ’)) β ( I βΎ π΅))) |
17 | 4, 16 | eqtrd 2777 |
. . . . 5
β’ (π β πΉ = ((π’ β π β¦ (Baseβπ’)) β ( I βΎ π΅))) |
18 | | funcrngcsetcALT.g |
. . . . . . 7
β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RngHomo π¦)))) |
19 | | coires1 6214 |
. . . . . . . . 9
β’ (( I
βΎ ((Baseβπ¦)
βm (Baseβπ₯))) β ( I βΎ (π₯ RngHomo π¦))) = (( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) βΎ
(π₯ RngHomo π¦)) |
20 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(Baseβπ₯) =
(Baseβπ₯) |
21 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(Baseβπ¦) =
(Baseβπ¦) |
22 | 20, 21 | rnghmf 46098 |
. . . . . . . . . . . 12
β’ (π§ β (π₯ RngHomo π¦) β π§:(Baseβπ₯)βΆ(Baseβπ¦)) |
23 | | fvex 6852 |
. . . . . . . . . . . . . 14
β’
(Baseβπ¦)
β V |
24 | | fvex 6852 |
. . . . . . . . . . . . . 14
β’
(Baseβπ₯)
β V |
25 | 23, 24 | pm3.2i 471 |
. . . . . . . . . . . . 13
β’
((Baseβπ¦)
β V β§ (Baseβπ₯) β V) |
26 | | elmapg 8736 |
. . . . . . . . . . . . 13
β’
(((Baseβπ¦)
β V β§ (Baseβπ₯) β V) β (π§ β ((Baseβπ¦) βm (Baseβπ₯)) β π§:(Baseβπ₯)βΆ(Baseβπ¦))) |
27 | 25, 26 | mp1i 13 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π§ β ((Baseβπ¦) βm (Baseβπ₯)) β π§:(Baseβπ₯)βΆ(Baseβπ¦))) |
28 | 22, 27 | syl5ibr 245 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π§ β (π₯ RngHomo π¦) β π§ β ((Baseβπ¦) βm (Baseβπ₯)))) |
29 | 28 | ssrdv 3948 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ RngHomo π¦) β ((Baseβπ¦) βm (Baseβπ₯))) |
30 | 29 | resabs1d 5966 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) βΎ
(π₯ RngHomo π¦)) = ( I βΎ (π₯ RngHomo π¦))) |
31 | 19, 30 | eqtr2id 2790 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β ( I βΎ (π₯ RngHomo π¦)) = (( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) β (
I βΎ (π₯ RngHomo π¦)))) |
32 | 31 | mpoeq3dva 7428 |
. . . . . . 7
β’ (π β (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯ RngHomo π¦))) = (π₯ β π΅, π¦ β π΅ β¦ (( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) β (
I βΎ (π₯ RngHomo π¦))))) |
33 | 18, 32 | eqtrd 2777 |
. . . . . 6
β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ (( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) β (
I βΎ (π₯ RngHomo π¦))))) |
34 | 7 | a1i 11 |
. . . . . . 7
β’ (π β π΅ = (Baseβπ
)) |
35 | 7 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β π΅ = (Baseβπ
)) |
36 | | fvresi 7115 |
. . . . . . . . . . . 12
β’ (π₯ β π΅ β (( I βΎ π΅)βπ₯) = π₯) |
37 | 36 | adantr 481 |
. . . . . . . . . . 11
β’ ((π₯ β π΅ β§ π¦ β π΅) β (( I βΎ π΅)βπ₯) = π₯) |
38 | 37 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (( I βΎ π΅)βπ₯) = π₯) |
39 | | fvresi 7115 |
. . . . . . . . . . . 12
β’ (π¦ β π΅ β (( I βΎ π΅)βπ¦) = π¦) |
40 | 39 | adantl 482 |
. . . . . . . . . . 11
β’ ((π₯ β π΅ β§ π¦ β π΅) β (( I βΎ π΅)βπ¦) = π¦) |
41 | 40 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (( I βΎ π΅)βπ¦) = π¦) |
42 | 38, 41 | oveq12d 7369 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((( I βΎ π΅)βπ₯)(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))(( I
βΎ π΅)βπ¦)) = (π₯(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))π¦)) |
43 | | eqidd 2738 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€)))) = (π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))) |
44 | | simprr 771 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π€ = π₯ β§ π§ = π¦)) β π§ = π¦) |
45 | 44 | fveq2d 6843 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π€ = π₯ β§ π§ = π¦)) β (Baseβπ§) = (Baseβπ¦)) |
46 | | simprl 769 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π€ = π₯ β§ π§ = π¦)) β π€ = π₯) |
47 | 46 | fveq2d 6843 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π€ = π₯ β§ π§ = π¦)) β (Baseβπ€) = (Baseβπ₯)) |
48 | 45, 47 | oveq12d 7369 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π€ = π₯ β§ π§ = π¦)) β ((Baseβπ§) βm (Baseβπ€)) = ((Baseβπ¦) βm
(Baseβπ₯))) |
49 | 48 | reseq2d 5935 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π€ = π₯ β§ π§ = π¦)) β ( I βΎ ((Baseβπ§) βm
(Baseβπ€))) = ( I
βΎ ((Baseβπ¦)
βm (Baseβπ₯)))) |
50 | 13 | com12 32 |
. . . . . . . . . . . 12
β’ (π₯ β π΅ β (π β π₯ β π)) |
51 | 50 | adantr 481 |
. . . . . . . . . . 11
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π β π₯ β π)) |
52 | 51 | impcom 408 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π₯ β π) |
53 | 9 | eleq2d 2823 |
. . . . . . . . . . . . 13
β’ (π β (π¦ β π΅ β π¦ β (π β© Rng))) |
54 | | elin 3924 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π β© Rng) β (π¦ β π β§ π¦ β Rng)) |
55 | 54 | simplbi 498 |
. . . . . . . . . . . . 13
β’ (π¦ β (π β© Rng) β π¦ β π) |
56 | 53, 55 | syl6bi 252 |
. . . . . . . . . . . 12
β’ (π β (π¦ β π΅ β π¦ β π)) |
57 | 56 | a1d 25 |
. . . . . . . . . . 11
β’ (π β (π₯ β π΅ β (π¦ β π΅ β π¦ β π))) |
58 | 57 | imp32 419 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π¦ β π) |
59 | | ovex 7384 |
. . . . . . . . . . . 12
β’
((Baseβπ¦)
βm (Baseβπ₯)) β V |
60 | 59 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((Baseβπ¦) βm (Baseβπ₯)) β V) |
61 | 60 | resiexd 7162 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) β
V) |
62 | 43, 49, 52, 58, 61 | ovmpod 7501 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))π¦) = ( I βΎ
((Baseβπ¦)
βm (Baseβπ₯)))) |
63 | 42, 62 | eqtr2d 2778 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) = ((( I
βΎ π΅)βπ₯)(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))(( I
βΎ π΅)βπ¦))) |
64 | | eqidd 2738 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π))) = (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))) |
65 | | oveq12 7360 |
. . . . . . . . . . . 12
β’ ((π = π₯ β§ π = π¦) β (π RngHomo π) = (π₯ RngHomo π¦)) |
66 | 65 | reseq2d 5935 |
. . . . . . . . . . 11
β’ ((π = π₯ β§ π = π¦) β ( I βΎ (π RngHomo π)) = ( I βΎ (π₯ RngHomo π¦))) |
67 | 66 | adantl 482 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π = π₯ β§ π = π¦)) β ( I βΎ (π RngHomo π)) = ( I βΎ (π₯ RngHomo π¦))) |
68 | | simprl 769 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π₯ β π΅) |
69 | | simprr 771 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π¦ β π΅) |
70 | | ovex 7384 |
. . . . . . . . . . . 12
β’ (π₯ RngHomo π¦) β V |
71 | 70 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ RngHomo π¦) β V) |
72 | 71 | resiexd 7162 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ( I βΎ (π₯ RngHomo π¦)) β V) |
73 | 64, 67, 68, 69, 72 | ovmpod 7501 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))π¦) = ( I βΎ (π₯ RngHomo π¦))) |
74 | 73 | eqcomd 2743 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ( I βΎ (π₯ RngHomo π¦)) = (π₯(π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))π¦)) |
75 | 63, 74 | coeq12d 5818 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) β (
I βΎ (π₯ RngHomo π¦))) = (((( I βΎ π΅)βπ₯)(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))(( I
βΎ π΅)βπ¦)) β (π₯(π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))π¦))) |
76 | 34, 35, 75 | mpoeq123dva 7425 |
. . . . . 6
β’ (π β (π₯ β π΅, π¦ β π΅ β¦ (( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))) β (
I βΎ (π₯ RngHomo π¦)))) = (π₯ β (Baseβπ
), π¦ β (Baseβπ
) β¦ (((( I βΎ π΅)βπ₯)(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))(( I
βΎ π΅)βπ¦)) β (π₯(π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))π¦)))) |
77 | 33, 76 | eqtrd 2777 |
. . . . 5
β’ (π β πΊ = (π₯ β (Baseβπ
), π¦ β (Baseβπ
) β¦ (((( I βΎ π΅)βπ₯)(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))(( I
βΎ π΅)βπ¦)) β (π₯(π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))π¦)))) |
78 | 17, 77 | opeq12d 4836 |
. . . 4
β’ (π β β¨πΉ, πΊβ© = β¨((π’ β π β¦ (Baseβπ’)) β ( I βΎ π΅)), (π₯ β (Baseβπ
), π¦ β (Baseβπ
) β¦ (((( I βΎ π΅)βπ₯)(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))(( I
βΎ π΅)βπ¦)) β (π₯(π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))π¦)))β©) |
79 | | eqid 2737 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
80 | | eqid 2737 |
. . . . . 6
β’
(ExtStrCatβπ)
= (ExtStrCatβπ) |
81 | | eqidd 2738 |
. . . . . 6
β’ (π β ( I βΎ π΅) = ( I βΎ π΅)) |
82 | | eqidd 2738 |
. . . . . 6
β’ (π β (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π))) = (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))) |
83 | 6, 80, 7, 8, 81, 82 | rngcifuestrc 46196 |
. . . . 5
β’ (π β ( I βΎ π΅)(π
Func (ExtStrCatβπ))(π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))) |
84 | | funcrngcsetcALT.s |
. . . . . 6
β’ π = (SetCatβπ) |
85 | | eqid 2737 |
. . . . . 6
β’
(Baseβ(ExtStrCatβπ)) = (Baseβ(ExtStrCatβπ)) |
86 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
87 | 80, 8 | estrcbas 17972 |
. . . . . . 7
β’ (π β π = (Baseβ(ExtStrCatβπ))) |
88 | 87 | mpteq1d 5198 |
. . . . . 6
β’ (π β (π’ β π β¦ (Baseβπ’)) = (π’ β (Baseβ(ExtStrCatβπ)) β¦ (Baseβπ’))) |
89 | | fveq2 6839 |
. . . . . . . . . . 11
β’ (π€ = π’ β (Baseβπ€) = (Baseβπ’)) |
90 | 89 | oveq2d 7367 |
. . . . . . . . . 10
β’ (π€ = π’ β ((Baseβπ§) βm (Baseβπ€)) = ((Baseβπ§) βm
(Baseβπ’))) |
91 | 90 | reseq2d 5935 |
. . . . . . . . 9
β’ (π€ = π’ β ( I βΎ ((Baseβπ§) βm
(Baseβπ€))) = ( I
βΎ ((Baseβπ§)
βm (Baseβπ’)))) |
92 | | fveq2 6839 |
. . . . . . . . . . 11
β’ (π§ = π£ β (Baseβπ§) = (Baseβπ£)) |
93 | 92 | oveq1d 7366 |
. . . . . . . . . 10
β’ (π§ = π£ β ((Baseβπ§) βm (Baseβπ’)) = ((Baseβπ£) βm
(Baseβπ’))) |
94 | 93 | reseq2d 5935 |
. . . . . . . . 9
β’ (π§ = π£ β ( I βΎ ((Baseβπ§) βm
(Baseβπ’))) = ( I
βΎ ((Baseβπ£)
βm (Baseβπ’)))) |
95 | 91, 94 | cbvmpov 7446 |
. . . . . . . 8
β’ (π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€)))) = (π’ β π, π£ β π β¦ ( I βΎ ((Baseβπ£) βm
(Baseβπ’)))) |
96 | 95 | a1i 11 |
. . . . . . 7
β’ (π β (π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€)))) = (π’ β π, π£ β π β¦ ( I βΎ ((Baseβπ£) βm
(Baseβπ’))))) |
97 | | eqidd 2738 |
. . . . . . . 8
β’ (π β ( I βΎ
((Baseβπ£)
βm (Baseβπ’))) = ( I βΎ ((Baseβπ£) βm
(Baseβπ’)))) |
98 | 87, 87, 97 | mpoeq123dv 7426 |
. . . . . . 7
β’ (π β (π’ β π, π£ β π β¦ ( I βΎ ((Baseβπ£) βm
(Baseβπ’)))) = (π’ β
(Baseβ(ExtStrCatβπ)), π£ β (Baseβ(ExtStrCatβπ)) β¦ ( I βΎ
((Baseβπ£)
βm (Baseβπ’))))) |
99 | 96, 98 | eqtrd 2777 |
. . . . . 6
β’ (π β (π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€)))) = (π’ β
(Baseβ(ExtStrCatβπ)), π£ β (Baseβ(ExtStrCatβπ)) β¦ ( I βΎ
((Baseβπ£)
βm (Baseβπ’))))) |
100 | 80, 84, 85, 86, 8, 88, 99 | funcestrcsetc 17997 |
. . . . 5
β’ (π β (π’ β π β¦ (Baseβπ’))((ExtStrCatβπ) Func π)(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))) |
101 | 79, 83, 100 | cofuval2 17733 |
. . . 4
β’ (π β (β¨(π’ β π β¦ (Baseβπ’)), (π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))β©
βfunc β¨( I βΎ π΅), (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))β©) = β¨((π’ β π β¦ (Baseβπ’)) β ( I βΎ π΅)), (π₯ β (Baseβπ
), π¦ β (Baseβπ
) β¦ (((( I βΎ π΅)βπ₯)(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))(( I
βΎ π΅)βπ¦)) β (π₯(π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))π¦)))β©) |
102 | 78, 101 | eqtr4d 2780 |
. . 3
β’ (π β β¨πΉ, πΊβ© = (β¨(π’ β π β¦ (Baseβπ’)), (π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))β©
βfunc β¨( I βΎ π΅), (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))β©)) |
103 | | df-br 5104 |
. . . . 5
β’ (( I
βΎ π΅)(π
Func (ExtStrCatβπ))(π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π))) β β¨( I βΎ π΅), (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))β© β (π
Func (ExtStrCatβπ))) |
104 | 83, 103 | sylib 217 |
. . . 4
β’ (π β β¨( I βΎ π΅), (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))β© β (π
Func (ExtStrCatβπ))) |
105 | | df-br 5104 |
. . . . 5
β’ ((π’ β π β¦ (Baseβπ’))((ExtStrCatβπ) Func π)(π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€)))) β
β¨(π’ β π β¦ (Baseβπ’)), (π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))β©
β ((ExtStrCatβπ)
Func π)) |
106 | 100, 105 | sylib 217 |
. . . 4
β’ (π β β¨(π’ β π β¦ (Baseβπ’)), (π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))β©
β ((ExtStrCatβπ)
Func π)) |
107 | 104, 106 | cofucl 17734 |
. . 3
β’ (π β (β¨(π’ β π β¦ (Baseβπ’)), (π€ β π, π§ β π β¦ ( I βΎ ((Baseβπ§) βm
(Baseβπ€))))β©
βfunc β¨( I βΎ π΅), (π β π΅, π β π΅ β¦ ( I βΎ (π RngHomo π)))β©) β (π
Func π)) |
108 | 102, 107 | eqeltrd 2838 |
. 2
β’ (π β β¨πΉ, πΊβ© β (π
Func π)) |
109 | | df-br 5104 |
. 2
β’ (πΉ(π
Func π)πΊ β β¨πΉ, πΊβ© β (π
Func π)) |
110 | 108, 109 | sylibr 233 |
1
β’ (π β πΉ(π
Func π)πΊ) |