Step | Hyp | Ref
| Expression |
1 | | mnringmulrcld.2 |
. . 3
โข ๐น = (๐
MndRing ๐) |
2 | | mnringmulrcld.3 |
. . 3
โข ๐ต = (Baseโ๐น) |
3 | | eqid 2732 |
. . 3
โข
(.rโ๐
) = (.rโ๐
) |
4 | | eqid 2732 |
. . 3
โข
(0gโ๐
) = (0gโ๐
) |
5 | | mnringmulrcld.1 |
. . 3
โข ๐ด = (Baseโ๐) |
6 | | eqid 2732 |
. . 3
โข
(+gโ๐) = (+gโ๐) |
7 | | mnringmulrcld.4 |
. . 3
โข ยท =
(.rโ๐น) |
8 | | mnringmulrcld.5 |
. . 3
โข (๐ โ ๐
โ Ring) |
9 | | mnringmulrcld.6 |
. . 3
โข (๐ โ ๐ โ ๐) |
10 | | mnringmulrcld.7 |
. . 3
โข (๐ โ ๐ โ ๐ต) |
11 | | mnringmulrcld.8 |
. . 3
โข (๐ โ ๐ โ ๐ต) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | mnringmulrvald 42976 |
. 2
โข (๐ โ (๐ ยท ๐) = (๐น ฮฃg (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))))) |
13 | | eqid 2732 |
. . 3
โข
(0gโ๐น) = (0gโ๐น) |
14 | 1, 8, 9 | mnringlmodd 42975 |
. . . 4
โข (๐ โ ๐น โ LMod) |
15 | | lmodcmn 20519 |
. . . 4
โข (๐น โ LMod โ ๐น โ CMnd) |
16 | 14, 15 | syl 17 |
. . 3
โข (๐ โ ๐น โ CMnd) |
17 | 5 | fvexi 6905 |
. . . . 5
โข ๐ด โ V |
18 | 17, 17 | xpex 7739 |
. . . 4
โข (๐ด ร ๐ด) โ V |
19 | 18 | a1i 11 |
. . 3
โข (๐ โ (๐ด ร ๐ด) โ V) |
20 | 8 | 3ad2ant1 1133 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ๐
โ Ring) |
21 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
โข
(Baseโ๐
) =
(Baseโ๐
) |
22 | 1, 2, 5, 21, 8, 9,
10 | mnringbasefd 42964 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐:๐ดโถ(Baseโ๐
)) |
23 | 22 | 3ad2ant1 1133 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ๐:๐ดโถ(Baseโ๐
)) |
24 | | simp2 1137 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ๐ โ ๐ด) |
25 | 23, 24 | ffvelcdmd 7087 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (๐โ๐) โ (Baseโ๐
)) |
26 | 1, 2, 5, 21, 8, 9,
11 | mnringbasefd 42964 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐:๐ดโถ(Baseโ๐
)) |
27 | 26 | 3ad2ant1 1133 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ๐:๐ดโถ(Baseโ๐
)) |
28 | | simp3 1138 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ๐ โ ๐ด) |
29 | 27, 28 | ffvelcdmd 7087 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (๐โ๐) โ (Baseโ๐
)) |
30 | 21, 3 | ringcl 20072 |
. . . . . . . . . . . . 13
โข ((๐
โ Ring โง (๐โ๐) โ (Baseโ๐
) โง (๐โ๐) โ (Baseโ๐
)) โ ((๐โ๐)(.rโ๐
)(๐โ๐)) โ (Baseโ๐
)) |
31 | 20, 25, 29, 30 | syl3anc 1371 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((๐โ๐)(.rโ๐
)(๐โ๐)) โ (Baseโ๐
)) |
32 | 21, 4 | ring0cl 20083 |
. . . . . . . . . . . . 13
โข (๐
โ Ring โ
(0gโ๐
)
โ (Baseโ๐
)) |
33 | 20, 32 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (0gโ๐
) โ (Baseโ๐
)) |
34 | 31, 33 | ifcld 4574 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)) โ (Baseโ๐
)) |
35 | 34 | adantr 481 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ โ ๐ด) โ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)) โ (Baseโ๐
)) |
36 | 35 | fmpttd 7114 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))):๐ดโถ(Baseโ๐
)) |
37 | 21 | fvexi 6905 |
. . . . . . . . . 10
โข
(Baseโ๐
)
โ V |
38 | 37, 17 | elmap 8864 |
. . . . . . . . 9
โข ((๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ ((Baseโ๐
) โm ๐ด) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))):๐ดโถ(Baseโ๐
)) |
39 | 36, 38 | sylibr 233 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ ((Baseโ๐
) โm ๐ด)) |
40 | 17 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ๐ด โ V) |
41 | | eqid 2732 |
. . . . . . . . 9
โข (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) = (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) |
42 | 40, 33, 41 | sniffsupp 9394 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) finSupp (0gโ๐
)) |
43 | 39, 42 | jca 512 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ ((Baseโ๐
) โm ๐ด) โง (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) finSupp (0gโ๐
))) |
44 | 9 | 3ad2ant1 1133 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ๐ โ ๐) |
45 | 1, 2, 5, 21, 4, 20, 44 | mnringelbased 42963 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ ๐ต โ ((๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ ((Baseโ๐
) โm ๐ด) โง (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) finSupp (0gโ๐
)))) |
46 | 43, 45 | mpbird 256 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ ๐ต) |
47 | 46 | 3expb 1120 |
. . . . 5
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด)) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ ๐ต) |
48 | 47 | ralrimivva 3200 |
. . . 4
โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ด (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ ๐ต) |
49 | | eqid 2732 |
. . . . 5
โข (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) = (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) |
50 | 49 | fmpo 8053 |
. . . 4
โข
(โ๐ โ
๐ด โ๐ โ ๐ด (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ ๐ต โ (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))):(๐ด ร ๐ด)โถ๐ต) |
51 | 48, 50 | sylib 217 |
. . 3
โข (๐ โ (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))):(๐ด ร ๐ด)โถ๐ต) |
52 | 17, 17 | mpoex 8065 |
. . . . 5
โข (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) โ V |
53 | 52 | a1i 11 |
. . . 4
โข (๐ โ (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) โ V) |
54 | 51 | ffnd 6718 |
. . . 4
โข (๐ โ (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) Fn (๐ด ร ๐ด)) |
55 | 13 | fvexi 6905 |
. . . . 5
โข
(0gโ๐น) โ V |
56 | 55 | a1i 11 |
. . . 4
โข (๐ โ (0gโ๐น) โ V) |
57 | 1, 2, 4, 8, 9, 10 | mnringbasefsuppd 42965 |
. . . . . 6
โข (๐ โ ๐ finSupp (0gโ๐
)) |
58 | 57 | fsuppimpd 9368 |
. . . . 5
โข (๐ โ (๐ supp (0gโ๐
)) โ Fin) |
59 | 1, 2, 4, 8, 9, 11 | mnringbasefsuppd 42965 |
. . . . . 6
โข (๐ โ ๐ finSupp (0gโ๐
)) |
60 | 59 | fsuppimpd 9368 |
. . . . 5
โข (๐ โ (๐ supp (0gโ๐
)) โ Fin) |
61 | | xpfi 9316 |
. . . . 5
โข (((๐ supp (0gโ๐
)) โ Fin โง (๐ supp (0gโ๐
)) โ Fin) โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โ Fin) |
62 | 58, 60, 61 | syl2anc 584 |
. . . 4
โข (๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โ Fin) |
63 | | elxpi 5698 |
. . . . . . 7
โข (๐ โ (๐ด ร ๐ด) โ โ๐โ๐(๐ = โจ๐, ๐โฉ โง (๐ โ ๐ด โง ๐ โ ๐ด))) |
64 | | simpl 483 |
. . . . . . . 8
โข ((๐ = โจ๐, ๐โฉ โง (๐ โ ๐ด โง ๐ โ ๐ด)) โ ๐ = โจ๐, ๐โฉ) |
65 | 64 | 2eximi 1838 |
. . . . . . 7
โข
(โ๐โ๐(๐ = โจ๐, ๐โฉ โง (๐ โ ๐ด โง ๐ โ ๐ด)) โ โ๐โ๐ ๐ = โจ๐, ๐โฉ) |
66 | 63, 65 | syl 17 |
. . . . . 6
โข (๐ โ (๐ด ร ๐ด) โ โ๐โ๐ ๐ = โจ๐, ๐โฉ) |
67 | 66 | adantl 482 |
. . . . 5
โข ((๐ โง ๐ โ (๐ด ร ๐ด)) โ โ๐โ๐ ๐ = โจ๐, ๐โฉ) |
68 | | nfv 1917 |
. . . . . 6
โข
โฒ๐(๐ โง ๐ โ (๐ด ร ๐ด)) |
69 | | nfv 1917 |
. . . . . . 7
โข
โฒ๐ ๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) |
70 | | nfmpo1 7488 |
. . . . . . . . 9
โข
โฒ๐(๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) |
71 | | nfcv 2903 |
. . . . . . . . 9
โข
โฒ๐๐ |
72 | 70, 71 | nffv 6901 |
. . . . . . . 8
โข
โฒ๐((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) |
73 | | nfcv 2903 |
. . . . . . . 8
โข
โฒ๐(0gโ๐น) |
74 | 72, 73 | nfeq 2916 |
. . . . . . 7
โข
โฒ๐((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น) |
75 | 69, 74 | nfor 1907 |
. . . . . 6
โข
โฒ๐(๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โจ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น)) |
76 | | nfv 1917 |
. . . . . . 7
โข
โฒ๐(๐ โง ๐ โ (๐ด ร ๐ด)) |
77 | | nfv 1917 |
. . . . . . . 8
โข
โฒ๐ ๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) |
78 | | nfmpo2 7489 |
. . . . . . . . . 10
โข
โฒ๐(๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) |
79 | | nfcv 2903 |
. . . . . . . . . 10
โข
โฒ๐๐ |
80 | 78, 79 | nffv 6901 |
. . . . . . . . 9
โข
โฒ๐((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) |
81 | | nfcv 2903 |
. . . . . . . . 9
โข
โฒ๐(0gโ๐น) |
82 | 80, 81 | nfeq 2916 |
. . . . . . . 8
โข
โฒ๐((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น) |
83 | 77, 82 | nfor 1907 |
. . . . . . 7
โข
โฒ๐(๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โจ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น)) |
84 | | simp3 1138 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (๐ด ร ๐ด) โง ๐ = โจ๐, ๐โฉ) โ ๐ = โจ๐, ๐โฉ) |
85 | | simp2 1137 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (๐ด ร ๐ด) โง ๐ = โจ๐, ๐โฉ) โ ๐ โ (๐ด ร ๐ด)) |
86 | 84, 85 | eqeltrrd 2834 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐ด ร ๐ด) โง ๐ = โจ๐, ๐โฉ) โ โจ๐, ๐โฉ โ (๐ด ร ๐ด)) |
87 | | opelxp 5712 |
. . . . . . . . . 10
โข
(โจ๐, ๐โฉ โ (๐ด ร ๐ด) โ (๐ โ ๐ด โง ๐ โ ๐ด)) |
88 | 86, 87 | sylib 217 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (๐ด ร ๐ด) โง ๐ = โจ๐, ๐โฉ) โ (๐ โ ๐ด โง ๐ โ ๐ด)) |
89 | | ianor 980 |
. . . . . . . . . . . . . . . 16
โข (ยฌ
(๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
))) โ (ยฌ ๐ โ (๐ supp (0gโ๐
)) โจ ยฌ ๐ โ (๐ supp (0gโ๐
)))) |
90 | 22 | ffnd 6718 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ Fn ๐ด) |
91 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ด โ V) |
92 | 4 | fvexi 6905 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(0gโ๐
) โ V |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (0gโ๐
) โ V) |
94 | | elsuppfn 8155 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ Fn ๐ด โง ๐ด โ V โง (0gโ๐
) โ V) โ (๐ โ (๐ supp (0gโ๐
)) โ (๐ โ ๐ด โง (๐โ๐) โ (0gโ๐
)))) |
95 | 90, 91, 93, 94 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ โ (๐ supp (0gโ๐
)) โ (๐ โ ๐ด โง (๐โ๐) โ (0gโ๐
)))) |
96 | 95 | biimprd 247 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((๐ โ ๐ด โง (๐โ๐) โ (0gโ๐
)) โ ๐ โ (๐ supp (0gโ๐
)))) |
97 | 96 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((๐ โ ๐ด โง (๐โ๐) โ (0gโ๐
)) โ ๐ โ (๐ supp (0gโ๐
)))) |
98 | 24, 97 | mpand 693 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((๐โ๐) โ (0gโ๐
) โ ๐ โ (๐ supp (0gโ๐
)))) |
99 | 98 | necon1bd 2958 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (ยฌ ๐ โ (๐ supp (0gโ๐
)) โ (๐โ๐) = (0gโ๐
))) |
100 | 26 | ffnd 6718 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ Fn ๐ด) |
101 | | elsuppfn 8155 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ Fn ๐ด โง ๐ด โ V โง (0gโ๐
) โ V) โ (๐ โ (๐ supp (0gโ๐
)) โ (๐ โ ๐ด โง (๐โ๐) โ (0gโ๐
)))) |
102 | 100, 91, 93, 101 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ โ (๐ supp (0gโ๐
)) โ (๐ โ ๐ด โง (๐โ๐) โ (0gโ๐
)))) |
103 | 102 | biimprd 247 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((๐ โ ๐ด โง (๐โ๐) โ (0gโ๐
)) โ ๐ โ (๐ supp (0gโ๐
)))) |
104 | 103 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((๐ โ ๐ด โง (๐โ๐) โ (0gโ๐
)) โ ๐ โ (๐ supp (0gโ๐
)))) |
105 | 28, 104 | mpand 693 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((๐โ๐) โ (0gโ๐
) โ ๐ โ (๐ supp (0gโ๐
)))) |
106 | 105 | necon1bd 2958 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (ยฌ ๐ โ (๐ supp (0gโ๐
)) โ (๐โ๐) = (0gโ๐
))) |
107 | 99, 106 | orim12d 963 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((ยฌ ๐ โ (๐ supp (0gโ๐
)) โจ ยฌ ๐ โ (๐ supp (0gโ๐
))) โ ((๐โ๐) = (0gโ๐
) โจ (๐โ๐) = (0gโ๐
)))) |
108 | 107 | imp 407 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง (ยฌ ๐ โ (๐ supp (0gโ๐
)) โจ ยฌ ๐ โ (๐ supp (0gโ๐
)))) โ ((๐โ๐) = (0gโ๐
) โจ (๐โ๐) = (0gโ๐
))) |
109 | 89, 108 | sylan2b 594 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง ยฌ (๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
)))) โ ((๐โ๐) = (0gโ๐
) โจ (๐โ๐) = (0gโ๐
))) |
110 | | oveq1 7415 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐โ๐) = (0gโ๐
) โ ((๐โ๐)(.rโ๐
)(๐โ๐)) = ((0gโ๐
)(.rโ๐
)(๐โ๐))) |
111 | 21, 3, 4 | ringlz 20106 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐
โ Ring โง (๐โ๐) โ (Baseโ๐
)) โ ((0gโ๐
)(.rโ๐
)(๐โ๐)) = (0gโ๐
)) |
112 | 20, 29, 111 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((0gโ๐
)(.rโ๐
)(๐โ๐)) = (0gโ๐
)) |
113 | 110, 112 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง (๐โ๐) = (0gโ๐
)) โ ((๐โ๐)(.rโ๐
)(๐โ๐)) = (0gโ๐
)) |
114 | | oveq2 7416 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐โ๐) = (0gโ๐
) โ ((๐โ๐)(.rโ๐
)(๐โ๐)) = ((๐โ๐)(.rโ๐
)(0gโ๐
))) |
115 | 21, 3, 4 | ringrz 20107 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐
โ Ring โง (๐โ๐) โ (Baseโ๐
)) โ ((๐โ๐)(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
116 | 20, 25, 115 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((๐โ๐)(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
117 | 114, 116 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง (๐โ๐) = (0gโ๐
)) โ ((๐โ๐)(.rโ๐
)(๐โ๐)) = (0gโ๐
)) |
118 | 113, 117 | jaodan 956 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง ((๐โ๐) = (0gโ๐
) โจ (๐โ๐) = (0gโ๐
))) โ ((๐โ๐)(.rโ๐
)(๐โ๐)) = (0gโ๐
)) |
119 | 118 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง ((๐โ๐) = (0gโ๐
) โจ (๐โ๐) = (0gโ๐
))) โง ๐ = (๐(+gโ๐)๐)) โ ((๐โ๐)(.rโ๐
)(๐โ๐)) = (0gโ๐
)) |
120 | | eqidd 2733 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง ((๐โ๐) = (0gโ๐
) โจ (๐โ๐) = (0gโ๐
))) โง ยฌ ๐ = (๐(+gโ๐)๐)) โ (0gโ๐
) = (0gโ๐
)) |
121 | 119, 120 | ifeqda 4564 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง ((๐โ๐) = (0gโ๐
) โจ (๐โ๐) = (0gโ๐
))) โ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)) = (0gโ๐
)) |
122 | 121 | mpteq2dv 5250 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง ((๐โ๐) = (0gโ๐
) โจ (๐โ๐) = (0gโ๐
))) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) = (๐ โ ๐ด โฆ (0gโ๐
))) |
123 | | fconstmpt 5738 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด ร
{(0gโ๐
)})
= (๐ โ ๐ด โฆ
(0gโ๐
)) |
124 | 1, 4, 5, 8, 9 | mnring0g2d 42969 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ด ร {(0gโ๐
)}) = (0gโ๐น)) |
125 | 123, 124 | eqtr3id 2786 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ โ ๐ด โฆ (0gโ๐
)) = (0gโ๐น)) |
126 | 125 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (๐ โ ๐ด โฆ (0gโ๐
)) = (0gโ๐น)) |
127 | 126 | adantr 481 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง ((๐โ๐) = (0gโ๐
) โจ (๐โ๐) = (0gโ๐
))) โ (๐ โ ๐ด โฆ (0gโ๐
)) = (0gโ๐น)) |
128 | 122, 127 | eqtrd 2772 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง ((๐โ๐) = (0gโ๐
) โจ (๐โ๐) = (0gโ๐
))) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) = (0gโ๐น)) |
129 | 109, 128 | syldan 591 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โง ยฌ (๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
)))) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) = (0gโ๐น)) |
130 | 129 | ex 413 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (ยฌ (๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
))) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) = (0gโ๐น))) |
131 | 130 | orrd 861 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
))) โจ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) = (0gโ๐น))) |
132 | 131 | 3expb 1120 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด)) โ ((๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
))) โจ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) = (0gโ๐น))) |
133 | 132 | 3adant3 1132 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โ ((๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
))) โจ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) = (0gโ๐น))) |
134 | | eleq1 2821 |
. . . . . . . . . . . . 13
โข (๐ = โจ๐, ๐โฉ โ (๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โ โจ๐, ๐โฉ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))))) |
135 | | opelxp 5712 |
. . . . . . . . . . . . 13
โข
(โจ๐, ๐โฉ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โ (๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
)))) |
136 | 134, 135 | bitrdi 286 |
. . . . . . . . . . . 12
โข (๐ = โจ๐, ๐โฉ โ (๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โ (๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
))))) |
137 | 136 | 3ad2ant3 1135 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โ (๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โ (๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
))))) |
138 | | simp2l 1199 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โ ๐ โ ๐ด) |
139 | | simp2r 1200 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โ ๐ โ ๐ด) |
140 | | eqidd 2733 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โ (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) = (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))) |
141 | | simp3 1138 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โ ๐ = โจ๐, ๐โฉ) |
142 | 17 | mptex 7224 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ V |
143 | 142 | a1i 11 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โง ๐ โ ๐ด โง ๐ โ ๐ด) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) โ V) |
144 | 140, 141,
143 | fvmpopr2d 7568 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โง ๐ โ ๐ด โง ๐ โ ๐ด) โ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) |
145 | 138, 139,
144 | mpd3an23 1463 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) |
146 | 145 | eqeq1d 2734 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โ (((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น) โ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) = (0gโ๐น))) |
147 | 137, 146 | orbi12d 917 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โ ((๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โจ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น)) โ ((๐ โ (๐ supp (0gโ๐
)) โง ๐ โ (๐ supp (0gโ๐
))) โจ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))) = (0gโ๐น)))) |
148 | 133, 147 | mpbird 256 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ด) โง ๐ = โจ๐, ๐โฉ) โ (๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โจ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น))) |
149 | 88, 148 | syld3an2 1411 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐ด ร ๐ด) โง ๐ = โจ๐, ๐โฉ) โ (๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โจ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น))) |
150 | 149 | 3expia 1121 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐ด ร ๐ด)) โ (๐ = โจ๐, ๐โฉ โ (๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โจ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น)))) |
151 | 76, 83, 150 | exlimd 2211 |
. . . . . 6
โข ((๐ โง ๐ โ (๐ด ร ๐ด)) โ (โ๐ ๐ = โจ๐, ๐โฉ โ (๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โจ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น)))) |
152 | 68, 75, 151 | exlimd 2211 |
. . . . 5
โข ((๐ โง ๐ โ (๐ด ร ๐ด)) โ (โ๐โ๐ ๐ = โจ๐, ๐โฉ โ (๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โจ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น)))) |
153 | 67, 152 | mpd 15 |
. . . 4
โข ((๐ โง ๐ โ (๐ด ร ๐ด)) โ (๐ โ ((๐ supp (0gโ๐
)) ร (๐ supp (0gโ๐
))) โจ ((๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))โ๐) = (0gโ๐น))) |
154 | 53, 54, 56, 62, 153 | finnzfsuppd 42951 |
. . 3
โข (๐ โ (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
)))) finSupp (0gโ๐น)) |
155 | 2, 13, 16, 19, 51, 154 | gsumcl 19782 |
. 2
โข (๐ โ (๐น ฮฃg (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐(+gโ๐)๐), ((๐โ๐)(.rโ๐
)(๐โ๐)), (0gโ๐
))))) โ ๐ต) |
156 | 12, 155 | eqeltrd 2833 |
1
โข (๐ โ (๐ ยท ๐) โ ๐ต) |