chrrhm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > chrrhm		Structured version Visualization version GIF version

Theorem chrrhm 20100

Description: The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.)

**Assertion**
Ref	Expression
chrrhm	⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (chr‘𝑆) ∥ (chr‘𝑅))

**Proof of Theorem chrrhm**
Step	Hyp	Ref	Expression
1		rhmrcl1 18935	. . . . . . 7 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring)
2		eqid 2769	. . . . . . . 8 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
3	2	zrhrhm 20081	. . . . . . 7 ⊢ (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤ_ring RingHom 𝑅))
4	1, 3	syl 17	. . . . . 6 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (ℤRHom‘𝑅) ∈ (ℤ_ring RingHom 𝑅))
5		zringbas 20045	. . . . . . 7 ⊢ ℤ = (Base‘ℤ_ring)
6		eqid 2769	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘𝑅)
7	5, 6	rhmf 18942	. . . . . 6 ⊢ ((ℤRHom‘𝑅) ∈ (ℤ_ring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶(Base‘𝑅))
8		ffn 6184	. . . . . 6 ⊢ ((ℤRHom‘𝑅):ℤ⟶(Base‘𝑅) → (ℤRHom‘𝑅) Fn ℤ)
9	4, 7, 8	3syl 18	. . . . 5 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (ℤRHom‘𝑅) Fn ℤ)
10		eqid 2769	. . . . . . 7 ⊢ (chr‘𝑅) = (chr‘𝑅)
11	10	chrcl 20095	. . . . . 6 ⊢ (𝑅 ∈ Ring → (chr‘𝑅) ∈ ℕ₀)
12		nn0z 11600	. . . . . 6 ⊢ ((chr‘𝑅) ∈ ℕ₀ → (chr‘𝑅) ∈ ℤ)
13	1, 11, 12	3syl 18	. . . . 5 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (chr‘𝑅) ∈ ℤ)
14		fvco2 6414	. . . . 5 ⊢ (((ℤRHom‘𝑅) Fn ℤ ∧ (chr‘𝑅) ∈ ℤ) → ((𝐹 ∘ (ℤRHom‘𝑅))‘(chr‘𝑅)) = (𝐹‘((ℤRHom‘𝑅)‘(chr‘𝑅))))
15	9, 13, 14	syl2anc 693	. . . 4 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((𝐹 ∘ (ℤRHom‘𝑅))‘(chr‘𝑅)) = (𝐹‘((ℤRHom‘𝑅)‘(chr‘𝑅))))
16		eqid 2769	. . . . . . 7 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
17	10, 2, 16	chrid 20096	. . . . . 6 ⊢ (𝑅 ∈ Ring → ((ℤRHom‘𝑅)‘(chr‘𝑅)) = (0_g‘𝑅))
18	1, 17	syl 17	. . . . 5 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((ℤRHom‘𝑅)‘(chr‘𝑅)) = (0_g‘𝑅))
19	18	fveq2d 6335	. . . 4 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘((ℤRHom‘𝑅)‘(chr‘𝑅))) = (𝐹‘(0_g‘𝑅)))
20	15, 19	eqtrd 2803	. . 3 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((𝐹 ∘ (ℤRHom‘𝑅))‘(chr‘𝑅)) = (𝐹‘(0_g‘𝑅)))
21		rhmco 18953	. . . . . 6 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (ℤRHom‘𝑅) ∈ (ℤ_ring RingHom 𝑅)) → (𝐹 ∘ (ℤRHom‘𝑅)) ∈ (ℤ_ring RingHom 𝑆))
22	4, 21	mpdan 702	. . . . 5 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 ∘ (ℤRHom‘𝑅)) ∈ (ℤ_ring RingHom 𝑆))
23		rhmrcl2 18936	. . . . . 6 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring)
24		eqid 2769	. . . . . . 7 ⊢ (ℤRHom‘𝑆) = (ℤRHom‘𝑆)
25	24	zrhrhmb 20080	. . . . . 6 ⊢ (𝑆 ∈ Ring → ((𝐹 ∘ (ℤRHom‘𝑅)) ∈ (ℤ_ring RingHom 𝑆) ↔ (𝐹 ∘ (ℤRHom‘𝑅)) = (ℤRHom‘𝑆)))
26	23, 25	syl 17	. . . . 5 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((𝐹 ∘ (ℤRHom‘𝑅)) ∈ (ℤ_ring RingHom 𝑆) ↔ (𝐹 ∘ (ℤRHom‘𝑅)) = (ℤRHom‘𝑆)))
27	22, 26	mpbid 222	. . . 4 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 ∘ (ℤRHom‘𝑅)) = (ℤRHom‘𝑆))
28	27	fveq1d 6333	. . 3 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((𝐹 ∘ (ℤRHom‘𝑅))‘(chr‘𝑅)) = ((ℤRHom‘𝑆)‘(chr‘𝑅)))
29		rhmghm 18941	. . . 4 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
30		eqid 2769	. . . . 5 ⊢ (0_g‘𝑆) = (0_g‘𝑆)
31	16, 30	ghmid 17880	. . . 4 ⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹‘(0_g‘𝑅)) = (0_g‘𝑆))
32	29, 31	syl 17	. . 3 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(0_g‘𝑅)) = (0_g‘𝑆))
33	20, 28, 32	3eqtr3d 2811	. 2 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((ℤRHom‘𝑆)‘(chr‘𝑅)) = (0_g‘𝑆))
34		eqid 2769	. . . 4 ⊢ (chr‘𝑆) = (chr‘𝑆)
35	34, 24, 30	chrdvds 20097	. . 3 ⊢ ((𝑆 ∈ Ring ∧ (chr‘𝑅) ∈ ℤ) → ((chr‘𝑆) ∥ (chr‘𝑅) ↔ ((ℤRHom‘𝑆)‘(chr‘𝑅)) = (0_g‘𝑆)))
36	23, 13, 35	syl2anc 693	. 2 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → ((chr‘𝑆) ∥ (chr‘𝑅) ↔ ((ℤRHom‘𝑆)‘(chr‘𝑅)) = (0_g‘𝑆)))
37	33, 36	mpbird 247	1 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (chr‘𝑆) ∥ (chr‘𝑅))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 = wceq 1629 ∈ wcel 2143 class class class wbr 4783 ∘ ccom 5252 Fn wfn 6025 ⟶wf 6026 ‘cfv 6030 (class class class)co 6791 ℕ₀cn0 11492 ℤcz 11577 ∥ cdvds 15194 Basecbs 16070 0_gc0g 16314 GrpHom cghm 17871 Ringcrg 18761 RingHom crh 18928 ℤ_ringzring 20039 ℤRHomczrh 20069 chrcchr 20071

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1868 ax-4 1883 ax-5 1989 ax-6 2055 ax-7 2091 ax-8 2145 ax-9 2152 ax-10 2172 ax-11 2188 ax-12 2201 ax-13 2406 ax-ext 2749 ax-rep 4901 ax-sep 4911 ax-nul 4919 ax-pow 4970 ax-pr 5033 ax-un 7094 ax-inf2 8700 ax-cnex 10192 ax-resscn 10193 ax-1cn 10194 ax-icn 10195 ax-addcl 10196 ax-addrcl 10197 ax-mulcl 10198 ax-mulrcl 10199 ax-mulcom 10200 ax-addass 10201 ax-mulass 10202 ax-distr 10203 ax-i2m1 10204 ax-1ne0 10205 ax-1rid 10206 ax-rnegex 10207 ax-rrecex 10208 ax-cnre 10209 ax-pre-lttri 10210 ax-pre-lttrn 10211 ax-pre-ltadd 10212 ax-pre-mulgt0 10213 ax-pre-sup 10214 ax-addf 10215 ax-mulf 10216

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1070 df-3an 1071 df-tru 1632 df-ex 1851 df-nf 1856 df-sb 2048 df-eu 2620 df-mo 2621 df-clab 2756 df-cleq 2762 df-clel 2765 df-nfc 2900 df-ne 2942 df-nel 3045 df-ral 3064 df-rex 3065 df-reu 3066 df-rmo 3067 df-rab 3068 df-v 3350 df-sbc 3585 df-csb 3680 df-dif 3723 df-un 3725 df-in 3727 df-ss 3734 df-pss 3736 df-nul 4061 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-tp 4318 df-op 4320 df-uni 4572 df-int 4609 df-iun 4653 df-br 4784 df-opab 4844 df-mpt 4861 df-tr 4884 df-id 5156 df-eprel 5161 df-po 5169 df-so 5170 df-fr 5207 df-we 5209 df-xp 5254 df-rel 5255 df-cnv 5256 df-co 5257 df-dm 5258 df-rn 5259 df-res 5260 df-ima 5261 df-pred 5822 df-ord 5868 df-on 5869 df-lim 5870 df-suc 5871 df-iota 5993 df-fun 6032 df-fn 6033 df-f 6034 df-f1 6035 df-fo 6036 df-f1o 6037 df-fv 6038 df-riota 6752 df-ov 6794 df-oprab 6795 df-mpt2 6796 df-om 7211 df-1st 7313 df-2nd 7314 df-wrecs 7557 df-recs 7619 df-rdg 7657 df-1o 7711 df-oadd 7715 df-er 7894 df-map 8009 df-en 8108 df-dom 8109 df-sdom 8110 df-fin 8111 df-sup 8502 df-inf 8503 df-pnf 10276 df-mnf 10277 df-xr 10278 df-ltxr 10279 df-le 10280 df-sub 10468 df-neg 10469 df-div 10885 df-nn 11221 df-2 11279 df-3 11280 df-4 11281 df-5 11282 df-6 11283 df-7 11284 df-8 11285 df-9 11286 df-n0 11493 df-z 11578 df-dec 11694 df-uz 11888 df-rp 12035 df-fz 12533 df-fl 12800 df-mod 12876 df-seq 13009 df-exp 13068 df-cj 14050 df-re 14051 df-im 14052 df-sqrt 14186 df-abs 14187 df-dvds 15195 df-struct 16072 df-ndx 16073 df-slot 16074 df-base 16076 df-sets 16077 df-ress 16078 df-plusg 16168 df-mulr 16169 df-starv 16170 df-tset 16174 df-ple 16175 df-ds 16178 df-unif 16179 df-0g 16316 df-mgm 17456 df-sgrp 17498 df-mnd 17509 df-mhm 17549 df-grp 17639 df-minusg 17640 df-sbg 17641 df-mulg 17755 df-subg 17805 df-ghm 17872 df-od 18161 df-cmn 18408 df-mgp 18704 df-ur 18716 df-ring 18763 df-cring 18764 df-rnghom 18931 df-subrg 18994 df-cnfld 19968 df-zring 20040 df-zrh 20073 df-chr 20075

This theorem is referenced by: (None)

W3C validator