Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
โข
(Baseโ๐
) =
(Baseโ๐
) |
2 | | eqid 2733 |
. . 3
โข
(1rโ๐
) = (1rโ๐
) |
3 | | eqid 2733 |
. . . 4
โข
(opprโ๐
) = (opprโ๐
) |
4 | 3, 2 | oppr1 20071 |
. . 3
โข
(1rโ๐
) =
(1rโ(opprโ๐
)) |
5 | | eqid 2733 |
. . 3
โข
(.rโ๐
) = (.rโ๐
) |
6 | | eqid 2733 |
. . 3
โข
(.rโ(opprโ๐
)) =
(.rโ(opprโ๐
)) |
7 | | issrngd.r |
. . 3
โข (๐ โ ๐
โ Ring) |
8 | 3 | opprring 20068 |
. . . 4
โข (๐
โ Ring โ
(opprโ๐
) โ Ring) |
9 | 7, 8 | syl 17 |
. . 3
โข (๐ โ
(opprโ๐
) โ Ring) |
10 | | id 22 |
. . . . . . . . 9
โข (๐ฅ = (1rโ๐
) โ ๐ฅ = (1rโ๐
)) |
11 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ฅ = (1rโ๐
) โ
((*๐โ๐
)โ๐ฅ) = ((*๐โ๐
)โ(1rโ๐
))) |
12 | 11 | fveq2d 6850 |
. . . . . . . . 9
โข (๐ฅ = (1rโ๐
) โ
((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ)) = ((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
)))) |
13 | 10, 12 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ฅ = (1rโ๐
) โ (๐ฅ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ)) โ (1rโ๐
) =
((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
))))) |
14 | | issrngd.id |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐พ) โ ( โ โ( โ
โ๐ฅ)) = ๐ฅ) |
15 | 14 | ex 414 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ โ ๐พ โ ( โ โ( โ
โ๐ฅ)) = ๐ฅ)) |
16 | | issrngd.k |
. . . . . . . . . . . . 13
โข (๐ โ ๐พ = (Baseโ๐
)) |
17 | 16 | eleq2d 2820 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ โ ๐พ โ ๐ฅ โ (Baseโ๐
))) |
18 | | issrngd.c |
. . . . . . . . . . . . . 14
โข (๐ โ โ =
(*๐โ๐
)) |
19 | 18 | fveq1d 6848 |
. . . . . . . . . . . . . 14
โข (๐ โ ( โ โ๐ฅ) =
((*๐โ๐
)โ๐ฅ)) |
20 | 18, 19 | fveq12d 6853 |
. . . . . . . . . . . . 13
โข (๐ โ ( โ โ( โ
โ๐ฅ)) =
((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ))) |
21 | 20 | eqeq1d 2735 |
. . . . . . . . . . . 12
โข (๐ โ (( โ โ( โ
โ๐ฅ)) = ๐ฅ โ
((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ)) = ๐ฅ)) |
22 | 15, 17, 21 | 3imtr3d 293 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ (Baseโ๐
) โ ((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ)) = ๐ฅ)) |
23 | 22 | imp 408 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (Baseโ๐
)) โ
((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ)) = ๐ฅ) |
24 | 23 | eqcomd 2739 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (Baseโ๐
)) โ ๐ฅ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ))) |
25 | 24 | ralrimiva 3140 |
. . . . . . . 8
โข (๐ โ โ๐ฅ โ (Baseโ๐
)๐ฅ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ))) |
26 | 1, 2 | ringidcl 19997 |
. . . . . . . . 9
โข (๐
โ Ring โ
(1rโ๐
)
โ (Baseโ๐
)) |
27 | 7, 26 | syl 17 |
. . . . . . . 8
โข (๐ โ (1rโ๐
) โ (Baseโ๐
)) |
28 | 13, 25, 27 | rspcdva 3584 |
. . . . . . 7
โข (๐ โ (1rโ๐
) =
((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
)))) |
29 | 28 | oveq1d 7376 |
. . . . . 6
โข (๐ โ
((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
))) =
(((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
)))(.rโ๐
)((*๐โ๐
)โ(1rโ๐
)))) |
30 | 11 | eleq1d 2819 |
. . . . . . . 8
โข (๐ฅ = (1rโ๐
) โ
(((*๐โ๐
)โ๐ฅ) โ (Baseโ๐
) โ ((*๐โ๐
)โ(1rโ๐
)) โ (Baseโ๐
))) |
31 | | issrngd.cl |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐พ) โ ( โ โ๐ฅ) โ ๐พ) |
32 | 31 | ex 414 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ ๐พ โ ( โ โ๐ฅ) โ ๐พ)) |
33 | 19, 16 | eleq12d 2828 |
. . . . . . . . . 10
โข (๐ โ (( โ โ๐ฅ) โ ๐พ โ ((*๐โ๐
)โ๐ฅ) โ (Baseโ๐
))) |
34 | 32, 17, 33 | 3imtr3d 293 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ (Baseโ๐
) โ ((*๐โ๐
)โ๐ฅ) โ (Baseโ๐
))) |
35 | 34 | ralrimiv 3139 |
. . . . . . . 8
โข (๐ โ โ๐ฅ โ (Baseโ๐
)((*๐โ๐
)โ๐ฅ) โ (Baseโ๐
)) |
36 | 30, 35, 27 | rspcdva 3584 |
. . . . . . 7
โข (๐ โ
((*๐โ๐
)โ(1rโ๐
)) โ (Baseโ๐
)) |
37 | | issrngd.dt |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐พ โง ๐ฆ โ ๐พ) โ ( โ โ(๐ฅ ยท ๐ฆ)) = (( โ โ๐ฆ) ยท ( โ
โ๐ฅ))) |
38 | 37 | 3expib 1123 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ ๐พ โง ๐ฆ โ ๐พ) โ ( โ โ(๐ฅ ยท ๐ฆ)) = (( โ โ๐ฆ) ยท ( โ
โ๐ฅ)))) |
39 | 16 | eleq2d 2820 |
. . . . . . . . . 10
โข (๐ โ (๐ฆ โ ๐พ โ ๐ฆ โ (Baseโ๐
))) |
40 | 17, 39 | anbi12d 632 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ ๐พ โง ๐ฆ โ ๐พ) โ (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)))) |
41 | | issrngd.t |
. . . . . . . . . . . 12
โข (๐ โ ยท =
(.rโ๐
)) |
42 | 41 | oveqd 7378 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ ยท ๐ฆ) = (๐ฅ(.rโ๐
)๐ฆ)) |
43 | 18, 42 | fveq12d 6853 |
. . . . . . . . . 10
โข (๐ โ ( โ โ(๐ฅ ยท ๐ฆ)) = ((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ))) |
44 | 18 | fveq1d 6848 |
. . . . . . . . . . 11
โข (๐ โ ( โ โ๐ฆ) =
((*๐โ๐
)โ๐ฆ)) |
45 | 41, 44, 19 | oveq123d 7382 |
. . . . . . . . . 10
โข (๐ โ (( โ โ๐ฆ) ยท ( โ
โ๐ฅ)) =
(((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ๐ฅ))) |
46 | 43, 45 | eqeq12d 2749 |
. . . . . . . . 9
โข (๐ โ (( โ โ(๐ฅ ยท ๐ฆ)) = (( โ โ๐ฆ) ยท ( โ
โ๐ฅ)) โ
((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ๐ฅ)))) |
47 | 38, 40, 46 | 3imtr3d 293 |
. . . . . . . 8
โข (๐ โ ((๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ
((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ๐ฅ)))) |
48 | 47 | ralrimivv 3192 |
. . . . . . 7
โข (๐ โ โ๐ฅ โ (Baseโ๐
)โ๐ฆ โ (Baseโ๐
)((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ๐ฅ))) |
49 | | fvoveq1 7384 |
. . . . . . . . 9
โข (๐ฅ = (1rโ๐
) โ
((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = ((*๐โ๐
)โ((1rโ๐
)(.rโ๐
)๐ฆ))) |
50 | 11 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ฅ = (1rโ๐
) โ
(((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ๐ฅ)) = (((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
)))) |
51 | 49, 50 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ฅ = (1rโ๐
) โ
(((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ๐ฅ)) โ ((*๐โ๐
)โ((1rโ๐
)(.rโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
))))) |
52 | | oveq2 7369 |
. . . . . . . . . 10
โข (๐ฆ =
((*๐โ๐
)โ(1rโ๐
)) โ
((1rโ๐
)(.rโ๐
)๐ฆ) = ((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
)))) |
53 | 52 | fveq2d 6850 |
. . . . . . . . 9
โข (๐ฆ =
((*๐โ๐
)โ(1rโ๐
)) โ
((*๐โ๐
)โ((1rโ๐
)(.rโ๐
)๐ฆ)) = ((*๐โ๐
)โ((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
))))) |
54 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ฆ =
((*๐โ๐
)โ(1rโ๐
)) โ
((*๐โ๐
)โ๐ฆ) = ((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
)))) |
55 | 54 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ฆ =
((*๐โ๐
)โ(1rโ๐
)) โ
(((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
))) =
(((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
)))(.rโ๐
)((*๐โ๐
)โ(1rโ๐
)))) |
56 | 53, 55 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ฆ =
((*๐โ๐
)โ(1rโ๐
)) โ
(((*๐โ๐
)โ((1rโ๐
)(.rโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
))) โ
((*๐โ๐
)โ((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
)))) =
(((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
)))(.rโ๐
)((*๐โ๐
)โ(1rโ๐
))))) |
57 | 51, 56 | rspc2va 3593 |
. . . . . . 7
โข
((((1rโ๐
) โ (Baseโ๐
) โง ((*๐โ๐
)โ(1rโ๐
)) โ (Baseโ๐
)) โง โ๐ฅ โ (Baseโ๐
)โ๐ฆ โ (Baseโ๐
)((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ๐ฅ))) โ
((*๐โ๐
)โ((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
)))) =
(((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
)))(.rโ๐
)((*๐โ๐
)โ(1rโ๐
)))) |
58 | 27, 36, 48, 57 | syl21anc 837 |
. . . . . 6
โข (๐ โ
((*๐โ๐
)โ((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
)))) =
(((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
)))(.rโ๐
)((*๐โ๐
)โ(1rโ๐
)))) |
59 | 29, 58 | eqtr4d 2776 |
. . . . 5
โข (๐ โ
((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
))) =
((*๐โ๐
)โ((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
))))) |
60 | 1, 5, 2 | ringlidm 20000 |
. . . . . 6
โข ((๐
โ Ring โง
((*๐โ๐
)โ(1rโ๐
)) โ (Baseโ๐
)) โ
((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
))) =
((*๐โ๐
)โ(1rโ๐
))) |
61 | 7, 36, 60 | syl2anc 585 |
. . . . 5
โข (๐ โ
((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
))) =
((*๐โ๐
)โ(1rโ๐
))) |
62 | 61 | fveq2d 6850 |
. . . . 5
โข (๐ โ
((*๐โ๐
)โ((1rโ๐
)(.rโ๐
)((*๐โ๐
)โ(1rโ๐
)))) =
((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
)))) |
63 | 59, 61, 62 | 3eqtr3d 2781 |
. . . 4
โข (๐ โ
((*๐โ๐
)โ(1rโ๐
)) =
((*๐โ๐
)โ((*๐โ๐
)โ(1rโ๐
)))) |
64 | | eqid 2733 |
. . . . . 6
โข
(*๐โ๐
) = (*๐โ๐
) |
65 | | eqid 2733 |
. . . . . 6
โข
(*rfโ๐
) = (*rfโ๐
) |
66 | 1, 64, 65 | stafval 20350 |
. . . . 5
โข
((1rโ๐
) โ (Baseโ๐
) โ ((*rfโ๐
)โ(1rโ๐
)) =
((*๐โ๐
)โ(1rโ๐
))) |
67 | 27, 66 | syl 17 |
. . . 4
โข (๐ โ
((*rfโ๐
)โ(1rโ๐
)) =
((*๐โ๐
)โ(1rโ๐
))) |
68 | 63, 67, 28 | 3eqtr4d 2783 |
. . 3
โข (๐ โ
((*rfโ๐
)โ(1rโ๐
)) = (1rโ๐
)) |
69 | 47 | imp 408 |
. . . . 5
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ
((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ๐ฅ))) |
70 | 1, 5, 3, 6 | opprmul 20060 |
. . . . 5
โข
(((*๐โ๐
)โ๐ฅ)(.rโ(opprโ๐
))((*๐โ๐
)โ๐ฆ)) = (((*๐โ๐
)โ๐ฆ)(.rโ๐
)((*๐โ๐
)โ๐ฅ)) |
71 | 69, 70 | eqtr4di 2791 |
. . . 4
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ
((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฅ)(.rโ(opprโ๐
))((*๐โ๐
)โ๐ฆ))) |
72 | 1, 5 | ringcl 19989 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ (๐ฅ(.rโ๐
)๐ฆ) โ (Baseโ๐
)) |
73 | 72 | 3expb 1121 |
. . . . . 6
โข ((๐
โ Ring โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ (๐ฅ(.rโ๐
)๐ฆ) โ (Baseโ๐
)) |
74 | 7, 73 | sylan 581 |
. . . . 5
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ (๐ฅ(.rโ๐
)๐ฆ) โ (Baseโ๐
)) |
75 | 1, 64, 65 | stafval 20350 |
. . . . 5
โข ((๐ฅ(.rโ๐
)๐ฆ) โ (Baseโ๐
) โ ((*rfโ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = ((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ))) |
76 | 74, 75 | syl 17 |
. . . 4
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ
((*rfโ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = ((*๐โ๐
)โ(๐ฅ(.rโ๐
)๐ฆ))) |
77 | 1, 64, 65 | stafval 20350 |
. . . . . 6
โข (๐ฅ โ (Baseโ๐
) โ
((*rfโ๐
)โ๐ฅ) = ((*๐โ๐
)โ๐ฅ)) |
78 | 1, 64, 65 | stafval 20350 |
. . . . . 6
โข (๐ฆ โ (Baseโ๐
) โ
((*rfโ๐
)โ๐ฆ) = ((*๐โ๐
)โ๐ฆ)) |
79 | 77, 78 | oveqan12d 7380 |
. . . . 5
โข ((๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ
(((*rfโ๐
)โ๐ฅ)(.rโ(opprโ๐
))((*rfโ๐
)โ๐ฆ)) = (((*๐โ๐
)โ๐ฅ)(.rโ(opprโ๐
))((*๐โ๐
)โ๐ฆ))) |
80 | 79 | adantl 483 |
. . . 4
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ
(((*rfโ๐
)โ๐ฅ)(.rโ(opprโ๐
))((*rfโ๐
)โ๐ฆ)) = (((*๐โ๐
)โ๐ฅ)(.rโ(opprโ๐
))((*๐โ๐
)โ๐ฆ))) |
81 | 71, 76, 80 | 3eqtr4d 2783 |
. . 3
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ
((*rfโ๐
)โ(๐ฅ(.rโ๐
)๐ฆ)) = (((*rfโ๐
)โ๐ฅ)(.rโ(opprโ๐
))((*rfโ๐
)โ๐ฆ))) |
82 | 3, 1 | opprbas 20064 |
. . 3
โข
(Baseโ๐
) =
(Baseโ(opprโ๐
)) |
83 | | eqid 2733 |
. . 3
โข
(+gโ๐
) = (+gโ๐
) |
84 | 3, 83 | oppradd 20066 |
. . 3
โข
(+gโ๐
) =
(+gโ(opprโ๐
)) |
85 | 34 | imp 408 |
. . . 4
โข ((๐ โง ๐ฅ โ (Baseโ๐
)) โ
((*๐โ๐
)โ๐ฅ) โ (Baseโ๐
)) |
86 | 1, 64, 65 | staffval 20349 |
. . . 4
โข
(*rfโ๐
) = (๐ฅ โ (Baseโ๐
) โฆ
((*๐โ๐
)โ๐ฅ)) |
87 | 85, 86 | fmptd 7066 |
. . 3
โข (๐ โ
(*rfโ๐
):(Baseโ๐
)โถ(Baseโ๐
)) |
88 | | issrngd.dp |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐พ โง ๐ฆ โ ๐พ) โ ( โ โ(๐ฅ + ๐ฆ)) = (( โ โ๐ฅ) + ( โ โ๐ฆ))) |
89 | 88 | 3expib 1123 |
. . . . . 6
โข (๐ โ ((๐ฅ โ ๐พ โง ๐ฆ โ ๐พ) โ ( โ โ(๐ฅ + ๐ฆ)) = (( โ โ๐ฅ) + ( โ โ๐ฆ)))) |
90 | | issrngd.p |
. . . . . . . . 9
โข (๐ โ + =
(+gโ๐
)) |
91 | 90 | oveqd 7378 |
. . . . . . . 8
โข (๐ โ (๐ฅ + ๐ฆ) = (๐ฅ(+gโ๐
)๐ฆ)) |
92 | 18, 91 | fveq12d 6853 |
. . . . . . 7
โข (๐ โ ( โ โ(๐ฅ + ๐ฆ)) = ((*๐โ๐
)โ(๐ฅ(+gโ๐
)๐ฆ))) |
93 | 90, 19, 44 | oveq123d 7382 |
. . . . . . 7
โข (๐ โ (( โ โ๐ฅ) + ( โ โ๐ฆ)) =
(((*๐โ๐
)โ๐ฅ)(+gโ๐
)((*๐โ๐
)โ๐ฆ))) |
94 | 92, 93 | eqeq12d 2749 |
. . . . . 6
โข (๐ โ (( โ โ(๐ฅ + ๐ฆ)) = (( โ โ๐ฅ) + ( โ โ๐ฆ)) โ
((*๐โ๐
)โ(๐ฅ(+gโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฅ)(+gโ๐
)((*๐โ๐
)โ๐ฆ)))) |
95 | 89, 40, 94 | 3imtr3d 293 |
. . . . 5
โข (๐ โ ((๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ
((*๐โ๐
)โ(๐ฅ(+gโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฅ)(+gโ๐
)((*๐โ๐
)โ๐ฆ)))) |
96 | 95 | imp 408 |
. . . 4
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ
((*๐โ๐
)โ(๐ฅ(+gโ๐
)๐ฆ)) = (((*๐โ๐
)โ๐ฅ)(+gโ๐
)((*๐โ๐
)โ๐ฆ))) |
97 | 1, 83 | ringacl 20007 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ (๐ฅ(+gโ๐
)๐ฆ) โ (Baseโ๐
)) |
98 | 97 | 3expb 1121 |
. . . . . 6
โข ((๐
โ Ring โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ (๐ฅ(+gโ๐
)๐ฆ) โ (Baseโ๐
)) |
99 | 7, 98 | sylan 581 |
. . . . 5
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ (๐ฅ(+gโ๐
)๐ฆ) โ (Baseโ๐
)) |
100 | 1, 64, 65 | stafval 20350 |
. . . . 5
โข ((๐ฅ(+gโ๐
)๐ฆ) โ (Baseโ๐
) โ ((*rfโ๐
)โ(๐ฅ(+gโ๐
)๐ฆ)) = ((*๐โ๐
)โ(๐ฅ(+gโ๐
)๐ฆ))) |
101 | 99, 100 | syl 17 |
. . . 4
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ
((*rfโ๐
)โ(๐ฅ(+gโ๐
)๐ฆ)) = ((*๐โ๐
)โ(๐ฅ(+gโ๐
)๐ฆ))) |
102 | 77, 78 | oveqan12d 7380 |
. . . . 5
โข ((๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ
(((*rfโ๐
)โ๐ฅ)(+gโ๐
)((*rfโ๐
)โ๐ฆ)) = (((*๐โ๐
)โ๐ฅ)(+gโ๐
)((*๐โ๐
)โ๐ฆ))) |
103 | 102 | adantl 483 |
. . . 4
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ
(((*rfโ๐
)โ๐ฅ)(+gโ๐
)((*rfโ๐
)โ๐ฆ)) = (((*๐โ๐
)โ๐ฅ)(+gโ๐
)((*๐โ๐
)โ๐ฆ))) |
104 | 96, 101, 103 | 3eqtr4d 2783 |
. . 3
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ
((*rfโ๐
)โ(๐ฅ(+gโ๐
)๐ฆ)) = (((*rfโ๐
)โ๐ฅ)(+gโ๐
)((*rfโ๐
)โ๐ฆ))) |
105 | 1, 2, 4, 5, 6, 7, 9, 68, 81, 82, 83, 84, 87, 104 | isrhmd 20171 |
. 2
โข (๐ โ
(*rfโ๐
) โ (๐
RingHom (opprโ๐
))) |
106 | 1, 64, 65 | staffval 20349 |
. . 3
โข
(*rfโ๐
) = (๐ฆ โ (Baseโ๐
) โฆ
((*๐โ๐
)โ๐ฆ)) |
107 | 106 | fmpt 7062 |
. . . . . . 7
โข
(โ๐ฆ โ
(Baseโ๐
)((*๐โ๐
)โ๐ฆ) โ (Baseโ๐
) โ (*rfโ๐
):(Baseโ๐
)โถ(Baseโ๐
)) |
108 | 87, 107 | sylibr 233 |
. . . . . 6
โข (๐ โ โ๐ฆ โ (Baseโ๐
)((*๐โ๐
)โ๐ฆ) โ (Baseโ๐
)) |
109 | 108 | r19.21bi 3233 |
. . . . 5
โข ((๐ โง ๐ฆ โ (Baseโ๐
)) โ
((*๐โ๐
)โ๐ฆ) โ (Baseโ๐
)) |
110 | | id 22 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ฆ โ ๐ฅ = ๐ฆ) |
111 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ฆ โ ((*๐โ๐
)โ๐ฅ) = ((*๐โ๐
)โ๐ฆ)) |
112 | 111 | fveq2d 6850 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ฆ โ ((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ)) = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฆ))) |
113 | 110, 112 | eqeq12d 2749 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (๐ฅ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ)) โ ๐ฆ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฆ)))) |
114 | 113 | rspccva 3582 |
. . . . . . . . 9
โข
((โ๐ฅ โ
(Baseโ๐
)๐ฅ =
((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ)) โง ๐ฆ โ (Baseโ๐
)) โ ๐ฆ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฆ))) |
115 | 25, 114 | sylan 581 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ (Baseโ๐
)) โ ๐ฆ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฆ))) |
116 | 115 | adantrl 715 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ ๐ฆ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฆ))) |
117 | | fveq2 6846 |
. . . . . . . 8
โข (๐ฅ =
((*๐โ๐
)โ๐ฆ) โ ((*๐โ๐
)โ๐ฅ) = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฆ))) |
118 | 117 | eqeq2d 2744 |
. . . . . . 7
โข (๐ฅ =
((*๐โ๐
)โ๐ฆ) โ (๐ฆ = ((*๐โ๐
)โ๐ฅ) โ ๐ฆ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฆ)))) |
119 | 116, 118 | syl5ibrcom 247 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ (๐ฅ = ((*๐โ๐
)โ๐ฆ) โ ๐ฆ = ((*๐โ๐
)โ๐ฅ))) |
120 | 24 | adantrr 716 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ ๐ฅ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ))) |
121 | | fveq2 6846 |
. . . . . . . 8
โข (๐ฆ =
((*๐โ๐
)โ๐ฅ) โ ((*๐โ๐
)โ๐ฆ) = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ))) |
122 | 121 | eqeq2d 2744 |
. . . . . . 7
โข (๐ฆ =
((*๐โ๐
)โ๐ฅ) โ (๐ฅ = ((*๐โ๐
)โ๐ฆ) โ ๐ฅ = ((*๐โ๐
)โ((*๐โ๐
)โ๐ฅ)))) |
123 | 120, 122 | syl5ibrcom 247 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ (๐ฆ = ((*๐โ๐
)โ๐ฅ) โ ๐ฅ = ((*๐โ๐
)โ๐ฆ))) |
124 | 119, 123 | impbid 211 |
. . . . 5
โข ((๐ โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))) โ (๐ฅ = ((*๐โ๐
)โ๐ฆ) โ ๐ฆ = ((*๐โ๐
)โ๐ฅ))) |
125 | 86, 85, 109, 124 | f1ocnv2d 7610 |
. . . 4
โข (๐ โ
((*rfโ๐
):(Baseโ๐
)โ1-1-ontoโ(Baseโ๐
) โง โก(*rfโ๐
) = (๐ฆ โ (Baseโ๐
) โฆ
((*๐โ๐
)โ๐ฆ)))) |
126 | 125 | simprd 497 |
. . 3
โข (๐ โ โก(*rfโ๐
) = (๐ฆ โ (Baseโ๐
) โฆ
((*๐โ๐
)โ๐ฆ))) |
127 | 106, 126 | eqtr4id 2792 |
. 2
โข (๐ โ
(*rfโ๐
) = โก(*rfโ๐
)) |
128 | 3, 65 | issrng 20352 |
. 2
โข (๐
โ *-Ring โ
((*rfโ๐
) โ (๐
RingHom (opprโ๐
)) โง
(*rfโ๐
) = โก(*rfโ๐
))) |
129 | 105, 127,
128 | sylanbrc 584 |
1
โข (๐ โ ๐
โ *-Ring) |