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

Theorem keridl 34457
 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 5739 . . 3 (𝐹 “ {𝑍}) ⊆ dom 𝐹
2 eqid 2778 . . . 4 (1st𝑅) = (1st𝑅)
3 eqid 2778 . . . 4 ran (1st𝑅) = ran (1st𝑅)
4 keridl.1 . . . 4 𝐺 = (1st𝑆)
5 eqid 2778 . . . 4 ran 𝐺 = ran 𝐺
62, 3, 4, 5rngohomf 34391 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st𝑅)⟶ran 𝐺)
71, 6fssdm 6307 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹 “ {𝑍}) ⊆ ran (1st𝑅))
8 eqid 2778 . . . . 5 (GId‘(1st𝑅)) = (GId‘(1st𝑅))
92, 3, 8rngo0cl 34344 . . . 4 (𝑅 ∈ RingOps → (GId‘(1st𝑅)) ∈ ran (1st𝑅))
1093ad2ant1 1124 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (GId‘(1st𝑅)) ∈ ran (1st𝑅))
11 keridl.2 . . . . 5 𝑍 = (GId‘𝐺)
122, 8, 4, 11rngohom0 34397 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(1st𝑅))) = 𝑍)
13 fvex 6459 . . . . 5 (𝐹‘(GId‘(1st𝑅))) ∈ V
1413elsn 4413 . . . 4 ((𝐹‘(GId‘(1st𝑅))) ∈ {𝑍} ↔ (𝐹‘(GId‘(1st𝑅))) = 𝑍)
1512, 14sylibr 226 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(1st𝑅))) ∈ {𝑍})
16 ffn 6291 . . . 4 (𝐹:ran (1st𝑅)⟶ran 𝐺𝐹 Fn ran (1st𝑅))
17 elpreima 6600 . . . 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 703 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}))
20 an4 646 . . . . . . . 8 (((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})) ↔ ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ ((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍})))
212, 3, 4rngohomadd 34394 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)𝐺(𝐹𝑦)))
2221adantr 474 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)𝐺(𝐹𝑦)))
23 oveq12 6931 . . . . . . . . . . . . . 14 (((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍) → ((𝐹𝑥)𝐺(𝐹𝑦)) = (𝑍𝐺𝑍))
2423adantl 475 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → ((𝐹𝑥)𝐺(𝐹𝑦)) = (𝑍𝐺𝑍))
254rngogrpo 34335 . . . . . . . . . . . . . . . 16 (𝑆 ∈ RingOps → 𝐺 ∈ GrpOp)
265, 11grpoidcl 27941 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ GrpOp → 𝑍 ∈ ran 𝐺)
275, 11grpolid 27943 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ GrpOp ∧ 𝑍 ∈ ran 𝐺) → (𝑍𝐺𝑍) = 𝑍)
2826, 27mpdan 677 . . . . . . . . . . . . . . . 16 (𝐺 ∈ GrpOp → (𝑍𝐺𝑍) = 𝑍)
2925, 28syl 17 . . . . . . . . . . . . . . 15 (𝑆 ∈ RingOps → (𝑍𝐺𝑍) = 𝑍)
30293ad2ant2 1125 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑍𝐺𝑍) = 𝑍)
3130ad2antrr 716 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → (𝑍𝐺𝑍) = 𝑍)
3222, 24, 313eqtrd 2818 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = 𝑍)
3332ex 403 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍) → (𝐹‘(𝑥(1st𝑅)𝑦)) = 𝑍))
34 fvex 6459 . . . . . . . . . . . . 13 (𝐹𝑥) ∈ V
3534elsn 4413 . . . . . . . . . . . 12 ((𝐹𝑥) ∈ {𝑍} ↔ (𝐹𝑥) = 𝑍)
36 fvex 6459 . . . . . . . . . . . . 13 (𝐹𝑦) ∈ V
3736elsn 4413 . . . . . . . . . . . 12 ((𝐹𝑦) ∈ {𝑍} ↔ (𝐹𝑦) = 𝑍)
3835, 37anbi12i 620 . . . . . . . . . . 11 (((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍}) ↔ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍))
39 fvex 6459 . . . . . . . . . . . 12 (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ V
4039elsn 4413 . . . . . . . . . . 11 ((𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍} ↔ (𝐹‘(𝑥(1st𝑅)𝑦)) = 𝑍)
4133, 38, 403imtr4g 288 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍}) → (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍}))
4241imdistanda 567 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ ((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍})) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
432, 3rngogcl 34337 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
44433expib 1113 . . . . . . . . . . 11 (𝑅 ∈ RingOps → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅)))
45443ad2ant1 1124 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅)))
4645anim1d 604 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍}) → ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
4742, 46syld 47 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ ((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍})) → ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
4820, 47syl5bi 234 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})) → ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
49 elpreima 6600 . . . . . . . . 9 (𝐹 Fn ran (1st𝑅) → (𝑥 ∈ (𝐹 “ {𝑍}) ↔ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍})))
506, 16, 493syl 18 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑥 ∈ (𝐹 “ {𝑍}) ↔ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍})))
51 elpreima 6600 . . . . . . . . 9 (𝐹 Fn ran (1st𝑅) → (𝑦 ∈ (𝐹 “ {𝑍}) ↔ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})))
526, 16, 513syl 18 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑦 ∈ (𝐹 “ {𝑍}) ↔ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})))
5350, 52anbi12d 624 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ (𝐹 “ {𝑍}) ∧ 𝑦 ∈ (𝐹 “ {𝑍})) ↔ ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍}))))
54 elpreima 6600 . . . . . . . 8 (𝐹 Fn ran (1st𝑅) → ((𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
556, 16, 543syl 18 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
5648, 53, 553imtr4d 286 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ (𝐹 “ {𝑍}) ∧ 𝑦 ∈ (𝐹 “ {𝑍})) → (𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍})))
5756impl 449 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) ∧ 𝑦 ∈ (𝐹 “ {𝑍})) → (𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}))
5857ralrimiva 3148 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) → ∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}))
5935anbi2i 616 . . . . . . 7 ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ↔ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍))
60 eqid 2778 . . . . . . . . . . . . . . . 16 (2nd𝑅) = (2nd𝑅)
612, 60, 3rngocl 34326 . . . . . . . . . . . . . . 15 ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
62613expb 1110 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅))) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
63623ad2antl1 1193 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅))) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
6463anass1rs 645 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
6564adantlrr 711 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
66 eqid 2778 . . . . . . . . . . . . . . . 16 (2nd𝑆) = (2nd𝑆)
672, 3, 60, 66rngohommul 34395 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅))) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)))
6867anass1rs 645 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)))
6968adantlrr 711 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)))
70 oveq2 6930 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = 𝑍 → ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑧)(2nd𝑆)𝑍))
7170adantl 475 . . . . . . . . . . . . . 14 ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍) → ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑧)(2nd𝑆)𝑍))
7271ad2antlr 717 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑧)(2nd𝑆)𝑍))
732, 3, 4, 5rngohomcl 34392 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹𝑧) ∈ ran 𝐺)
7411, 5, 4, 66rngorz 34348 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ RingOps ∧ (𝐹𝑧) ∈ ran 𝐺) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
75743ad2antl2 1194 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹𝑧) ∈ ran 𝐺) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
7673, 75syldan 585 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
7776adantlr 705 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
7869, 72, 773eqtrd 2818 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = 𝑍)
79 fvex 6459 . . . . . . . . . . . . 13 (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ V
8079elsn 4413 . . . . . . . . . . . 12 ((𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍} ↔ (𝐹‘(𝑧(2nd𝑅)𝑥)) = 𝑍)
8178, 80sylibr 226 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})
82 elpreima 6600 . . . . . . . . . . . . 13 (𝐹 Fn ran (1st𝑅) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ↔ ((𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})))
836, 16, 823syl 18 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ↔ ((𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})))
8483ad2antrr 716 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ↔ ((𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})))
8565, 81, 84mpbir2and 703 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}))
862, 60, 3rngocl 34326 . . . . . . . . . . . . . . 15 ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
87863expb 1110 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
88873ad2antl1 1193 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
8988anassrs 461 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
9089adantlrr 711 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
912, 3, 60, 66rngohommul 34395 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)))
9291anassrs 461 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)))
9392adantlrr 711 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)))
94 oveq1 6929 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = 𝑍 → ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)) = (𝑍(2nd𝑆)(𝐹𝑧)))
9594adantl 475 . . . . . . . . . . . . . 14 ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍) → ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)) = (𝑍(2nd𝑆)(𝐹𝑧)))
9695ad2antlr 717 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)) = (𝑍(2nd𝑆)(𝐹𝑧)))
9711, 5, 4, 66rngolz 34347 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ RingOps ∧ (𝐹𝑧) ∈ ran 𝐺) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
98973ad2antl2 1194 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹𝑧) ∈ ran 𝐺) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
9973, 98syldan 585 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
10099adantlr 705 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
10193, 96, 1003eqtrd 2818 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = 𝑍)
102 fvex 6459 . . . . . . . . . . . . 13 (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ V
103102elsn 4413 . . . . . . . . . . . 12 ((𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍} ↔ (𝐹‘(𝑥(2nd𝑅)𝑧)) = 𝑍)
104101, 103sylibr 226 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})
105 elpreima 6600 . . . . . . . . . . . . 13 (𝐹 Fn ran (1st𝑅) → ((𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})))
1066, 16, 1053syl 18 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})))
107106ad2antrr 716 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})))
10890, 104, 107mpbir2and 703 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))
10985, 108jca 507 . . . . . . . . 9 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍})))
110109ralrimiva 3148 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍})))
111110ex 403 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
11259, 111syl5bi 234 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
11350, 112sylbid 232 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑥 ∈ (𝐹 “ {𝑍}) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
114113imp 397 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍})))
11558, 114jca 507 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) → (∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
116115ralrimiva 3148 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ∀𝑥 ∈ (𝐹 “ {𝑍})(∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
1172, 60, 3, 8isidl 34439 . . 3 (𝑅 ∈ RingOps → ((𝐹 “ {𝑍}) ∈ (Idl‘𝑅) ↔ ((𝐹 “ {𝑍}) ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑥 ∈ (𝐹 “ {𝑍})(∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))))
1181173ad2ant1 1124 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝐹 “ {𝑍}) ∈ (Idl‘𝑅) ↔ ((𝐹 “ {𝑍}) ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑥 ∈ (𝐹 “ {𝑍})(∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))))
1197, 19, 116, 118mpbir3and 1399 1 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹 “ {𝑍}) ∈ (Idl‘𝑅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107  ∀wral 3090   ⊆ wss 3792  {csn 4398  ◡ccnv 5354  ran crn 5356   “ cima 5358   Fn wfn 6130  ⟶wf 6131  ‘cfv 6135  (class class class)co 6922  1st c1st 7443  2nd c2nd 7444  GrpOpcgr 27916  GIdcgi 27917  RingOpscrngo 34319   RngHom crnghom 34385  Idlcidl 34432 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-1st 7445  df-2nd 7446  df-map 8142  df-grpo 27920  df-gid 27921  df-ginv 27922  df-ablo 27972  df-ghomOLD 34309  df-rngo 34320  df-rngohom 34388  df-idl 34435 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator