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 36888
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 6077 . . 3 (𝐹 “ {𝑍}) ⊆ dom 𝐹
2 eqid 2732 . . . 4 (1st𝑅) = (1st𝑅)
3 eqid 2732 . . . 4 ran (1st𝑅) = ran (1st𝑅)
4 keridl.1 . . . 4 𝐺 = (1st𝑆)
5 eqid 2732 . . . 4 ran 𝐺 = ran 𝐺
62, 3, 4, 5rngohomf 36822 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → 𝐹:ran (1st𝑅)⟶ran 𝐺)
71, 6fssdm 6734 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹 “ {𝑍}) ⊆ ran (1st𝑅))
8 eqid 2732 . . . . 5 (GId‘(1st𝑅)) = (GId‘(1st𝑅))
92, 3, 8rngo0cl 36775 . . . 4 (𝑅 ∈ RingOps → (GId‘(1st𝑅)) ∈ ran (1st𝑅))
1093ad2ant1 1133 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (GId‘(1st𝑅)) ∈ ran (1st𝑅))
11 keridl.2 . . . . 5 𝑍 = (GId‘𝐺)
122, 8, 4, 11rngohom0 36828 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(1st𝑅))) = 𝑍)
13 fvex 6901 . . . . 5 (𝐹‘(GId‘(1st𝑅))) ∈ V
1413elsn 4642 . . . 4 ((𝐹‘(GId‘(1st𝑅))) ∈ {𝑍} ↔ (𝐹‘(GId‘(1st𝑅))) = 𝑍)
1512, 14sylibr 233 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(1st𝑅))) ∈ {𝑍})
16 ffn 6714 . . . 4 (𝐹:ran (1st𝑅)⟶ran 𝐺𝐹 Fn ran (1st𝑅))
17 elpreima 7056 . . . 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 711 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}))
20 an4 654 . . . . . . . 8 (((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})) ↔ ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ ((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍})))
212, 3, 4rngohomadd 36825 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)𝐺(𝐹𝑦)))
2221adantr 481 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = ((𝐹𝑥)𝐺(𝐹𝑦)))
23 oveq12 7414 . . . . . . . . . . . . . 14 (((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍) → ((𝐹𝑥)𝐺(𝐹𝑦)) = (𝑍𝐺𝑍))
2423adantl 482 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → ((𝐹𝑥)𝐺(𝐹𝑦)) = (𝑍𝐺𝑍))
254rngogrpo 36766 . . . . . . . . . . . . . . . 16 (𝑆 ∈ RingOps → 𝐺 ∈ GrpOp)
265, 11grpoidcl 29754 . . . . . . . . . . . . . . . 16 (𝐺 ∈ GrpOp → 𝑍 ∈ ran 𝐺)
275, 11grpolid 29756 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ GrpOp ∧ 𝑍 ∈ ran 𝐺) → (𝑍𝐺𝑍) = 𝑍)
2825, 26, 27syl2anc2 585 . . . . . . . . . . . . . . 15 (𝑆 ∈ RingOps → (𝑍𝐺𝑍) = 𝑍)
29283ad2ant2 1134 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑍𝐺𝑍) = 𝑍)
3029ad2antrr 724 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → (𝑍𝐺𝑍) = 𝑍)
3122, 24, 303eqtrd 2776 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) ∧ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍)) → (𝐹‘(𝑥(1st𝑅)𝑦)) = 𝑍)
3231ex 413 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍) → (𝐹‘(𝑥(1st𝑅)𝑦)) = 𝑍))
33 fvex 6901 . . . . . . . . . . . . 13 (𝐹𝑥) ∈ V
3433elsn 4642 . . . . . . . . . . . 12 ((𝐹𝑥) ∈ {𝑍} ↔ (𝐹𝑥) = 𝑍)
35 fvex 6901 . . . . . . . . . . . . 13 (𝐹𝑦) ∈ V
3635elsn 4642 . . . . . . . . . . . 12 ((𝐹𝑦) ∈ {𝑍} ↔ (𝐹𝑦) = 𝑍)
3734, 36anbi12i 627 . . . . . . . . . . 11 (((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍}) ↔ ((𝐹𝑥) = 𝑍 ∧ (𝐹𝑦) = 𝑍))
38 fvex 6901 . . . . . . . . . . . 12 (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ V
3938elsn 4642 . . . . . . . . . . 11 ((𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍} ↔ (𝐹‘(𝑥(1st𝑅)𝑦)) = 𝑍)
4032, 37, 393imtr4g 295 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅))) → (((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍}) → (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍}))
4140imdistanda 572 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ ((𝐹𝑥) ∈ {𝑍} ∧ (𝐹𝑦) ∈ {𝑍})) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
422, 3rngogcl 36768 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅))
43423expib 1122 . . . . . . . . . . 11 (𝑅 ∈ RingOps → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅)))
44433ad2ant1 1133 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ 𝑦 ∈ ran (1st𝑅)) → (𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅)))
4544anim1d 611 . . . . . . . . 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, 46biimtrid 241 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})) → ((𝑥(1st𝑅)𝑦) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(1st𝑅)𝑦)) ∈ {𝑍})))
48 elpreima 7056 . . . . . . . . 9 (𝐹 Fn ran (1st𝑅) → (𝑥 ∈ (𝐹 “ {𝑍}) ↔ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍})))
496, 16, 483syl 18 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑥 ∈ (𝐹 “ {𝑍}) ↔ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍})))
50 elpreima 7056 . . . . . . . . 9 (𝐹 Fn ran (1st𝑅) → (𝑦 ∈ (𝐹 “ {𝑍}) ↔ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})))
516, 16, 503syl 18 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑦 ∈ (𝐹 “ {𝑍}) ↔ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍})))
5249, 51anbi12d 631 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ (𝐹 “ {𝑍}) ∧ 𝑦 ∈ (𝐹 “ {𝑍})) ↔ ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ∧ (𝑦 ∈ ran (1st𝑅) ∧ (𝐹𝑦) ∈ {𝑍}))))
53 elpreima 7056 . . . . . . . 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 293 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ (𝐹 “ {𝑍}) ∧ 𝑦 ∈ (𝐹 “ {𝑍})) → (𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍})))
5655impl 456 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) ∧ 𝑦 ∈ (𝐹 “ {𝑍})) → (𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}))
5756ralrimiva 3146 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) → ∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}))
5834anbi2i 623 . . . . . . 7 ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) ↔ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍))
59 eqid 2732 . . . . . . . . . . . . . . . 16 (2nd𝑅) = (2nd𝑅)
602, 59, 3rngocl 36757 . . . . . . . . . . . . . . 15 ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
61603expb 1120 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅))) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
62613ad2antl1 1185 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅))) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
6362anass1rs 653 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
6463adantlrr 719 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅))
65 eqid 2732 . . . . . . . . . . . . . . . 16 (2nd𝑆) = (2nd𝑆)
662, 3, 59, 65rngohommul 36826 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑥 ∈ ran (1st𝑅))) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)))
6766anass1rs 653 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)))
6867adantlrr 719 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)))
69 oveq2 7413 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = 𝑍 → ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑧)(2nd𝑆)𝑍))
7069adantl 482 . . . . . . . . . . . . . 14 ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍) → ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑧)(2nd𝑆)𝑍))
7170ad2antlr 725 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑧)(2nd𝑆)(𝐹𝑥)) = ((𝐹𝑧)(2nd𝑆)𝑍))
722, 3, 4, 5rngohomcl 36823 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹𝑧) ∈ ran 𝐺)
7311, 5, 4, 65rngorz 36779 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ RingOps ∧ (𝐹𝑧) ∈ ran 𝐺) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
74733ad2antl2 1186 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹𝑧) ∈ ran 𝐺) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
7572, 74syldan 591 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
7675adantlr 713 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑧)(2nd𝑆)𝑍) = 𝑍)
7768, 71, 763eqtrd 2776 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) = 𝑍)
78 fvex 6901 . . . . . . . . . . . . 13 (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ V
7978elsn 4642 . . . . . . . . . . . 12 ((𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍} ↔ (𝐹‘(𝑧(2nd𝑅)𝑥)) = 𝑍)
8077, 79sylibr 233 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})
81 elpreima 7056 . . . . . . . . . . . . 13 (𝐹 Fn ran (1st𝑅) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ↔ ((𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})))
826, 16, 813syl 18 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ↔ ((𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})))
8382ad2antrr 724 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ↔ ((𝑧(2nd𝑅)𝑥) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑧(2nd𝑅)𝑥)) ∈ {𝑍})))
8464, 80, 83mpbir2and 711 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}))
852, 59, 3rngocl 36757 . . . . . . . . . . . . . . 15 ((𝑅 ∈ RingOps ∧ 𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
86853expb 1120 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
87863ad2antl1 1185 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
8887anassrs 468 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
8988adantlrr 719 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅))
902, 3, 59, 65rngohommul 36826 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ 𝑧 ∈ ran (1st𝑅))) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)))
9190anassrs 468 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ ran (1st𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)))
9291adantlrr 719 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)))
93 oveq1 7412 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = 𝑍 → ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)) = (𝑍(2nd𝑆)(𝐹𝑧)))
9493adantl 482 . . . . . . . . . . . . . 14 ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍) → ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)) = (𝑍(2nd𝑆)(𝐹𝑧)))
9594ad2antlr 725 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝐹𝑥)(2nd𝑆)(𝐹𝑧)) = (𝑍(2nd𝑆)(𝐹𝑧)))
9611, 5, 4, 65rngolz 36778 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ RingOps ∧ (𝐹𝑧) ∈ ran 𝐺) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
97963ad2antl2 1186 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹𝑧) ∈ ran 𝐺) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
9872, 97syldan 591 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
9998adantlr 713 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑍(2nd𝑆)(𝐹𝑧)) = 𝑍)
10092, 95, 993eqtrd 2776 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) = 𝑍)
101 fvex 6901 . . . . . . . . . . . . 13 (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ V
102101elsn 4642 . . . . . . . . . . . 12 ((𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍} ↔ (𝐹‘(𝑥(2nd𝑅)𝑧)) = 𝑍)
103100, 102sylibr 233 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})
104 elpreima 7056 . . . . . . . . . . . . 13 (𝐹 Fn ran (1st𝑅) → ((𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})))
1056, 16, 1043syl 18 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})))
106105ad2antrr 724 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}) ↔ ((𝑥(2nd𝑅)𝑧) ∈ ran (1st𝑅) ∧ (𝐹‘(𝑥(2nd𝑅)𝑧)) ∈ {𝑍})))
10789, 103, 106mpbir2and 711 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))
10884, 107jca 512 . . . . . . . . 9 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍})))
109108ralrimiva 3146 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍})))
110109ex 413 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) = 𝑍) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
11158, 110biimtrid 241 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝑥 ∈ ran (1st𝑅) ∧ (𝐹𝑥) ∈ {𝑍}) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
11249, 111sylbid 239 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝑥 ∈ (𝐹 “ {𝑍}) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
113112imp 407 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍})))
11457, 113jca 512 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑥 ∈ (𝐹 “ {𝑍})) → (∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
115114ralrimiva 3146 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ∀𝑥 ∈ (𝐹 “ {𝑍})(∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))
1162, 59, 3, 8isidl 36870 . . 3 (𝑅 ∈ RingOps → ((𝐹 “ {𝑍}) ∈ (Idl‘𝑅) ↔ ((𝐹 “ {𝑍}) ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑥 ∈ (𝐹 “ {𝑍})(∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))))
1171163ad2ant1 1133 . 2 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → ((𝐹 “ {𝑍}) ∈ (Idl‘𝑅) ↔ ((𝐹 “ {𝑍}) ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑥 ∈ (𝐹 “ {𝑍})(∀𝑦 ∈ (𝐹 “ {𝑍})(𝑥(1st𝑅)𝑦) ∈ (𝐹 “ {𝑍}) ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ (𝐹 “ {𝑍}) ∧ (𝑥(2nd𝑅)𝑧) ∈ (𝐹 “ {𝑍}))))))
1187, 19, 115, 117mpbir3and 1342 1 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹 “ {𝑍}) ∈ (Idl‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3061  wss 3947  {csn 4627  ccnv 5674  ran crn 5676  cima 5678   Fn wfn 6535  wf 6536  cfv 6540  (class class class)co 7405  1st c1st 7969  2nd c2nd 7970  GrpOpcgr 29729  GIdcgi 29730  RingOpscrngo 36750   RngHom crnghom 36816  Idlcidl 36863
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-map 8818  df-grpo 29733  df-gid 29734  df-ginv 29735  df-ablo 29785  df-ghomOLD 36740  df-rngo 36751  df-rngohom 36819  df-idl 36866
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator