Step | Hyp | Ref
| Expression |
1 | | psrring.s |
. . 3
โข ๐ = (๐ผ mPwSer ๐
) |
2 | | psrring.i |
. . 3
โข (๐ โ ๐ผ โ ๐) |
3 | | psrring.r |
. . 3
โข (๐ โ ๐
โ Ring) |
4 | | psrass.d |
. . 3
โข ๐ท = {๐ โ (โ0
โm ๐ผ)
โฃ (โก๐ โ โ) โ
Fin} |
5 | | psrass.t |
. . 3
โข ร =
(.rโ๐) |
6 | | psrass.b |
. . 3
โข ๐ต = (Baseโ๐) |
7 | | psrass.x |
. . 3
โข (๐ โ ๐ โ ๐ต) |
8 | | psrass.y |
. . 3
โข (๐ โ ๐ โ ๐ต) |
9 | | psrass.k |
. . 3
โข ๐พ = (Baseโ๐
) |
10 | | psrass.n |
. . 3
โข ยท = (
ยท๐ โ๐) |
11 | | psrass.a |
. . 3
โข (๐ โ ๐ด โ ๐พ) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | psrass23l 21393 |
. 2
โข (๐ โ ((๐ด ยท ๐) ร ๐) = (๐ด ยท (๐ ร ๐))) |
13 | | eqid 2733 |
. . . . . . . . . 10
โข
(Baseโ๐
) =
(Baseโ๐
) |
14 | | eqid 2733 |
. . . . . . . . . 10
โข
(.rโ๐
) = (.rโ๐
) |
15 | 11 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ท) โ ๐ด โ ๐พ) |
16 | 15, 9 | eleqtrdi 2844 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ท) โ ๐ด โ (Baseโ๐
)) |
17 | 16 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ด โ (Baseโ๐
)) |
18 | 8 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ โ ๐ต) |
19 | | ssrab2 4038 |
. . . . . . . . . . 11
โข {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โ ๐ท |
20 | | simplr 768 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ โ ๐ท) |
21 | | simpr 486 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) |
22 | | eqid 2733 |
. . . . . . . . . . . . 13
โข {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} = {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} |
23 | 4, 22 | psrbagconcl 21352 |
. . . . . . . . . . . 12
โข ((๐ โ ๐ท โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (๐ โf โ ๐ฅ) โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) |
24 | 20, 21, 23 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (๐ โf โ ๐ฅ) โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) |
25 | 19, 24 | sselid 3943 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (๐ โf โ ๐ฅ) โ ๐ท) |
26 | 1, 10, 13, 6, 14, 4, 17, 18, 25 | psrvscaval 21376 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ((๐ด ยท ๐)โ(๐ โf โ ๐ฅ)) = (๐ด(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) |
27 | 26 | oveq2d 7374 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ((๐โ๐ฅ)(.rโ๐
)((๐ด ยท ๐)โ(๐ โf โ ๐ฅ))) = ((๐โ๐ฅ)(.rโ๐
)(๐ด(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) |
28 | 7 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ โ ๐ต) |
29 | 1, 13, 4, 6, 28 | psrelbas 21363 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐:๐ทโถ(Baseโ๐
)) |
30 | 19, 21 | sselid 3943 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ฅ โ ๐ท) |
31 | 29, 30 | ffvelcdmd 7037 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (๐โ๐ฅ) โ (Baseโ๐
)) |
32 | 1, 13, 4, 6, 18 | psrelbas 21363 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐:๐ทโถ(Baseโ๐
)) |
33 | 32, 25 | ffvelcdmd 7037 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (๐โ(๐ โf โ ๐ฅ)) โ (Baseโ๐
)) |
34 | | psrcom.c |
. . . . . . . . . . 11
โข (๐ โ ๐
โ CRing) |
35 | 34 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐
โ CRing) |
36 | 13, 14 | crngcom 19987 |
. . . . . . . . . . 11
โข ((๐
โ CRing โง ๐ข โ (Baseโ๐
) โง ๐ฃ โ (Baseโ๐
)) โ (๐ข(.rโ๐
)๐ฃ) = (๐ฃ(.rโ๐
)๐ข)) |
37 | 36 | 3expb 1121 |
. . . . . . . . . 10
โข ((๐
โ CRing โง (๐ข โ (Baseโ๐
) โง ๐ฃ โ (Baseโ๐
))) โ (๐ข(.rโ๐
)๐ฃ) = (๐ฃ(.rโ๐
)๐ข)) |
38 | 35, 37 | sylan 581 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โง (๐ข โ (Baseโ๐
) โง ๐ฃ โ (Baseโ๐
))) โ (๐ข(.rโ๐
)๐ฃ) = (๐ฃ(.rโ๐
)๐ข)) |
39 | 3 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐
โ Ring) |
40 | 13, 14 | ringass 19989 |
. . . . . . . . . 10
โข ((๐
โ Ring โง (๐ข โ (Baseโ๐
) โง ๐ฃ โ (Baseโ๐
) โง ๐ค โ (Baseโ๐
))) โ ((๐ข(.rโ๐
)๐ฃ)(.rโ๐
)๐ค) = (๐ข(.rโ๐
)(๐ฃ(.rโ๐
)๐ค))) |
41 | 39, 40 | sylan 581 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โง (๐ข โ (Baseโ๐
) โง ๐ฃ โ (Baseโ๐
) โง ๐ค โ (Baseโ๐
))) โ ((๐ข(.rโ๐
)๐ฃ)(.rโ๐
)๐ค) = (๐ข(.rโ๐
)(๐ฃ(.rโ๐
)๐ค))) |
42 | 31, 17, 33, 38, 41 | caov12d 7576 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ((๐โ๐ฅ)(.rโ๐
)(๐ด(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) = (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) |
43 | 27, 42 | eqtrd 2773 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ((๐โ๐ฅ)(.rโ๐
)((๐ด ยท ๐)โ(๐ โf โ ๐ฅ))) = (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) |
44 | 43 | mpteq2dva 5206 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ท) โ (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)((๐ด ยท ๐)โ(๐ โf โ ๐ฅ)))) = (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))) |
45 | 44 | oveq2d 7374 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)((๐ด ยท ๐)โ(๐ โf โ ๐ฅ))))) = (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))))) |
46 | | eqid 2733 |
. . . . . 6
โข
(0gโ๐
) = (0gโ๐
) |
47 | | eqid 2733 |
. . . . . 6
โข
(+gโ๐
) = (+gโ๐
) |
48 | 3 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ท) โ ๐
โ Ring) |
49 | 4 | psrbaglefi 21350 |
. . . . . . 7
โข (๐ โ ๐ท โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โ Fin) |
50 | 49 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ท) โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โ Fin) |
51 | 13, 14 | ringcl 19986 |
. . . . . . 7
โข ((๐
โ Ring โง (๐โ๐ฅ) โ (Baseโ๐
) โง (๐โ(๐ โf โ ๐ฅ)) โ (Baseโ๐
)) โ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))) โ (Baseโ๐
)) |
52 | 39, 31, 33, 51 | syl3anc 1372 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))) โ (Baseโ๐
)) |
53 | | ovex 7391 |
. . . . . . . . . . 11
โข
(โ0 โm ๐ผ) โ V |
54 | 4, 53 | rabex2 5292 |
. . . . . . . . . 10
โข ๐ท โ V |
55 | 54 | mptrabex 7176 |
. . . . . . . . 9
โข (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โ V |
56 | | funmpt 6540 |
. . . . . . . . 9
โข Fun
(๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) |
57 | | fvex 6856 |
. . . . . . . . 9
โข
(0gโ๐
) โ V |
58 | 55, 56, 57 | 3pm3.2i 1340 |
. . . . . . . 8
โข ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โ V โง Fun (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โง
(0gโ๐
)
โ V) |
59 | 58 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ท) โ ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โ V โง Fun (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โง
(0gโ๐
)
โ V)) |
60 | | suppssdm 8109 |
. . . . . . . . 9
โข ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) supp
(0gโ๐
))
โ dom (๐ฅ โ
{๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) |
61 | | eqid 2733 |
. . . . . . . . . 10
โข (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) = (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) |
62 | 61 | dmmptss 6194 |
. . . . . . . . 9
โข dom
(๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} |
63 | 60, 62 | sstri 3954 |
. . . . . . . 8
โข ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) supp
(0gโ๐
))
โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} |
64 | 63 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ท) โ ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) supp
(0gโ๐
))
โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) |
65 | | suppssfifsupp 9325 |
. . . . . . 7
โข ((((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โ V โง Fun (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โง
(0gโ๐
)
โ V) โง ({๐ฆ โ
๐ท โฃ ๐ฆ โr โค ๐} โ Fin โง ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) supp
(0gโ๐
))
โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐})) โ (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) finSupp
(0gโ๐
)) |
66 | 59, 50, 64, 65 | syl12anc 836 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ท) โ (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) finSupp
(0gโ๐
)) |
67 | 13, 46, 47, 14, 48, 50, 16, 52, 66 | gsummulc2 20036 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))) = (๐ด(.rโ๐
)(๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))))) |
68 | 45, 67 | eqtrd 2773 |
. . . 4
โข ((๐ โง ๐ โ ๐ท) โ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)((๐ด ยท ๐)โ(๐ โf โ ๐ฅ))))) = (๐ด(.rโ๐
)(๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))))) |
69 | 68 | mpteq2dva 5206 |
. . 3
โข (๐ โ (๐ โ ๐ท โฆ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)((๐ด ยท ๐)โ(๐ โf โ ๐ฅ)))))) = (๐ โ ๐ท โฆ (๐ด(.rโ๐
)(๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))))) |
70 | 1, 10, 9, 6, 3, 11,
8 | psrvscacl 21377 |
. . . 4
โข (๐ โ (๐ด ยท ๐) โ ๐ต) |
71 | 1, 6, 14, 5, 4, 7,
70 | psrmulfval 21369 |
. . 3
โข (๐ โ (๐ ร (๐ด ยท ๐)) = (๐ โ ๐ท โฆ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)((๐ด ยท ๐)โ(๐ โf โ ๐ฅ))))))) |
72 | 1, 6, 5, 3, 7, 8 | psrmulcl 21372 |
. . . . 5
โข (๐ โ (๐ ร ๐) โ ๐ต) |
73 | 1, 10, 9, 6, 14, 4,
11, 72 | psrvsca 21375 |
. . . 4
โข (๐ โ (๐ด ยท (๐ ร ๐)) = ((๐ท ร {๐ด}) โf
(.rโ๐
)(๐ ร ๐))) |
74 | 54 | a1i 11 |
. . . . 5
โข (๐ โ ๐ท โ V) |
75 | | ovex 7391 |
. . . . . 6
โข (๐
ฮฃg
(๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) โ V |
76 | 75 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) โ V) |
77 | | fconstmpt 5695 |
. . . . . 6
โข (๐ท ร {๐ด}) = (๐ โ ๐ท โฆ ๐ด) |
78 | 77 | a1i 11 |
. . . . 5
โข (๐ โ (๐ท ร {๐ด}) = (๐ โ ๐ท โฆ ๐ด)) |
79 | 1, 6, 14, 5, 4, 7,
8 | psrmulfval 21369 |
. . . . 5
โข (๐ โ (๐ ร ๐) = (๐ โ ๐ท โฆ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))))) |
80 | 74, 15, 76, 78, 79 | offval2 7638 |
. . . 4
โข (๐ โ ((๐ท ร {๐ด}) โf
(.rโ๐
)(๐ ร ๐)) = (๐ โ ๐ท โฆ (๐ด(.rโ๐
)(๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))))) |
81 | 73, 80 | eqtrd 2773 |
. . 3
โข (๐ โ (๐ด ยท (๐ ร ๐)) = (๐ โ ๐ท โฆ (๐ด(.rโ๐
)(๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))))) |
82 | 69, 71, 81 | 3eqtr4d 2783 |
. 2
โข (๐ โ (๐ ร (๐ด ยท ๐)) = (๐ด ยท (๐ ร ๐))) |
83 | 12, 82 | jca 513 |
1
โข (๐ โ (((๐ด ยท ๐) ร ๐) = (๐ด ยท (๐ ร ๐)) โง (๐ ร (๐ด ยท ๐)) = (๐ด ยท (๐ ร ๐)))) |