Metamath Proof Explorer


Theorem imasring

Description: The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses imasring.u φ U = F 𝑠 R
imasring.v φ V = Base R
imasring.p + ˙ = + R
imasring.t · ˙ = R
imasring.o 1 ˙ = 1 R
imasring.f φ F : V onto B
imasring.e1 φ a V b V p V q V F a = F p F b = F q F a + ˙ b = F p + ˙ q
imasring.e2 φ a V b V p V q V F a = F p F b = F q F a · ˙ b = F p · ˙ q
imasring.r φ R Ring
Assertion imasring φ U Ring F 1 ˙ = 1 U

Proof

Step Hyp Ref Expression
1 imasring.u φ U = F 𝑠 R
2 imasring.v φ V = Base R
3 imasring.p + ˙ = + R
4 imasring.t · ˙ = R
5 imasring.o 1 ˙ = 1 R
6 imasring.f φ F : V onto B
7 imasring.e1 φ a V b V p V q V F a = F p F b = F q F a + ˙ b = F p + ˙ q
8 imasring.e2 φ a V b V p V q V F a = F p F b = F q F a · ˙ b = F p · ˙ q
9 imasring.r φ R Ring
10 1 2 6 9 imasbas φ B = Base U
11 eqidd φ + U = + U
12 eqidd φ U = U
13 3 a1i φ + ˙ = + R
14 ringgrp R Ring R Grp
15 9 14 syl φ R Grp
16 eqid 0 R = 0 R
17 1 2 13 6 7 15 16 imasgrp φ U Grp F 0 R = 0 U
18 17 simpld φ U Grp
19 eqid U = U
20 9 adantr φ u V v V R Ring
21 simprl φ u V v V u V
22 2 adantr φ u V v V V = Base R
23 21 22 eleqtrd φ u V v V u Base R
24 simprr φ u V v V v V
25 24 22 eleqtrd φ u V v V v Base R
26 eqid Base R = Base R
27 26 4 ringcl R Ring u Base R v Base R u · ˙ v Base R
28 20 23 25 27 syl3anc φ u V v V u · ˙ v Base R
29 28 22 eleqtrrd φ u V v V u · ˙ v V
30 29 caovclg φ p V q V p · ˙ q V
31 6 8 1 2 9 4 19 30 imasmulf φ U : B × B B
32 fovrn U : B × B B u B v B u U v B
33 31 32 syl3an1 φ u B v B u U v B
34 forn F : V onto B ran F = B
35 6 34 syl φ ran F = B
36 35 eleq2d φ u ran F u B
37 35 eleq2d φ v ran F v B
38 35 eleq2d φ w ran F w B
39 36 37 38 3anbi123d φ u ran F v ran F w ran F u B v B w B
40 fofn F : V onto B F Fn V
41 6 40 syl φ F Fn V
42 fvelrnb F Fn V u ran F x V F x = u
43 fvelrnb F Fn V v ran F y V F y = v
44 fvelrnb F Fn V w ran F z V F z = w
45 42 43 44 3anbi123d F Fn V u ran F v ran F w ran F x V F x = u y V F y = v z V F z = w
46 41 45 syl φ u ran F v ran F w ran F x V F x = u y V F y = v z V F z = w
47 39 46 bitr3d φ u B v B w B x V F x = u y V F y = v z V F z = w
48 3reeanv x V y V z V F x = u F y = v F z = w x V F x = u y V F y = v z V F z = w
49 47 48 bitr4di φ u B v B w B x V y V z V F x = u F y = v F z = w
50 9 adantr φ x V y V z V R Ring
51 simp2 φ x V y V x V
52 2 3ad2ant1 φ x V y V V = Base R
53 51 52 eleqtrd φ x V y V x Base R
54 53 3adant3r3 φ x V y V z V x Base R
55 simp3 φ x V y V y V
56 55 52 eleqtrd φ x V y V y Base R
57 56 3adant3r3 φ x V y V z V y Base R
58 simpr3 φ x V y V z V z V
59 2 adantr φ x V y V z V V = Base R
60 58 59 eleqtrd φ x V y V z V z Base R
61 26 4 ringass R Ring x Base R y Base R z Base R x · ˙ y · ˙ z = x · ˙ y · ˙ z
62 50 54 57 60 61 syl13anc φ x V y V z V x · ˙ y · ˙ z = x · ˙ y · ˙ z
63 62 fveq2d φ x V y V z V F x · ˙ y · ˙ z = F x · ˙ y · ˙ z
64 simpl φ x V y V z V φ
65 29 caovclg φ x V y V x · ˙ y V
66 65 3adantr3 φ x V y V z V x · ˙ y V
67 6 8 1 2 9 4 19 imasmulval φ x · ˙ y V z V F x · ˙ y U F z = F x · ˙ y · ˙ z
68 64 66 58 67 syl3anc φ x V y V z V F x · ˙ y U F z = F x · ˙ y · ˙ z
69 simpr1 φ x V y V z V x V
70 29 caovclg φ y V z V y · ˙ z V
71 70 3adantr1 φ x V y V z V y · ˙ z V
72 6 8 1 2 9 4 19 imasmulval φ x V y · ˙ z V F x U F y · ˙ z = F x · ˙ y · ˙ z
73 64 69 71 72 syl3anc φ x V y V z V F x U F y · ˙ z = F x · ˙ y · ˙ z
74 63 68 73 3eqtr4d φ x V y V z V F x · ˙ y U F z = F x U F y · ˙ z
75 6 8 1 2 9 4 19 imasmulval φ x V y V F x U F y = F x · ˙ y
76 75 3adant3r3 φ x V y V z V F x U F y = F x · ˙ y
77 76 oveq1d φ x V y V z V F x U F y U F z = F x · ˙ y U F z
78 6 8 1 2 9 4 19 imasmulval φ y V z V F y U F z = F y · ˙ z
79 78 3adant3r1 φ x V y V z V F y U F z = F y · ˙ z
80 79 oveq2d φ x V y V z V F x U F y U F z = F x U F y · ˙ z
81 74 77 80 3eqtr4d φ x V y V z V F x U F y U F z = F x U F y U F z
82 simp1 F x = u F y = v F z = w F x = u
83 simp2 F x = u F y = v F z = w F y = v
84 82 83 oveq12d F x = u F y = v F z = w F x U F y = u U v
85 simp3 F x = u F y = v F z = w F z = w
86 84 85 oveq12d F x = u F y = v F z = w F x U F y U F z = u U v U w
87 83 85 oveq12d F x = u F y = v F z = w F y U F z = v U w
88 82 87 oveq12d F x = u F y = v F z = w F x U F y U F z = u U v U w
89 86 88 eqeq12d F x = u F y = v F z = w F x U F y U F z = F x U F y U F z u U v U w = u U v U w
90 81 89 syl5ibcom φ x V y V z V F x = u F y = v F z = w u U v U w = u U v U w
91 90 3exp2 φ x V y V z V F x = u F y = v F z = w u U v U w = u U v U w
92 91 imp32 φ x V y V z V F x = u F y = v F z = w u U v U w = u U v U w
93 92 rexlimdv φ x V y V z V F x = u F y = v F z = w u U v U w = u U v U w
94 93 rexlimdvva φ x V y V z V F x = u F y = v F z = w u U v U w = u U v U w
95 49 94 sylbid φ u B v B w B u U v U w = u U v U w
96 95 imp φ u B v B w B u U v U w = u U v U w
97 26 3 4 ringdi R Ring x Base R y Base R z Base R x · ˙ y + ˙ z = x · ˙ y + ˙ x · ˙ z
98 50 54 57 60 97 syl13anc φ x V y V z V x · ˙ y + ˙ z = x · ˙ y + ˙ x · ˙ z
99 98 fveq2d φ x V y V z V F x · ˙ y + ˙ z = F x · ˙ y + ˙ x · ˙ z
100 26 3 ringacl R Ring u Base R v Base R u + ˙ v Base R
101 20 23 25 100 syl3anc φ u V v V u + ˙ v Base R
102 101 22 eleqtrrd φ u V v V u + ˙ v V
103 102 caovclg φ y V z V y + ˙ z V
104 103 3adantr1 φ x V y V z V y + ˙ z V
105 6 8 1 2 9 4 19 imasmulval φ x V y + ˙ z V F x U F y + ˙ z = F x · ˙ y + ˙ z
106 64 69 104 105 syl3anc φ x V y V z V F x U F y + ˙ z = F x · ˙ y + ˙ z
107 29 caovclg φ x V z V x · ˙ z V
108 107 3adantr2 φ x V y V z V x · ˙ z V
109 eqid + U = + U
110 6 7 1 2 9 3 109 imasaddval φ x · ˙ y V x · ˙ z V F x · ˙ y + U F x · ˙ z = F x · ˙ y + ˙ x · ˙ z
111 64 66 108 110 syl3anc φ x V y V z V F x · ˙ y + U F x · ˙ z = F x · ˙ y + ˙ x · ˙ z
112 99 106 111 3eqtr4d φ x V y V z V F x U F y + ˙ z = F x · ˙ y + U F x · ˙ z
113 6 7 1 2 9 3 109 imasaddval φ y V z V F y + U F z = F y + ˙ z
114 113 3adant3r1 φ x V y V z V F y + U F z = F y + ˙ z
115 114 oveq2d φ x V y V z V F x U F y + U F z = F x U F y + ˙ z
116 6 8 1 2 9 4 19 imasmulval φ x V z V F x U F z = F x · ˙ z
117 116 3adant3r2 φ x V y V z V F x U F z = F x · ˙ z
118 76 117 oveq12d φ x V y V z V F x U F y + U F x U F z = F x · ˙ y + U F x · ˙ z
119 112 115 118 3eqtr4d φ x V y V z V F x U F y + U F z = F x U F y + U F x U F z
120 83 85 oveq12d F x = u F y = v F z = w F y + U F z = v + U w
121 82 120 oveq12d F x = u F y = v F z = w F x U F y + U F z = u U v + U w
122 82 85 oveq12d F x = u F y = v F z = w F x U F z = u U w
123 84 122 oveq12d F x = u F y = v F z = w F x U F y + U F x U F z = u U v + U u U w
124 121 123 eqeq12d F x = u F y = v F z = w F x U F y + U F z = F x U F y + U F x U F z u U v + U w = u U v + U u U w
125 119 124 syl5ibcom φ x V y V z V F x = u F y = v F z = w u U v + U w = u U v + U u U w
126 125 3exp2 φ x V y V z V F x = u F y = v F z = w u U v + U w = u U v + U u U w
127 126 imp32 φ x V y V z V F x = u F y = v F z = w u U v + U w = u U v + U u U w
128 127 rexlimdv φ x V y V z V F x = u F y = v F z = w u U v + U w = u U v + U u U w
129 128 rexlimdvva φ x V y V z V F x = u F y = v F z = w u U v + U w = u U v + U u U w
130 49 129 sylbid φ u B v B w B u U v + U w = u U v + U u U w
131 130 imp φ u B v B w B u U v + U w = u U v + U u U w
132 26 3 4 ringdir R Ring x Base R y Base R z Base R x + ˙ y · ˙ z = x · ˙ z + ˙ y · ˙ z
133 50 54 57 60 132 syl13anc φ x V y V z V x + ˙ y · ˙ z = x · ˙ z + ˙ y · ˙ z
134 133 fveq2d φ x V y V z V F x + ˙ y · ˙ z = F x · ˙ z + ˙ y · ˙ z
135 102 caovclg φ x V y V x + ˙ y V
136 135 3adantr3 φ x V y V z V x + ˙ y V
137 6 8 1 2 9 4 19 imasmulval φ x + ˙ y V z V F x + ˙ y U F z = F x + ˙ y · ˙ z
138 64 136 58 137 syl3anc φ x V y V z V F x + ˙ y U F z = F x + ˙ y · ˙ z
139 6 7 1 2 9 3 109 imasaddval φ x · ˙ z V y · ˙ z V F x · ˙ z + U F y · ˙ z = F x · ˙ z + ˙ y · ˙ z
140 64 108 71 139 syl3anc φ x V y V z V F x · ˙ z + U F y · ˙ z = F x · ˙ z + ˙ y · ˙ z
141 134 138 140 3eqtr4d φ x V y V z V F x + ˙ y U F z = F x · ˙ z + U F y · ˙ z
142 6 7 1 2 9 3 109 imasaddval φ x V y V F x + U F y = F x + ˙ y
143 142 3adant3r3 φ x V y V z V F x + U F y = F x + ˙ y
144 143 oveq1d φ x V y V z V F x + U F y U F z = F x + ˙ y U F z
145 117 79 oveq12d φ x V y V z V F x U F z + U F y U F z = F x · ˙ z + U F y · ˙ z
146 141 144 145 3eqtr4d φ x V y V z V F x + U F y U F z = F x U F z + U F y U F z
147 82 83 oveq12d F x = u F y = v F z = w F x + U F y = u + U v
148 147 85 oveq12d F x = u F y = v F z = w F x + U F y U F z = u + U v U w
149 122 87 oveq12d F x = u F y = v F z = w F x U F z + U F y U F z = u U w + U v U w
150 148 149 eqeq12d F x = u F y = v F z = w F x + U F y U F z = F x U F z + U F y U F z u + U v U w = u U w + U v U w
151 146 150 syl5ibcom φ x V y V z V F x = u F y = v F z = w u + U v U w = u U w + U v U w
152 151 3exp2 φ x V y V z V F x = u F y = v F z = w u + U v U w = u U w + U v U w
153 152 imp32 φ x V y V z V F x = u F y = v F z = w u + U v U w = u U w + U v U w
154 153 rexlimdv φ x V y V z V F x = u F y = v F z = w u + U v U w = u U w + U v U w
155 154 rexlimdvva φ x V y V z V F x = u F y = v F z = w u + U v U w = u U w + U v U w
156 49 155 sylbid φ u B v B w B u + U v U w = u U w + U v U w
157 156 imp φ u B v B w B u + U v U w = u U w + U v U w
158 fof F : V onto B F : V B
159 6 158 syl φ F : V B
160 26 5 ringidcl R Ring 1 ˙ Base R
161 9 160 syl φ 1 ˙ Base R
162 161 2 eleqtrrd φ 1 ˙ V
163 159 162 ffvelrnd φ F 1 ˙ B
164 41 42 syl φ u ran F x V F x = u
165 36 164 bitr3d φ u B x V F x = u
166 simpl φ x V φ
167 162 adantr φ x V 1 ˙ V
168 simpr φ x V x V
169 6 8 1 2 9 4 19 imasmulval φ 1 ˙ V x V F 1 ˙ U F x = F 1 ˙ · ˙ x
170 166 167 168 169 syl3anc φ x V F 1 ˙ U F x = F 1 ˙ · ˙ x
171 2 eleq2d φ x V x Base R
172 171 biimpa φ x V x Base R
173 26 4 5 ringlidm R Ring x Base R 1 ˙ · ˙ x = x
174 9 172 173 syl2an2r φ x V 1 ˙ · ˙ x = x
175 174 fveq2d φ x V F 1 ˙ · ˙ x = F x
176 170 175 eqtrd φ x V F 1 ˙ U F x = F x
177 oveq2 F x = u F 1 ˙ U F x = F 1 ˙ U u
178 id F x = u F x = u
179 177 178 eqeq12d F x = u F 1 ˙ U F x = F x F 1 ˙ U u = u
180 176 179 syl5ibcom φ x V F x = u F 1 ˙ U u = u
181 180 rexlimdva φ x V F x = u F 1 ˙ U u = u
182 165 181 sylbid φ u B F 1 ˙ U u = u
183 182 imp φ u B F 1 ˙ U u = u
184 6 8 1 2 9 4 19 imasmulval φ x V 1 ˙ V F x U F 1 ˙ = F x · ˙ 1 ˙
185 167 184 mpd3an3 φ x V F x U F 1 ˙ = F x · ˙ 1 ˙
186 26 4 5 ringridm R Ring x Base R x · ˙ 1 ˙ = x
187 9 172 186 syl2an2r φ x V x · ˙ 1 ˙ = x
188 187 fveq2d φ x V F x · ˙ 1 ˙ = F x
189 185 188 eqtrd φ x V F x U F 1 ˙ = F x
190 oveq1 F x = u F x U F 1 ˙ = u U F 1 ˙
191 190 178 eqeq12d F x = u F x U F 1 ˙ = F x u U F 1 ˙ = u
192 189 191 syl5ibcom φ x V F x = u u U F 1 ˙ = u
193 192 rexlimdva φ x V F x = u u U F 1 ˙ = u
194 165 193 sylbid φ u B u U F 1 ˙ = u
195 194 imp φ u B u U F 1 ˙ = u
196 10 11 12 18 33 96 131 157 163 183 195 isringd φ U Ring
197 163 10 eleqtrd φ F 1 ˙ Base U
198 10 eleq2d φ u B u Base U
199 182 194 jcad φ u B F 1 ˙ U u = u u U F 1 ˙ = u
200 198 199 sylbird φ u Base U F 1 ˙ U u = u u U F 1 ˙ = u
201 200 ralrimiv φ u Base U F 1 ˙ U u = u u U F 1 ˙ = u
202 eqid Base U = Base U
203 eqid 1 U = 1 U
204 202 19 203 isringid U Ring F 1 ˙ Base U u Base U F 1 ˙ U u = u u U F 1 ˙ = u 1 U = F 1 ˙
205 196 204 syl φ F 1 ˙ Base U u Base U F 1 ˙ U u = u u U F 1 ˙ = u 1 U = F 1 ˙
206 197 201 205 mpbi2and φ 1 U = F 1 ˙
207 206 eqcomd φ F 1 ˙ = 1 U
208 196 207 jca φ U Ring F 1 ˙ = 1 U