Metamath Proof Explorer


Theorem issrngd

Description: Properties that determine a star ring. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses issrngd.k φ K = Base R
issrngd.p φ + ˙ = + R
issrngd.t φ · ˙ = R
issrngd.c φ ˙ = * R
issrngd.r φ R Ring
issrngd.cl φ x K ˙ x K
issrngd.dp φ x K y K ˙ x + ˙ y = ˙ x + ˙ ˙ y
issrngd.dt φ x K y K ˙ x · ˙ y = ˙ y · ˙ ˙ x
issrngd.id φ x K ˙ ˙ x = x
Assertion issrngd φ R *-Ring

Proof

Step Hyp Ref Expression
1 issrngd.k φ K = Base R
2 issrngd.p φ + ˙ = + R
3 issrngd.t φ · ˙ = R
4 issrngd.c φ ˙ = * R
5 issrngd.r φ R Ring
6 issrngd.cl φ x K ˙ x K
7 issrngd.dp φ x K y K ˙ x + ˙ y = ˙ x + ˙ ˙ y
8 issrngd.dt φ x K y K ˙ x · ˙ y = ˙ y · ˙ ˙ x
9 issrngd.id φ x K ˙ ˙ x = x
10 eqid Base R = Base R
11 eqid 1 R = 1 R
12 eqid opp r R = opp r R
13 12 11 oppr1 1 R = 1 opp r R
14 eqid R = R
15 eqid opp r R = opp r R
16 12 opprring R Ring opp r R Ring
17 5 16 syl φ opp r R Ring
18 id x = 1 R x = 1 R
19 fveq2 x = 1 R x * R = 1 R * R
20 19 fveq2d x = 1 R x * R * R = 1 R * R * R
21 18 20 eqeq12d x = 1 R x = x * R * R 1 R = 1 R * R * R
22 9 ex φ x K ˙ ˙ x = x
23 1 eleq2d φ x K x Base R
24 4 fveq1d φ ˙ x = x * R
25 4 24 fveq12d φ ˙ ˙ x = x * R * R
26 25 eqeq1d φ ˙ ˙ x = x x * R * R = x
27 22 23 26 3imtr3d φ x Base R x * R * R = x
28 27 imp φ x Base R x * R * R = x
29 28 eqcomd φ x Base R x = x * R * R
30 29 ralrimiva φ x Base R x = x * R * R
31 10 11 ringidcl R Ring 1 R Base R
32 5 31 syl φ 1 R Base R
33 21 30 32 rspcdva φ 1 R = 1 R * R * R
34 33 oveq1d φ 1 R R 1 R * R = 1 R * R * R R 1 R * R
35 19 eleq1d x = 1 R x * R Base R 1 R * R Base R
36 6 ex φ x K ˙ x K
37 24 1 eleq12d φ ˙ x K x * R Base R
38 36 23 37 3imtr3d φ x Base R x * R Base R
39 38 ralrimiv φ x Base R x * R Base R
40 35 39 32 rspcdva φ 1 R * R Base R
41 8 3expib φ x K y K ˙ x · ˙ y = ˙ y · ˙ ˙ x
42 1 eleq2d φ y K y Base R
43 23 42 anbi12d φ x K y K x Base R y Base R
44 3 oveqd φ x · ˙ y = x R y
45 4 44 fveq12d φ ˙ x · ˙ y = x R y * R
46 4 fveq1d φ ˙ y = y * R
47 3 46 24 oveq123d φ ˙ y · ˙ ˙ x = y * R R x * R
48 45 47 eqeq12d φ ˙ x · ˙ y = ˙ y · ˙ ˙ x x R y * R = y * R R x * R
49 41 43 48 3imtr3d φ x Base R y Base R x R y * R = y * R R x * R
50 49 ralrimivv φ x Base R y Base R x R y * R = y * R R x * R
51 fvoveq1 x = 1 R x R y * R = 1 R R y * R
52 19 oveq2d x = 1 R y * R R x * R = y * R R 1 R * R
53 51 52 eqeq12d x = 1 R x R y * R = y * R R x * R 1 R R y * R = y * R R 1 R * R
54 oveq2 y = 1 R * R 1 R R y = 1 R R 1 R * R
55 54 fveq2d y = 1 R * R 1 R R y * R = 1 R R 1 R * R * R
56 fveq2 y = 1 R * R y * R = 1 R * R * R
57 56 oveq1d y = 1 R * R y * R R 1 R * R = 1 R * R * R R 1 R * R
58 55 57 eqeq12d y = 1 R * R 1 R R y * R = y * R R 1 R * R 1 R R 1 R * R * R = 1 R * R * R R 1 R * R
59 53 58 rspc2va 1 R Base R 1 R * R Base R x Base R y Base R x R y * R = y * R R x * R 1 R R 1 R * R * R = 1 R * R * R R 1 R * R
60 32 40 50 59 syl21anc φ 1 R R 1 R * R * R = 1 R * R * R R 1 R * R
61 34 60 eqtr4d φ 1 R R 1 R * R = 1 R R 1 R * R * R
62 10 14 11 ringlidm R Ring 1 R * R Base R 1 R R 1 R * R = 1 R * R
63 5 40 62 syl2anc φ 1 R R 1 R * R = 1 R * R
64 63 fveq2d φ 1 R R 1 R * R * R = 1 R * R * R
65 61 63 64 3eqtr3d φ 1 R * R = 1 R * R * R
66 eqid * R = * R
67 eqid 𝑟𝑓 R = 𝑟𝑓 R
68 10 66 67 stafval 1 R Base R 𝑟𝑓 R 1 R = 1 R * R
69 32 68 syl φ 𝑟𝑓 R 1 R = 1 R * R
70 65 69 33 3eqtr4d φ 𝑟𝑓 R 1 R = 1 R
71 49 imp φ x Base R y Base R x R y * R = y * R R x * R
72 10 14 12 15 opprmul x * R opp r R y * R = y * R R x * R
73 71 72 eqtr4di φ x Base R y Base R x R y * R = x * R opp r R y * R
74 10 14 ringcl R Ring x Base R y Base R x R y Base R
75 74 3expb R Ring x Base R y Base R x R y Base R
76 5 75 sylan φ x Base R y Base R x R y Base R
77 10 66 67 stafval x R y Base R 𝑟𝑓 R x R y = x R y * R
78 76 77 syl φ x Base R y Base R 𝑟𝑓 R x R y = x R y * R
79 10 66 67 stafval x Base R 𝑟𝑓 R x = x * R
80 10 66 67 stafval y Base R 𝑟𝑓 R y = y * R
81 79 80 oveqan12d x Base R y Base R 𝑟𝑓 R x opp r R 𝑟𝑓 R y = x * R opp r R y * R
82 81 adantl φ x Base R y Base R 𝑟𝑓 R x opp r R 𝑟𝑓 R y = x * R opp r R y * R
83 73 78 82 3eqtr4d φ x Base R y Base R 𝑟𝑓 R x R y = 𝑟𝑓 R x opp r R 𝑟𝑓 R y
84 12 10 opprbas Base R = Base opp r R
85 eqid + R = + R
86 12 85 oppradd + R = + opp r R
87 38 imp φ x Base R x * R Base R
88 10 66 67 staffval 𝑟𝑓 R = x Base R x * R
89 87 88 fmptd φ 𝑟𝑓 R : Base R Base R
90 7 3expib φ x K y K ˙ x + ˙ y = ˙ x + ˙ ˙ y
91 2 oveqd φ x + ˙ y = x + R y
92 4 91 fveq12d φ ˙ x + ˙ y = x + R y * R
93 2 24 46 oveq123d φ ˙ x + ˙ ˙ y = x * R + R y * R
94 92 93 eqeq12d φ ˙ x + ˙ y = ˙ x + ˙ ˙ y x + R y * R = x * R + R y * R
95 90 43 94 3imtr3d φ x Base R y Base R x + R y * R = x * R + R y * R
96 95 imp φ x Base R y Base R x + R y * R = x * R + R y * R
97 10 85 ringacl R Ring x Base R y Base R x + R y Base R
98 97 3expb R Ring x Base R y Base R x + R y Base R
99 5 98 sylan φ x Base R y Base R x + R y Base R
100 10 66 67 stafval x + R y Base R 𝑟𝑓 R x + R y = x + R y * R
101 99 100 syl φ x Base R y Base R 𝑟𝑓 R x + R y = x + R y * R
102 79 80 oveqan12d x Base R y Base R 𝑟𝑓 R x + R 𝑟𝑓 R y = x * R + R y * R
103 102 adantl φ x Base R y Base R 𝑟𝑓 R x + R 𝑟𝑓 R y = x * R + R y * R
104 96 101 103 3eqtr4d φ x Base R y Base R 𝑟𝑓 R x + R y = 𝑟𝑓 R x + R 𝑟𝑓 R y
105 10 11 13 14 15 5 17 70 83 84 85 86 89 104 isrhmd φ 𝑟𝑓 R R RingHom opp r R
106 10 66 67 staffval 𝑟𝑓 R = y Base R y * R
107 106 fmpt y Base R y * R Base R 𝑟𝑓 R : Base R Base R
108 89 107 sylibr φ y Base R y * R Base R
109 108 r19.21bi φ y Base R y * R Base R
110 id x = y x = y
111 fveq2 x = y x * R = y * R
112 111 fveq2d x = y x * R * R = y * R * R
113 110 112 eqeq12d x = y x = x * R * R y = y * R * R
114 113 rspccva x Base R x = x * R * R y Base R y = y * R * R
115 30 114 sylan φ y Base R y = y * R * R
116 115 adantrl φ x Base R y Base R y = y * R * R
117 fveq2 x = y * R x * R = y * R * R
118 117 eqeq2d x = y * R y = x * R y = y * R * R
119 116 118 syl5ibrcom φ x Base R y Base R x = y * R y = x * R
120 29 adantrr φ x Base R y Base R x = x * R * R
121 fveq2 y = x * R y * R = x * R * R
122 121 eqeq2d y = x * R x = y * R x = x * R * R
123 120 122 syl5ibrcom φ x Base R y Base R y = x * R x = y * R
124 119 123 impbid φ x Base R y Base R x = y * R y = x * R
125 88 87 109 124 f1ocnv2d φ 𝑟𝑓 R : Base R 1-1 onto Base R 𝑟𝑓 R -1 = y Base R y * R
126 125 simprd φ 𝑟𝑓 R -1 = y Base R y * R
127 106 126 eqtr4id φ 𝑟𝑓 R = 𝑟𝑓 R -1
128 12 67 issrng R *-Ring 𝑟𝑓 R R RingHom opp r R 𝑟𝑓 R = 𝑟𝑓 R -1
129 105 127 128 sylanbrc φ R *-Ring