Users' Mathboxes 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