Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  keridl Structured version   Visualization version   GIF version

Theorem keridl 35370
 Description: The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.)
Hypotheses
Ref Expression
keridl.1 𝐺 = (1st𝑆)
keridl.2 𝑍 = (GId‘𝐺)
Assertion
Ref Expression
keridl ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹 “ {𝑍}) ∈ (Idl‘𝑅))

Proof of Theorem keridl
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnvimass 5930 . . 3 (𝐹 “ {𝑍}) ⊆ dom 𝐹
2 eqid 2824 . . . 4 (1st𝑅) = (1st𝑅)
3 eqid 2824 . . . 4 ran (1st𝑅) = ran (1st𝑅)
4 keridl.1 . . . 4 𝐺 = (1st𝑆)
5 eqid 2824 . . . 4 ran 𝐺 = ran 𝐺
62, 3, 4, 5rngohomf 35304 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st𝑅)⟶ran 𝐺)
71, 6fssdm 6511 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹 “ {𝑍}) ⊆ ran (1st𝑅))
8 eqid 2824 . . . . 5 (GId‘(1st𝑅)) = (GId‘(1st𝑅))
92, 3, 8rngo0cl 35257 . . . 4 (𝑅 ∈ RingOps → (GId‘(1st𝑅)) ∈ ran (1st𝑅))
1093ad2ant1 1130 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (GId‘(1st𝑅)) ∈ ran (1st𝑅))
11 keridl.2 . . . . 5 𝑍 = (GId‘𝐺)
122, 8, 4, 11rngohom0 35310 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(1st𝑅))) = 𝑍)
13 fvex 6664 . . . . 5 (𝐹‘(GId‘(1st𝑅))) ∈ V
1413elsn 4563 . . . 4 ((𝐹‘(GId‘(1st𝑅))) ∈ {𝑍} ↔ (𝐹‘(GId‘(1st𝑅))) = 𝑍)
1512, 14sylibr 237 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(1st𝑅))) ∈ {𝑍})
16 ffn 6495 . . . 4 (𝐹:ran (1st𝑅)⟶ran 𝐺𝐹 Fn ran (1st𝑅))
17 elpreima 6809 . . . 4 (𝐹 Fn ran (1st𝑅) → ((GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}) ↔ ((GId‘(1st𝑅)) ∈ ran (1st𝑅) ∧ (𝐹‘(GId‘(1st𝑅))) ∈ {𝑍})))
186, 16, 173syl 18 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}) ↔ ((GId‘(1st𝑅)) ∈ ran (1st𝑅) ∧ (𝐹‘(GId‘(1st𝑅))) ∈ {𝑍})))
1910, 15, 18mpbir2and 712 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}))
20 an4 655 . . . . . . . 8 (((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})) ↔ ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ ((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍})))
212, 3, 4rngohomadd 35307 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)𝐺(𝐹𝑦)))
2221adantr 484 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)𝐺(𝐹𝑦)))
23 oveq12 7147 . . . . . . . . . . . . . 14 (((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍) → ((𝐹𝑥)𝐺(𝐹𝑦)) = (𝑍𝐺𝑍))
2423adantl 485 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → ((𝐹𝑥)𝐺(𝐹𝑦)) = (𝑍𝐺𝑍))
254rngogrpo 35248 . . . . . . . . . . . . . . . 16 (𝑆 ∈ RingOps → 𝐺 ∈ GrpOp)
265, 11grpoidcl 28286 . . . . . . . . . . . . . . . 16 (𝐺 ∈ GrpOp → 𝑍 ∈ ran 𝐺)
275, 11grpolid 28288 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ GrpOp ∧ 𝑍 ∈ ran 𝐺) → (𝑍𝐺𝑍) = 𝑍)
2825, 26, 27syl2anc2 588 . . . . . . . . . . . . . . 15 (𝑆 ∈ RingOps → (𝑍𝐺𝑍) = 𝑍)
29283ad2ant2 1131 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑍𝐺𝑍) = 𝑍)
3029ad2antrr 725 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → (𝑍𝐺𝑍) = 𝑍)
3122, 24, 303eqtrd 2863 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = 𝑍)
3231ex 416 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍) → (𝐹‘(𝑥(1st𝑅)𝑦)) = 𝑍))
33 fvex 6664 . . . . . . . . . . . . 13 (𝐹𝑥) ∈ V
3433elsn 4563 . . . . . . . . . . . 12 ((𝐹𝑥) ∈ {𝑍} ↔ (𝐹𝑥) = 𝑍)
35 fvex 6664 . . . . . . . . . . . . 13 (𝐹𝑦) ∈ V
3635elsn 4563 . . . . . . . . . . . 12 ((𝐹𝑦) ∈ {𝑍} ↔ (𝐹𝑦) = 𝑍)
3734, 36anbi12i 629 . . . . . . . . . . 11 (((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍}) ↔ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍))
38 fvex 6664 . . . . . . . . . . . 12 (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ V
3938elsn 4563 . . . . . . . . . . 11 ((𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍} ↔ (𝐹‘(𝑥(1st𝑅)𝑦)) = 𝑍)
4032, 37, 393imtr4g 299 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍}) → (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍}))
4140imdistanda 575 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ ((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍})) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
422, 3rngogcl 35250 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
43423expib 1119 . . . . . . . . . . 11 (𝑅 ∈ RingOps → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅)))
44433ad2ant1 1130 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅)))
4544anim1d 613 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍}) → ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
4641, 45syld 47 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ ((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍})) → ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
4720, 46syl5bi 245 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})) → ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
48 elpreima 6809 . . . . . . . . 9 (𝐹 Fn ran (1st𝑅) → (𝑥 ∈ (𝐹 “ {𝑍}) ↔ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍})))
496, 16, 483syl 18 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑥 ∈ (𝐹 “ {𝑍}) ↔ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍})))
50 elpreima 6809 . . . . . . . . 9 (𝐹 Fn ran (1st𝑅) → (𝑦 ∈ (𝐹 “ {𝑍}) ↔ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})))
516, 16, 503syl 18 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑦 ∈ (𝐹 “ {𝑍}) ↔ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})))
5249, 51anbi12d 633 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ (𝐹 “ {𝑍}) ∧ 𝑦 ∈ (𝐹 “ {𝑍})) ↔ ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍}))))
53 elpreima 6809 . . . . . . . 8 (𝐹 Fn ran (1st𝑅) → ((𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
546, 16, 533syl 18 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
5547, 52, 543imtr4d 297 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ (𝐹 “ {𝑍}) ∧ 𝑦 ∈ (𝐹 “ {𝑍})) → (𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍})))
5655impl 459 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) ∧ 𝑦 ∈ (𝐹 “ {𝑍})) → (𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}))
5756ralrimiva 3176 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) → ∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}))
5834anbi2i 625 . . . . . . 7 ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ↔ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍))
59 eqid 2824 . . . . . . . . . . . . . . . 16 (2nd𝑅) = (2nd𝑅)
602, 59, 3rngocl 35239 . . . . . . . . . . . . . . 15 ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
61603expb 1117 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅))) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
62613ad2antl1 1182 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅))) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
6362anass1rs 654 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
6463adantlrr 720 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
65 eqid 2824 . . . . . . . . . . . . . . . 16 (2nd𝑆) = (2nd𝑆)
662, 3, 59, 65rngohommul 35308 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅))) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)))
6766anass1rs 654 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)))
6867adantlrr 720 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)))
69 oveq2 7146 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = 𝑍 → ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑧)(2nd𝑆)𝑍))
7069adantl 485 . . . . . . . . . . . . . 14 ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍) → ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑧)(2nd𝑆)𝑍))
7170ad2antlr 726 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑧)(2nd𝑆)𝑍))
722, 3, 4, 5rngohomcl 35305 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹𝑧) ∈ ran 𝐺)
7311, 5, 4, 65rngorz 35261 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ RingOps ∧ (𝐹𝑧) ∈ ran 𝐺) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
74733ad2antl2 1183 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹𝑧) ∈ ran 𝐺) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
7572, 74syldan 594 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
7675adantlr 714 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
7768, 71, 763eqtrd 2863 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = 𝑍)
78 fvex 6664 . . . . . . . . . . . . 13 (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ V
7978elsn 4563 . . . . . . . . . . . 12 ((𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍} ↔ (𝐹‘(𝑧(2nd𝑅)𝑥)) = 𝑍)
8077, 79sylibr 237 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})
81 elpreima 6809 . . . . . . . . . . . . 13 (𝐹 Fn ran (1st𝑅) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ↔ ((𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})))
826, 16, 813syl 18 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ↔ ((𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})))
8382ad2antrr 725 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ↔ ((𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})))
8464, 80, 83mpbir2and 712 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}))
852, 59, 3rngocl 35239 . . . . . . . . . . . . . . 15 ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
86853expb 1117 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
87863ad2antl1 1182 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
8887anassrs 471 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
8988adantlrr 720 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
902, 3, 59, 65rngohommul 35308 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)))
9190anassrs 471 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)))
9291adantlrr 720 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)))
93 oveq1 7145 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = 𝑍 → ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)) = (𝑍(2nd𝑆)(𝐹𝑧)))
9493adantl 485 . . . . . . . . . . . . . 14 ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍) → ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)) = (𝑍(2nd𝑆)(𝐹𝑧)))
9594ad2antlr 726 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)) = (𝑍(2nd𝑆)(𝐹𝑧)))
9611, 5, 4, 65rngolz 35260 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ RingOps ∧ (𝐹𝑧) ∈ ran 𝐺) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
97963ad2antl2 1183 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹𝑧) ∈ ran 𝐺) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
9872, 97syldan 594 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
9998adantlr 714 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
10092, 95, 993eqtrd 2863 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = 𝑍)
101 fvex 6664 . . . . . . . . . . . . 13 (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ V
102101elsn 4563 . . . . . . . . . . . 12 ((𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍} ↔ (𝐹‘(𝑥(2nd𝑅)𝑧)) = 𝑍)
103100, 102sylibr 237 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})
104 elpreima 6809 . . . . . . . . . . . . 13 (𝐹 Fn ran (1st𝑅) → ((𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})))
1056, 16, 1043syl 18 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})))
106105ad2antrr 725 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})))
10789, 103, 106mpbir2and 712 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))
10884, 107jca 515 . . . . . . . . 9 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍})))
109108ralrimiva 3176 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍})))
110109ex 416 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
11158, 110syl5bi 245 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
11249, 111sylbid 243 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑥 ∈ (𝐹 “ {𝑍}) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
113112imp 410 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍})))
11457, 113jca 515 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) → (∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
115114ralrimiva 3176 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ∀𝑥 ∈ (𝐹 “ {𝑍})(∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
1162, 59, 3, 8isidl 35352 . . 3 (𝑅 ∈ RingOps → ((𝐹 “ {𝑍}) ∈ (Idl‘𝑅) ↔ ((𝐹 “ {𝑍}) ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑥 ∈ (𝐹 “ {𝑍})(∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))))
1171163ad2ant1 1130 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝐹 “ {𝑍}) ∈ (Idl‘𝑅) ↔ ((𝐹 “ {𝑍}) ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑥 ∈ (𝐹 “ {𝑍})(∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))))
1187, 19, 115, 117mpbir3and 1339 1 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹 “ {𝑍}) ∈ (Idl‘𝑅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115  ∀wral 3132   ⊆ wss 3918  {csn 4548  ◡ccnv 5535  ran crn 5537   “ cima 5539   Fn wfn 6331  ⟶wf 6332  ‘cfv 6336  (class class class)co 7138  1st c1st 7670  2nd c2nd 7671  GrpOpcgr 28261  GIdcgi 28262  RingOpscrngo 35232   RngHom crnghom 35298  Idlcidl 35345 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-ral 3137  df-rex 3138  df-reu 3139  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7096  df-ov 7141  df-oprab 7142  df-mpo 7143  df-1st 7672  df-2nd 7673  df-map 8391  df-grpo 28265  df-gid 28266  df-ginv 28267  df-ablo 28317  df-ghomOLD 35222  df-rngo 35233  df-rngohom 35301  df-idl 35348 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator