Step | Hyp | Ref
| Expression |
1 | | imasring.u |
. . . 4
โข (๐ โ ๐ = (๐น โs ๐
)) |
2 | | imasring.v |
. . . 4
โข (๐ โ ๐ = (Baseโ๐
)) |
3 | | imasring.f |
. . . 4
โข (๐ โ ๐น:๐โontoโ๐ต) |
4 | | imasring.r |
. . . 4
โข (๐ โ ๐
โ Ring) |
5 | 1, 2, 3, 4 | imasbas 17457 |
. . 3
โข (๐ โ ๐ต = (Baseโ๐)) |
6 | | eqidd 2733 |
. . 3
โข (๐ โ (+gโ๐) = (+gโ๐)) |
7 | | eqidd 2733 |
. . 3
โข (๐ โ (.rโ๐) = (.rโ๐)) |
8 | | imasring.p |
. . . . . 6
โข + =
(+gโ๐
) |
9 | 8 | a1i 11 |
. . . . 5
โข (๐ โ + =
(+gโ๐
)) |
10 | | imasring.e1 |
. . . . 5
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (((๐นโ๐) = (๐นโ๐) โง (๐นโ๐) = (๐นโ๐)) โ (๐นโ(๐ + ๐)) = (๐นโ(๐ + ๐)))) |
11 | | ringgrp 20060 |
. . . . . 6
โข (๐
โ Ring โ ๐
โ Grp) |
12 | 4, 11 | syl 17 |
. . . . 5
โข (๐ โ ๐
โ Grp) |
13 | | eqid 2732 |
. . . . 5
โข
(0gโ๐
) = (0gโ๐
) |
14 | 1, 2, 9, 3, 10, 12, 13 | imasgrp 18938 |
. . . 4
โข (๐ โ (๐ โ Grp โง (๐นโ(0gโ๐
)) = (0gโ๐))) |
15 | 14 | simpld 495 |
. . 3
โข (๐ โ ๐ โ Grp) |
16 | | imasring.e2 |
. . . . 5
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (((๐นโ๐) = (๐นโ๐) โง (๐นโ๐) = (๐นโ๐)) โ (๐นโ(๐ ยท ๐)) = (๐นโ(๐ ยท ๐)))) |
17 | | imasring.t |
. . . . 5
โข ยท =
(.rโ๐
) |
18 | | eqid 2732 |
. . . . 5
โข
(.rโ๐) = (.rโ๐) |
19 | 4 | adantr 481 |
. . . . . . . 8
โข ((๐ โง (๐ข โ ๐ โง ๐ฃ โ ๐)) โ ๐
โ Ring) |
20 | | simprl 769 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ ๐ โง ๐ฃ โ ๐)) โ ๐ข โ ๐) |
21 | 2 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ ๐ โง ๐ฃ โ ๐)) โ ๐ = (Baseโ๐
)) |
22 | 20, 21 | eleqtrd 2835 |
. . . . . . . 8
โข ((๐ โง (๐ข โ ๐ โง ๐ฃ โ ๐)) โ ๐ข โ (Baseโ๐
)) |
23 | | simprr 771 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ ๐ โง ๐ฃ โ ๐)) โ ๐ฃ โ ๐) |
24 | 23, 21 | eleqtrd 2835 |
. . . . . . . 8
โข ((๐ โง (๐ข โ ๐ โง ๐ฃ โ ๐)) โ ๐ฃ โ (Baseโ๐
)) |
25 | | eqid 2732 |
. . . . . . . . 9
โข
(Baseโ๐
) =
(Baseโ๐
) |
26 | 25, 17 | ringcl 20072 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ข โ (Baseโ๐
) โง ๐ฃ โ (Baseโ๐
)) โ (๐ข ยท ๐ฃ) โ (Baseโ๐
)) |
27 | 19, 22, 24, 26 | syl3anc 1371 |
. . . . . . 7
โข ((๐ โง (๐ข โ ๐ โง ๐ฃ โ ๐)) โ (๐ข ยท ๐ฃ) โ (Baseโ๐
)) |
28 | 27, 21 | eleqtrrd 2836 |
. . . . . 6
โข ((๐ โง (๐ข โ ๐ โง ๐ฃ โ ๐)) โ (๐ข ยท ๐ฃ) โ ๐) |
29 | 28 | caovclg 7598 |
. . . . 5
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ ยท ๐) โ ๐) |
30 | 3, 16, 1, 2, 4, 17,
18, 29 | imasmulf 17481 |
. . . 4
โข (๐ โ (.rโ๐):(๐ต ร ๐ต)โถ๐ต) |
31 | | fovcdm 7576 |
. . . 4
โข
(((.rโ๐):(๐ต ร ๐ต)โถ๐ต โง ๐ข โ ๐ต โง ๐ฃ โ ๐ต) โ (๐ข(.rโ๐)๐ฃ) โ ๐ต) |
32 | 30, 31 | syl3an1 1163 |
. . 3
โข ((๐ โง ๐ข โ ๐ต โง ๐ฃ โ ๐ต) โ (๐ข(.rโ๐)๐ฃ) โ ๐ต) |
33 | | forn 6808 |
. . . . . . . . . 10
โข (๐น:๐โontoโ๐ต โ ran ๐น = ๐ต) |
34 | 3, 33 | syl 17 |
. . . . . . . . 9
โข (๐ โ ran ๐น = ๐ต) |
35 | 34 | eleq2d 2819 |
. . . . . . . 8
โข (๐ โ (๐ข โ ran ๐น โ ๐ข โ ๐ต)) |
36 | 34 | eleq2d 2819 |
. . . . . . . 8
โข (๐ โ (๐ฃ โ ran ๐น โ ๐ฃ โ ๐ต)) |
37 | 34 | eleq2d 2819 |
. . . . . . . 8
โข (๐ โ (๐ค โ ran ๐น โ ๐ค โ ๐ต)) |
38 | 35, 36, 37 | 3anbi123d 1436 |
. . . . . . 7
โข (๐ โ ((๐ข โ ran ๐น โง ๐ฃ โ ran ๐น โง ๐ค โ ran ๐น) โ (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต))) |
39 | | fofn 6807 |
. . . . . . . . 9
โข (๐น:๐โontoโ๐ต โ ๐น Fn ๐) |
40 | 3, 39 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐น Fn ๐) |
41 | | fvelrnb 6952 |
. . . . . . . . 9
โข (๐น Fn ๐ โ (๐ข โ ran ๐น โ โ๐ฅ โ ๐ (๐นโ๐ฅ) = ๐ข)) |
42 | | fvelrnb 6952 |
. . . . . . . . 9
โข (๐น Fn ๐ โ (๐ฃ โ ran ๐น โ โ๐ฆ โ ๐ (๐นโ๐ฆ) = ๐ฃ)) |
43 | | fvelrnb 6952 |
. . . . . . . . 9
โข (๐น Fn ๐ โ (๐ค โ ran ๐น โ โ๐ง โ ๐ (๐นโ๐ง) = ๐ค)) |
44 | 41, 42, 43 | 3anbi123d 1436 |
. . . . . . . 8
โข (๐น Fn ๐ โ ((๐ข โ ran ๐น โง ๐ฃ โ ran ๐น โง ๐ค โ ran ๐น) โ (โ๐ฅ โ ๐ (๐นโ๐ฅ) = ๐ข โง โ๐ฆ โ ๐ (๐นโ๐ฆ) = ๐ฃ โง โ๐ง โ ๐ (๐นโ๐ง) = ๐ค))) |
45 | 40, 44 | syl 17 |
. . . . . . 7
โข (๐ โ ((๐ข โ ran ๐น โง ๐ฃ โ ran ๐น โง ๐ค โ ran ๐น) โ (โ๐ฅ โ ๐ (๐นโ๐ฅ) = ๐ข โง โ๐ฆ โ ๐ (๐นโ๐ฆ) = ๐ฃ โง โ๐ง โ ๐ (๐นโ๐ง) = ๐ค))) |
46 | 38, 45 | bitr3d 280 |
. . . . . 6
โข (๐ โ ((๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต) โ (โ๐ฅ โ ๐ (๐นโ๐ฅ) = ๐ข โง โ๐ฆ โ ๐ (๐นโ๐ฆ) = ๐ฃ โง โ๐ง โ ๐ (๐นโ๐ง) = ๐ค))) |
47 | | 3reeanv 3227 |
. . . . . 6
โข
(โ๐ฅ โ
๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (โ๐ฅ โ ๐ (๐นโ๐ฅ) = ๐ข โง โ๐ฆ โ ๐ (๐นโ๐ฆ) = ๐ฃ โง โ๐ง โ ๐ (๐นโ๐ง) = ๐ค)) |
48 | 46, 47 | bitr4di 288 |
. . . . 5
โข (๐ โ ((๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค))) |
49 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐
โ Ring) |
50 | | simp2 1137 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ๐ฅ โ ๐) |
51 | 2 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ๐ = (Baseโ๐
)) |
52 | 50, 51 | eleqtrd 2835 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ๐ฅ โ (Baseโ๐
)) |
53 | 52 | 3adant3r3 1184 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฅ โ (Baseโ๐
)) |
54 | | simp3 1138 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ๐ฆ โ ๐) |
55 | 54, 51 | eleqtrd 2835 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ๐ฆ โ (Baseโ๐
)) |
56 | 55 | 3adant3r3 1184 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ โ (Baseโ๐
)) |
57 | | simpr3 1196 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ ๐) |
58 | 2 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ = (Baseโ๐
)) |
59 | 57, 58 | eleqtrd 2835 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ (Baseโ๐
)) |
60 | 25, 17 | ringass 20075 |
. . . . . . . . . . . . . 14
โข ((๐
โ Ring โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
) โง ๐ง โ (Baseโ๐
))) โ ((๐ฅ ยท ๐ฆ) ยท ๐ง) = (๐ฅ ยท (๐ฆ ยท ๐ง))) |
61 | 49, 53, 56, 59, 60 | syl13anc 1372 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ฅ ยท ๐ฆ) ยท ๐ง) = (๐ฅ ยท (๐ฆ ยท ๐ง))) |
62 | 61 | fveq2d 6895 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ((๐ฅ ยท ๐ฆ) ยท ๐ง)) = (๐นโ(๐ฅ ยท (๐ฆ ยท ๐ง)))) |
63 | | simpl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐) |
64 | 28 | caovclg 7598 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ ยท ๐ฆ) โ ๐) |
65 | 64 | 3adantr3 1171 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฅ ยท ๐ฆ) โ ๐) |
66 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 17480 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ ยท ๐ฆ) โ ๐ โง ๐ง โ ๐) โ ((๐นโ(๐ฅ ยท ๐ฆ))(.rโ๐)(๐นโ๐ง)) = (๐นโ((๐ฅ ยท ๐ฆ) ยท ๐ง))) |
67 | 63, 65, 57, 66 | syl3anc 1371 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ(๐ฅ ยท ๐ฆ))(.rโ๐)(๐นโ๐ง)) = (๐นโ((๐ฅ ยท ๐ฆ) ยท ๐ง))) |
68 | | simpr1 1194 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฅ โ ๐) |
69 | 28 | caovclg 7598 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ ยท ๐ง) โ ๐) |
70 | 69 | 3adantr1 1169 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ ยท ๐ง) โ ๐) |
71 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 17480 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ โง (๐ฆ ยท ๐ง) โ ๐) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ(๐ฆ ยท ๐ง))) = (๐นโ(๐ฅ ยท (๐ฆ ยท ๐ง)))) |
72 | 63, 68, 70, 71 | syl3anc 1371 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ(๐ฆ ยท ๐ง))) = (๐นโ(๐ฅ ยท (๐ฆ ยท ๐ง)))) |
73 | 62, 67, 72 | 3eqtr4d 2782 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ(๐ฅ ยท ๐ฆ))(.rโ๐)(๐นโ๐ง)) = ((๐นโ๐ฅ)(.rโ๐)(๐นโ(๐ฆ ยท ๐ง)))) |
74 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 17480 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ)) = (๐นโ(๐ฅ ยท ๐ฆ))) |
75 | 74 | 3adant3r3 1184 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ)) = (๐นโ(๐ฅ ยท ๐ฆ))) |
76 | 75 | oveq1d 7423 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ))(.rโ๐)(๐นโ๐ง)) = ((๐นโ(๐ฅ ยท ๐ฆ))(.rโ๐)(๐นโ๐ง))) |
77 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 17480 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐) โ ((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง)) = (๐นโ(๐ฆ ยท ๐ง))) |
78 | 77 | 3adant3r1 1182 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง)) = (๐นโ(๐ฆ ยท ๐ง))) |
79 | 78 | oveq2d 7424 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฅ)(.rโ๐)((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง))) = ((๐นโ๐ฅ)(.rโ๐)(๐นโ(๐ฆ ยท ๐ง)))) |
80 | 73, 76, 79 | 3eqtr4d 2782 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ))(.rโ๐)(๐นโ๐ง)) = ((๐นโ๐ฅ)(.rโ๐)((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง)))) |
81 | | simp1 1136 |
. . . . . . . . . . . . 13
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (๐นโ๐ฅ) = ๐ข) |
82 | | simp2 1137 |
. . . . . . . . . . . . 13
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (๐นโ๐ฆ) = ๐ฃ) |
83 | 81, 82 | oveq12d 7426 |
. . . . . . . . . . . 12
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ)) = (๐ข(.rโ๐)๐ฃ)) |
84 | | simp3 1138 |
. . . . . . . . . . . 12
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (๐นโ๐ง) = ๐ค) |
85 | 83, 84 | oveq12d 7426 |
. . . . . . . . . . 11
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ))(.rโ๐)(๐นโ๐ง)) = ((๐ข(.rโ๐)๐ฃ)(.rโ๐)๐ค)) |
86 | 82, 84 | oveq12d 7426 |
. . . . . . . . . . . 12
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง)) = (๐ฃ(.rโ๐)๐ค)) |
87 | 81, 86 | oveq12d 7426 |
. . . . . . . . . . 11
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐นโ๐ฅ)(.rโ๐)((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง))) = (๐ข(.rโ๐)(๐ฃ(.rโ๐)๐ค))) |
88 | 85, 87 | eqeq12d 2748 |
. . . . . . . . . 10
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ))(.rโ๐)(๐นโ๐ง)) = ((๐นโ๐ฅ)(.rโ๐)((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง))) โ ((๐ข(.rโ๐)๐ฃ)(.rโ๐)๐ค) = (๐ข(.rโ๐)(๐ฃ(.rโ๐)๐ค)))) |
89 | 80, 88 | syl5ibcom 244 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐ข(.rโ๐)๐ฃ)(.rโ๐)๐ค) = (๐ข(.rโ๐)(๐ฃ(.rโ๐)๐ค)))) |
90 | 89 | 3exp2 1354 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ โ (๐ฆ โ ๐ โ (๐ง โ ๐ โ (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐ข(.rโ๐)๐ฃ)(.rโ๐)๐ค) = (๐ข(.rโ๐)(๐ฃ(.rโ๐)๐ค))))))) |
91 | 90 | imp32 419 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ง โ ๐ โ (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐ข(.rโ๐)๐ฃ)(.rโ๐)๐ค) = (๐ข(.rโ๐)(๐ฃ(.rโ๐)๐ค))))) |
92 | 91 | rexlimdv 3153 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (โ๐ง โ ๐ ((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐ข(.rโ๐)๐ฃ)(.rโ๐)๐ค) = (๐ข(.rโ๐)(๐ฃ(.rโ๐)๐ค)))) |
93 | 92 | rexlimdvva 3211 |
. . . . 5
โข (๐ โ (โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐ข(.rโ๐)๐ฃ)(.rโ๐)๐ค) = (๐ข(.rโ๐)(๐ฃ(.rโ๐)๐ค)))) |
94 | 48, 93 | sylbid 239 |
. . . 4
โข (๐ โ ((๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต) โ ((๐ข(.rโ๐)๐ฃ)(.rโ๐)๐ค) = (๐ข(.rโ๐)(๐ฃ(.rโ๐)๐ค)))) |
95 | 94 | imp 407 |
. . 3
โข ((๐ โง (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต)) โ ((๐ข(.rโ๐)๐ฃ)(.rโ๐)๐ค) = (๐ข(.rโ๐)(๐ฃ(.rโ๐)๐ค))) |
96 | 25, 8, 17 | ringdi 20080 |
. . . . . . . . . . . . . 14
โข ((๐
โ Ring โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
) โง ๐ง โ (Baseโ๐
))) โ (๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง))) |
97 | 49, 53, 56, 59, 96 | syl13anc 1372 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง))) |
98 | 97 | fveq2d 6895 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ(๐ฅ ยท (๐ฆ + ๐ง))) = (๐นโ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)))) |
99 | 25, 8 | ringacl 20094 |
. . . . . . . . . . . . . . . . 17
โข ((๐
โ Ring โง ๐ข โ (Baseโ๐
) โง ๐ฃ โ (Baseโ๐
)) โ (๐ข + ๐ฃ) โ (Baseโ๐
)) |
100 | 19, 22, 24, 99 | syl3anc 1371 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ข โ ๐ โง ๐ฃ โ ๐)) โ (๐ข + ๐ฃ) โ (Baseโ๐
)) |
101 | 100, 21 | eleqtrrd 2836 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ข โ ๐ โง ๐ฃ โ ๐)) โ (๐ข + ๐ฃ) โ ๐) |
102 | 101 | caovclg 7598 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ + ๐ง) โ ๐) |
103 | 102 | 3adantr1 1169 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ + ๐ง) โ ๐) |
104 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 17480 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ โง (๐ฆ + ๐ง) โ ๐) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ(๐ฆ + ๐ง))) = (๐นโ(๐ฅ ยท (๐ฆ + ๐ง)))) |
105 | 63, 68, 103, 104 | syl3anc 1371 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ(๐ฆ + ๐ง))) = (๐นโ(๐ฅ ยท (๐ฆ + ๐ง)))) |
106 | 28 | caovclg 7598 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ ๐ โง ๐ง โ ๐)) โ (๐ฅ ยท ๐ง) โ ๐) |
107 | 106 | 3adantr2 1170 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฅ ยท ๐ง) โ ๐) |
108 | | eqid 2732 |
. . . . . . . . . . . . . 14
โข
(+gโ๐) = (+gโ๐) |
109 | 3, 10, 1, 2, 4, 8, 108 | imasaddval 17477 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ ยท ๐ฆ) โ ๐ โง (๐ฅ ยท ๐ง) โ ๐) โ ((๐นโ(๐ฅ ยท ๐ฆ))(+gโ๐)(๐นโ(๐ฅ ยท ๐ง))) = (๐นโ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)))) |
110 | 63, 65, 107, 109 | syl3anc 1371 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ(๐ฅ ยท ๐ฆ))(+gโ๐)(๐นโ(๐ฅ ยท ๐ง))) = (๐นโ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)))) |
111 | 98, 105, 110 | 3eqtr4d 2782 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ(๐ฆ + ๐ง))) = ((๐นโ(๐ฅ ยท ๐ฆ))(+gโ๐)(๐นโ(๐ฅ ยท ๐ง)))) |
112 | 3, 10, 1, 2, 4, 8, 108 | imasaddval 17477 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐) โ ((๐นโ๐ฆ)(+gโ๐)(๐นโ๐ง)) = (๐นโ(๐ฆ + ๐ง))) |
113 | 112 | 3adant3r1 1182 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ)(+gโ๐)(๐นโ๐ง)) = (๐นโ(๐ฆ + ๐ง))) |
114 | 113 | oveq2d 7424 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฅ)(.rโ๐)((๐นโ๐ฆ)(+gโ๐)(๐นโ๐ง))) = ((๐นโ๐ฅ)(.rโ๐)(๐นโ(๐ฆ + ๐ง)))) |
115 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 17480 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ โง ๐ง โ ๐) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง)) = (๐นโ(๐ฅ ยท ๐ง))) |
116 | 115 | 3adant3r2 1183 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง)) = (๐นโ(๐ฅ ยท ๐ง))) |
117 | 75, 116 | oveq12d 7426 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ))(+gโ๐)((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง))) = ((๐นโ(๐ฅ ยท ๐ฆ))(+gโ๐)(๐นโ(๐ฅ ยท ๐ง)))) |
118 | 111, 114,
117 | 3eqtr4d 2782 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฅ)(.rโ๐)((๐นโ๐ฆ)(+gโ๐)(๐นโ๐ง))) = (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ))(+gโ๐)((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง)))) |
119 | 82, 84 | oveq12d 7426 |
. . . . . . . . . . . 12
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐นโ๐ฆ)(+gโ๐)(๐นโ๐ง)) = (๐ฃ(+gโ๐)๐ค)) |
120 | 81, 119 | oveq12d 7426 |
. . . . . . . . . . 11
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐นโ๐ฅ)(.rโ๐)((๐นโ๐ฆ)(+gโ๐)(๐นโ๐ง))) = (๐ข(.rโ๐)(๐ฃ(+gโ๐)๐ค))) |
121 | 81, 84 | oveq12d 7426 |
. . . . . . . . . . . 12
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง)) = (๐ข(.rโ๐)๐ค)) |
122 | 83, 121 | oveq12d 7426 |
. . . . . . . . . . 11
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ))(+gโ๐)((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง))) = ((๐ข(.rโ๐)๐ฃ)(+gโ๐)(๐ข(.rโ๐)๐ค))) |
123 | 120, 122 | eqeq12d 2748 |
. . . . . . . . . 10
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (((๐นโ๐ฅ)(.rโ๐)((๐นโ๐ฆ)(+gโ๐)(๐นโ๐ง))) = (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ฆ))(+gโ๐)((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง))) โ (๐ข(.rโ๐)(๐ฃ(+gโ๐)๐ค)) = ((๐ข(.rโ๐)๐ฃ)(+gโ๐)(๐ข(.rโ๐)๐ค)))) |
124 | 118, 123 | syl5ibcom 244 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (๐ข(.rโ๐)(๐ฃ(+gโ๐)๐ค)) = ((๐ข(.rโ๐)๐ฃ)(+gโ๐)(๐ข(.rโ๐)๐ค)))) |
125 | 124 | 3exp2 1354 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ โ (๐ฆ โ ๐ โ (๐ง โ ๐ โ (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (๐ข(.rโ๐)(๐ฃ(+gโ๐)๐ค)) = ((๐ข(.rโ๐)๐ฃ)(+gโ๐)(๐ข(.rโ๐)๐ค))))))) |
126 | 125 | imp32 419 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ง โ ๐ โ (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (๐ข(.rโ๐)(๐ฃ(+gโ๐)๐ค)) = ((๐ข(.rโ๐)๐ฃ)(+gโ๐)(๐ข(.rโ๐)๐ค))))) |
127 | 126 | rexlimdv 3153 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (โ๐ง โ ๐ ((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (๐ข(.rโ๐)(๐ฃ(+gโ๐)๐ค)) = ((๐ข(.rโ๐)๐ฃ)(+gโ๐)(๐ข(.rโ๐)๐ค)))) |
128 | 127 | rexlimdvva 3211 |
. . . . 5
โข (๐ โ (โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (๐ข(.rโ๐)(๐ฃ(+gโ๐)๐ค)) = ((๐ข(.rโ๐)๐ฃ)(+gโ๐)(๐ข(.rโ๐)๐ค)))) |
129 | 48, 128 | sylbid 239 |
. . . 4
โข (๐ โ ((๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต) โ (๐ข(.rโ๐)(๐ฃ(+gโ๐)๐ค)) = ((๐ข(.rโ๐)๐ฃ)(+gโ๐)(๐ข(.rโ๐)๐ค)))) |
130 | 129 | imp 407 |
. . 3
โข ((๐ โง (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต)) โ (๐ข(.rโ๐)(๐ฃ(+gโ๐)๐ค)) = ((๐ข(.rโ๐)๐ฃ)(+gโ๐)(๐ข(.rโ๐)๐ค))) |
131 | 25, 8, 17 | ringdir 20081 |
. . . . . . . . . . . . . 14
โข ((๐
โ Ring โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
) โง ๐ง โ (Baseโ๐
))) โ ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) |
132 | 49, 53, 56, 59, 131 | syl13anc 1372 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) |
133 | 132 | fveq2d 6895 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ((๐ฅ + ๐ฆ) ยท ๐ง)) = (๐นโ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
134 | 101 | caovclg 7598 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ + ๐ฆ) โ ๐) |
135 | 134 | 3adantr3 1171 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฅ + ๐ฆ) โ ๐) |
136 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 17480 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ + ๐ฆ) โ ๐ โง ๐ง โ ๐) โ ((๐นโ(๐ฅ + ๐ฆ))(.rโ๐)(๐นโ๐ง)) = (๐นโ((๐ฅ + ๐ฆ) ยท ๐ง))) |
137 | 63, 135, 57, 136 | syl3anc 1371 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ(๐ฅ + ๐ฆ))(.rโ๐)(๐นโ๐ง)) = (๐นโ((๐ฅ + ๐ฆ) ยท ๐ง))) |
138 | 3, 10, 1, 2, 4, 8, 108 | imasaddval 17477 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ ยท ๐ง) โ ๐ โง (๐ฆ ยท ๐ง) โ ๐) โ ((๐นโ(๐ฅ ยท ๐ง))(+gโ๐)(๐นโ(๐ฆ ยท ๐ง))) = (๐นโ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
139 | 63, 107, 70, 138 | syl3anc 1371 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ(๐ฅ ยท ๐ง))(+gโ๐)(๐นโ(๐ฆ ยท ๐ง))) = (๐นโ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง)))) |
140 | 133, 137,
139 | 3eqtr4d 2782 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ(๐ฅ + ๐ฆ))(.rโ๐)(๐นโ๐ง)) = ((๐นโ(๐ฅ ยท ๐ง))(+gโ๐)(๐นโ(๐ฆ ยท ๐ง)))) |
141 | 3, 10, 1, 2, 4, 8, 108 | imasaddval 17477 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) = (๐นโ(๐ฅ + ๐ฆ))) |
142 | 141 | 3adant3r3 1184 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) = (๐นโ(๐ฅ + ๐ฆ))) |
143 | 142 | oveq1d 7423 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))(.rโ๐)(๐นโ๐ง)) = ((๐นโ(๐ฅ + ๐ฆ))(.rโ๐)(๐นโ๐ง))) |
144 | 116, 78 | oveq12d 7426 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง))(+gโ๐)((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง))) = ((๐นโ(๐ฅ ยท ๐ง))(+gโ๐)(๐นโ(๐ฆ ยท ๐ง)))) |
145 | 140, 143,
144 | 3eqtr4d 2782 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))(.rโ๐)(๐นโ๐ง)) = (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง))(+gโ๐)((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง)))) |
146 | 81, 82 | oveq12d 7426 |
. . . . . . . . . . . 12
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) = (๐ข(+gโ๐)๐ฃ)) |
147 | 146, 84 | oveq12d 7426 |
. . . . . . . . . . 11
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))(.rโ๐)(๐นโ๐ง)) = ((๐ข(+gโ๐)๐ฃ)(.rโ๐)๐ค)) |
148 | 121, 86 | oveq12d 7426 |
. . . . . . . . . . 11
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง))(+gโ๐)((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง))) = ((๐ข(.rโ๐)๐ค)(+gโ๐)(๐ฃ(.rโ๐)๐ค))) |
149 | 147, 148 | eqeq12d 2748 |
. . . . . . . . . 10
โข (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))(.rโ๐)(๐นโ๐ง)) = (((๐นโ๐ฅ)(.rโ๐)(๐นโ๐ง))(+gโ๐)((๐นโ๐ฆ)(.rโ๐)(๐นโ๐ง))) โ ((๐ข(+gโ๐)๐ฃ)(.rโ๐)๐ค) = ((๐ข(.rโ๐)๐ค)(+gโ๐)(๐ฃ(.rโ๐)๐ค)))) |
150 | 145, 149 | syl5ibcom 244 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐ข(+gโ๐)๐ฃ)(.rโ๐)๐ค) = ((๐ข(.rโ๐)๐ค)(+gโ๐)(๐ฃ(.rโ๐)๐ค)))) |
151 | 150 | 3exp2 1354 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ โ (๐ฆ โ ๐ โ (๐ง โ ๐ โ (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐ข(+gโ๐)๐ฃ)(.rโ๐)๐ค) = ((๐ข(.rโ๐)๐ค)(+gโ๐)(๐ฃ(.rโ๐)๐ค))))))) |
152 | 151 | imp32 419 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ง โ ๐ โ (((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐ข(+gโ๐)๐ฃ)(.rโ๐)๐ค) = ((๐ข(.rโ๐)๐ค)(+gโ๐)(๐ฃ(.rโ๐)๐ค))))) |
153 | 152 | rexlimdv 3153 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (โ๐ง โ ๐ ((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐ข(+gโ๐)๐ฃ)(.rโ๐)๐ค) = ((๐ข(.rโ๐)๐ค)(+gโ๐)(๐ฃ(.rโ๐)๐ค)))) |
154 | 153 | rexlimdvva 3211 |
. . . . 5
โข (๐ โ (โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐นโ๐ฅ) = ๐ข โง (๐นโ๐ฆ) = ๐ฃ โง (๐นโ๐ง) = ๐ค) โ ((๐ข(+gโ๐)๐ฃ)(.rโ๐)๐ค) = ((๐ข(.rโ๐)๐ค)(+gโ๐)(๐ฃ(.rโ๐)๐ค)))) |
155 | 48, 154 | sylbid 239 |
. . . 4
โข (๐ โ ((๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต) โ ((๐ข(+gโ๐)๐ฃ)(.rโ๐)๐ค) = ((๐ข(.rโ๐)๐ค)(+gโ๐)(๐ฃ(.rโ๐)๐ค)))) |
156 | 155 | imp 407 |
. . 3
โข ((๐ โง (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต)) โ ((๐ข(+gโ๐)๐ฃ)(.rโ๐)๐ค) = ((๐ข(.rโ๐)๐ค)(+gโ๐)(๐ฃ(.rโ๐)๐ค))) |
157 | | fof 6805 |
. . . . 5
โข (๐น:๐โontoโ๐ต โ ๐น:๐โถ๐ต) |
158 | 3, 157 | syl 17 |
. . . 4
โข (๐ โ ๐น:๐โถ๐ต) |
159 | | imasring.o |
. . . . . . 7
โข 1 =
(1rโ๐
) |
160 | 25, 159 | ringidcl 20082 |
. . . . . 6
โข (๐
โ Ring โ 1 โ
(Baseโ๐
)) |
161 | 4, 160 | syl 17 |
. . . . 5
โข (๐ โ 1 โ (Baseโ๐
)) |
162 | 161, 2 | eleqtrrd 2836 |
. . . 4
โข (๐ โ 1 โ ๐) |
163 | 158, 162 | ffvelcdmd 7087 |
. . 3
โข (๐ โ (๐นโ 1 ) โ ๐ต) |
164 | 40, 41 | syl 17 |
. . . . . 6
โข (๐ โ (๐ข โ ran ๐น โ โ๐ฅ โ ๐ (๐นโ๐ฅ) = ๐ข)) |
165 | 35, 164 | bitr3d 280 |
. . . . 5
โข (๐ โ (๐ข โ ๐ต โ โ๐ฅ โ ๐ (๐นโ๐ฅ) = ๐ข)) |
166 | | simpl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐) โ ๐) |
167 | 162 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐) โ 1 โ ๐) |
168 | | simpr 485 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐) โ ๐ฅ โ ๐) |
169 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 17480 |
. . . . . . . . 9
โข ((๐ โง 1 โ ๐ โง ๐ฅ โ ๐) โ ((๐นโ 1
)(.rโ๐)(๐นโ๐ฅ)) = (๐นโ( 1 ยท ๐ฅ))) |
170 | 166, 167,
168, 169 | syl3anc 1371 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐) โ ((๐นโ 1
)(.rโ๐)(๐นโ๐ฅ)) = (๐นโ( 1 ยท ๐ฅ))) |
171 | 2 | eleq2d 2819 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ ๐ โ ๐ฅ โ (Baseโ๐
))) |
172 | 171 | biimpa 477 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐) โ ๐ฅ โ (Baseโ๐
)) |
173 | 25, 17, 159 | ringlidm 20085 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ฅ โ (Baseโ๐
)) โ ( 1 ยท ๐ฅ) = ๐ฅ) |
174 | 4, 172, 173 | syl2an2r 683 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐) โ ( 1 ยท ๐ฅ) = ๐ฅ) |
175 | 174 | fveq2d 6895 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐) โ (๐นโ( 1 ยท ๐ฅ)) = (๐นโ๐ฅ)) |
176 | 170, 175 | eqtrd 2772 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ ((๐นโ 1
)(.rโ๐)(๐นโ๐ฅ)) = (๐นโ๐ฅ)) |
177 | | oveq2 7416 |
. . . . . . . 8
โข ((๐นโ๐ฅ) = ๐ข โ ((๐นโ 1
)(.rโ๐)(๐นโ๐ฅ)) = ((๐นโ 1
)(.rโ๐)๐ข)) |
178 | | id 22 |
. . . . . . . 8
โข ((๐นโ๐ฅ) = ๐ข โ (๐นโ๐ฅ) = ๐ข) |
179 | 177, 178 | eqeq12d 2748 |
. . . . . . 7
โข ((๐นโ๐ฅ) = ๐ข โ (((๐นโ 1
)(.rโ๐)(๐นโ๐ฅ)) = (๐นโ๐ฅ) โ ((๐นโ 1
)(.rโ๐)๐ข) = ๐ข)) |
180 | 176, 179 | syl5ibcom 244 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ ((๐นโ๐ฅ) = ๐ข โ ((๐นโ 1
)(.rโ๐)๐ข) = ๐ข)) |
181 | 180 | rexlimdva 3155 |
. . . . 5
โข (๐ โ (โ๐ฅ โ ๐ (๐นโ๐ฅ) = ๐ข โ ((๐นโ 1
)(.rโ๐)๐ข) = ๐ข)) |
182 | 165, 181 | sylbid 239 |
. . . 4
โข (๐ โ (๐ข โ ๐ต โ ((๐นโ 1
)(.rโ๐)๐ข) = ๐ข)) |
183 | 182 | imp 407 |
. . 3
โข ((๐ โง ๐ข โ ๐ต) โ ((๐นโ 1
)(.rโ๐)๐ข) = ๐ข) |
184 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 17480 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ โง 1 โ ๐) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ 1 )) = (๐นโ(๐ฅ ยท 1 ))) |
185 | 167, 184 | mpd3an3 1462 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ 1 )) = (๐นโ(๐ฅ ยท 1 ))) |
186 | 25, 17, 159 | ringridm 20086 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ฅ โ (Baseโ๐
)) โ (๐ฅ ยท 1 ) = ๐ฅ) |
187 | 4, 172, 186 | syl2an2r 683 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐) โ (๐ฅ ยท 1 ) = ๐ฅ) |
188 | 187 | fveq2d 6895 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐) โ (๐นโ(๐ฅ ยท 1 )) = (๐นโ๐ฅ)) |
189 | 185, 188 | eqtrd 2772 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ 1 )) = (๐นโ๐ฅ)) |
190 | | oveq1 7415 |
. . . . . . . 8
โข ((๐นโ๐ฅ) = ๐ข โ ((๐นโ๐ฅ)(.rโ๐)(๐นโ 1 )) = (๐ข(.rโ๐)(๐นโ 1 ))) |
191 | 190, 178 | eqeq12d 2748 |
. . . . . . 7
โข ((๐นโ๐ฅ) = ๐ข โ (((๐นโ๐ฅ)(.rโ๐)(๐นโ 1 )) = (๐นโ๐ฅ) โ (๐ข(.rโ๐)(๐นโ 1 )) = ๐ข)) |
192 | 189, 191 | syl5ibcom 244 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ ((๐นโ๐ฅ) = ๐ข โ (๐ข(.rโ๐)(๐นโ 1 )) = ๐ข)) |
193 | 192 | rexlimdva 3155 |
. . . . 5
โข (๐ โ (โ๐ฅ โ ๐ (๐นโ๐ฅ) = ๐ข โ (๐ข(.rโ๐)(๐นโ 1 )) = ๐ข)) |
194 | 165, 193 | sylbid 239 |
. . . 4
โข (๐ โ (๐ข โ ๐ต โ (๐ข(.rโ๐)(๐นโ 1 )) = ๐ข)) |
195 | 194 | imp 407 |
. . 3
โข ((๐ โง ๐ข โ ๐ต) โ (๐ข(.rโ๐)(๐นโ 1 )) = ๐ข) |
196 | 5, 6, 7, 15, 32, 95, 130, 156, 163, 183, 195 | isringd 20104 |
. 2
โข (๐ โ ๐ โ Ring) |
197 | 163, 5 | eleqtrd 2835 |
. . . 4
โข (๐ โ (๐นโ 1 ) โ (Baseโ๐)) |
198 | 5 | eleq2d 2819 |
. . . . . 6
โข (๐ โ (๐ข โ ๐ต โ ๐ข โ (Baseโ๐))) |
199 | 182, 194 | jcad 513 |
. . . . . 6
โข (๐ โ (๐ข โ ๐ต โ (((๐นโ 1
)(.rโ๐)๐ข) = ๐ข โง (๐ข(.rโ๐)(๐นโ 1 )) = ๐ข))) |
200 | 198, 199 | sylbird 259 |
. . . . 5
โข (๐ โ (๐ข โ (Baseโ๐) โ (((๐นโ 1
)(.rโ๐)๐ข) = ๐ข โง (๐ข(.rโ๐)(๐นโ 1 )) = ๐ข))) |
201 | 200 | ralrimiv 3145 |
. . . 4
โข (๐ โ โ๐ข โ (Baseโ๐)(((๐นโ 1
)(.rโ๐)๐ข) = ๐ข โง (๐ข(.rโ๐)(๐นโ 1 )) = ๐ข)) |
202 | | eqid 2732 |
. . . . . 6
โข
(Baseโ๐) =
(Baseโ๐) |
203 | | eqid 2732 |
. . . . . 6
โข
(1rโ๐) = (1rโ๐) |
204 | 202, 18, 203 | isringid 20087 |
. . . . 5
โข (๐ โ Ring โ (((๐นโ 1 ) โ (Baseโ๐) โง โ๐ข โ (Baseโ๐)(((๐นโ 1
)(.rโ๐)๐ข) = ๐ข โง (๐ข(.rโ๐)(๐นโ 1 )) = ๐ข)) โ (1rโ๐) = (๐นโ 1 ))) |
205 | 196, 204 | syl 17 |
. . . 4
โข (๐ โ (((๐นโ 1 ) โ (Baseโ๐) โง โ๐ข โ (Baseโ๐)(((๐นโ 1
)(.rโ๐)๐ข) = ๐ข โง (๐ข(.rโ๐)(๐นโ 1 )) = ๐ข)) โ (1rโ๐) = (๐นโ 1 ))) |
206 | 197, 201,
205 | mpbi2and 710 |
. . 3
โข (๐ โ (1rโ๐) = (๐นโ 1 )) |
207 | 206 | eqcomd 2738 |
. 2
โข (๐ โ (๐นโ 1 ) =
(1rโ๐)) |
208 | 196, 207 | jca 512 |
1
โข (๐ โ (๐ โ Ring โง (๐นโ 1 ) =
(1rโ๐))) |