Step | Hyp | Ref
| Expression |
1 | | opprabs.4 |
. . . . . 6
β’ (π β Β· Fn (π΅ Γ π΅)) |
2 | | eqid 2731 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβπ
) |
3 | | opprabs.m |
. . . . . . . . 9
β’ Β· =
(.rβπ
) |
4 | | opprabs.o |
. . . . . . . . 9
β’ π =
(opprβπ
) |
5 | | eqid 2731 |
. . . . . . . . 9
β’
(.rβπ) = (.rβπ) |
6 | 2, 3, 4, 5 | opprmulfval 20104 |
. . . . . . . 8
β’
(.rβπ) = tpos Β· |
7 | 6 | tposeqi 8226 |
. . . . . . 7
β’ tpos
(.rβπ) =
tpos tpos Β· |
8 | | fnrel 6640 |
. . . . . . . 8
β’ ( Β· Fn
(π΅ Γ π΅) β Rel Β· ) |
9 | | relxp 5687 |
. . . . . . . . 9
β’ Rel
(π΅ Γ π΅) |
10 | | fndm 6641 |
. . . . . . . . . 10
β’ ( Β· Fn
(π΅ Γ π΅) β dom Β· = (π΅ Γ π΅)) |
11 | 10 | releqd 5770 |
. . . . . . . . 9
β’ ( Β· Fn
(π΅ Γ π΅) β (Rel dom Β· β
Rel (π΅ Γ π΅))) |
12 | 9, 11 | mpbiri 257 |
. . . . . . . 8
β’ ( Β· Fn
(π΅ Γ π΅) β Rel dom Β·
) |
13 | | tpostpos2 8214 |
. . . . . . . 8
β’ ((Rel
Β·
β§ Rel dom Β· ) β tpos tpos
Β·
= Β· ) |
14 | 8, 12, 13 | syl2anc 584 |
. . . . . . 7
β’ ( Β· Fn
(π΅ Γ π΅) β tpos tpos Β· =
Β·
) |
15 | 7, 14 | eqtrid 2783 |
. . . . . 6
β’ ( Β· Fn
(π΅ Γ π΅) β tpos
(.rβπ) =
Β·
) |
16 | 1, 15 | syl 17 |
. . . . 5
β’ (π β tpos
(.rβπ) =
Β·
) |
17 | 16, 3 | eqtrdi 2787 |
. . . 4
β’ (π β tpos
(.rβπ) =
(.rβπ
)) |
18 | 17 | opeq2d 4873 |
. . 3
β’ (π β
β¨(.rβndx), tpos (.rβπ)β© = β¨(.rβndx),
(.rβπ
)β©) |
19 | 18 | oveq2d 7409 |
. 2
β’ (π β (π
sSet β¨(.rβndx), tpos
(.rβπ)β©) = (π
sSet β¨(.rβndx),
(.rβπ
)β©)) |
20 | | opprabs.1 |
. . 3
β’ (π β π
β π) |
21 | 4, 2 | opprbas 20109 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ) |
22 | | eqid 2731 |
. . . . . 6
β’
(opprβπ) = (opprβπ) |
23 | 21, 5, 22 | opprval 20103 |
. . . . 5
β’
(opprβπ) = (π sSet β¨(.rβndx), tpos
(.rβπ)β©) |
24 | 2, 3, 4 | opprval 20103 |
. . . . . 6
β’ π = (π
sSet β¨(.rβndx), tpos
Β·
β©) |
25 | 24 | oveq1i 7403 |
. . . . 5
β’ (π sSet
β¨(.rβndx), tpos (.rβπ)β©) = ((π
sSet β¨(.rβndx), tpos
Β·
β©) sSet β¨(.rβndx), tpos (.rβπ)β©) |
26 | 23, 25 | eqtri 2759 |
. . . 4
β’
(opprβπ) = ((π
sSet β¨(.rβndx), tpos
Β·
β©) sSet β¨(.rβndx), tpos (.rβπ)β©) |
27 | | fvex 6891 |
. . . . . 6
β’
(.rβπ) β V |
28 | 27 | tposex 8227 |
. . . . 5
β’ tpos
(.rβπ)
β V |
29 | | setsabs 17094 |
. . . . 5
β’ ((π
β π β§ tpos (.rβπ) β V) β ((π
sSet
β¨(.rβndx), tpos Β· β©) sSet
β¨(.rβndx), tpos (.rβπ)β©) = (π
sSet β¨(.rβndx), tpos
(.rβπ)β©)) |
30 | 28, 29 | mpan2 689 |
. . . 4
β’ (π
β π β ((π
sSet β¨(.rβndx), tpos
Β·
β©) sSet β¨(.rβndx), tpos (.rβπ)β©) = (π
sSet β¨(.rβndx), tpos
(.rβπ)β©)) |
31 | 26, 30 | eqtrid 2783 |
. . 3
β’ (π
β π β (opprβπ) = (π
sSet β¨(.rβndx), tpos
(.rβπ)β©)) |
32 | 20, 31 | syl 17 |
. 2
β’ (π β
(opprβπ) = (π
sSet β¨(.rβndx), tpos
(.rβπ)β©)) |
33 | | mulridx 17221 |
. . 3
β’
.r = Slot (.rβndx) |
34 | | opprabs.2 |
. . 3
β’ (π β Fun π
) |
35 | | opprabs.3 |
. . 3
β’ (π β (.rβndx)
β dom π
) |
36 | 33, 20, 34, 35 | setsidvald 17114 |
. 2
β’ (π β π
= (π
sSet β¨(.rβndx),
(.rβπ
)β©)) |
37 | 19, 32, 36 | 3eqtr4rd 2782 |
1
β’ (π β π
= (opprβπ)) |