kerunit

Description: If a unit element lies in the kernel of a ring homomorphism, then 0 = 1 , i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017)

	Ref	Expression
Hypotheses	kerunit.1	$⊢ U = Unit (R)$
	kerunit.2	$⊢ \underset{˙}{0} = 0_{S}$
	kerunit.3	$⊢ \underset{˙}{1} = 1_{S}$
Assertion	kerunit	$⊢ (F \in (R RingHom S) \land U \cap F^{-1} [\{\underset{˙}{0}\}] \neq \emptyset) \to \underset{˙}{1} = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		kerunit.1	$⊢ U = Unit (R)$
2		kerunit.2	$⊢ \underset{˙}{0} = 0_{S}$
3		kerunit.3	$⊢ \underset{˙}{1} = 1_{S}$
4		elin	$⊢ x \in (U \cap F^{-1} [\{\underset{˙}{0}\}]) \leftrightarrow (x \in U \land x \in F^{-1} [\{\underset{˙}{0}\}])$
5	4	bilani	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to (x \in U \land x \in F^{-1} [\{\underset{˙}{0}\}])$
6	5	simpld	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to x \in U$
7		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
8		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
9		eqid	$⊢ \cdot_{R} = \cdot_{R}$
10		eqid	$⊢ 1_{R} = 1_{R}$
11	1 8 9 10	unitlinv	$⊢ (R \in Ring \land x \in U) \to {inv}_{r} (R) (x) \cdot_{R} x = 1_{R}$
12	11	fveq2d	$⊢ (R \in Ring \land x \in U) \to F ({inv}_{r} (R) (x) \cdot_{R} x) = F (1_{R})$
13	7 12	sylan	$⊢ (F \in (R RingHom S) \land x \in U) \to F ({inv}_{r} (R) (x) \cdot_{R} x) = F (1_{R})$
14	6 13	syldan	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F ({inv}_{r} (R) (x) \cdot_{R} x) = F (1_{R})$
15		simpl	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F \in (R RingHom S)$
16	7	adantr	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to R \in Ring$
17		eqid	$⊢ {Base}_{R} = {Base}_{R}$
18	1 8 17	ringinvcl	$⊢ (R \in Ring \land x \in U) \to {inv}_{r} (R) (x) \in {Base}_{R}$
19	16 6 18	syl2anc	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to {inv}_{r} (R) (x) \in {Base}_{R}$
20	17 1	unitcl	$⊢ x \in U \to x \in {Base}_{R}$
21	6 20	syl	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to x \in {Base}_{R}$
22		eqid	$⊢ \cdot_{S} = \cdot_{S}$
23	17 9 22	rhmmul	$⊢ (F \in (R RingHom S) \land {inv}_{r} (R) (x) \in {Base}_{R} \land x \in {Base}_{R}) \to F ({inv}_{r} (R) (x) \cdot_{R} x) = F ({inv}_{r} (R) (x)) \cdot_{S} F (x)$
24	15 19 21 23	syl3anc	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F ({inv}_{r} (R) (x) \cdot_{R} x) = F ({inv}_{r} (R) (x)) \cdot_{S} F (x)$
25	5	simprd	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to x \in F^{-1} [\{\underset{˙}{0}\}]$
26		eqid	$⊢ {Base}_{S} = {Base}_{S}$
27	17 26	rhmf	$⊢ F \in (R RingHom S) \to F : {Base}_{R} ⟶ {Base}_{S}$
28		ffn	$⊢ F : {Base}_{R} ⟶ {Base}_{S} \to F Fn {Base}_{R}$
29		elpreima	$⊢ F Fn {Base}_{R} \to (x \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (x \in {Base}_{R} \land F (x) \in \{\underset{˙}{0}\}))$
30	27 28 29	3syl	$⊢ F \in (R RingHom S) \to (x \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (x \in {Base}_{R} \land F (x) \in \{\underset{˙}{0}\}))$
31	30	simplbda	$⊢ (F \in (R RingHom S) \land x \in F^{-1} [\{\underset{˙}{0}\}]) \to F (x) \in \{\underset{˙}{0}\}$
32	25 31	syldan	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F (x) \in \{\underset{˙}{0}\}$
33		fvex	$⊢ F (x) \in V$
34	33	elsn	$⊢ F (x) \in \{\underset{˙}{0}\} \leftrightarrow F (x) = \underset{˙}{0}$
35	32 34	sylib	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F (x) = \underset{˙}{0}$
36	35	oveq2d	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F ({inv}_{r} (R) (x)) \cdot_{S} F (x) = F ({inv}_{r} (R) (x)) \cdot_{S} \underset{˙}{0}$
37		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
38	37	adantr	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to S \in Ring$
39	27	adantr	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F : {Base}_{R} ⟶ {Base}_{S}$
40	39 19	ffvelcdmd	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F ({inv}_{r} (R) (x)) \in {Base}_{S}$
41	26 22 2	ringrz	$⊢ (S \in Ring \land F ({inv}_{r} (R) (x)) \in {Base}_{S}) \to F ({inv}_{r} (R) (x)) \cdot_{S} \underset{˙}{0} = \underset{˙}{0}$
42	38 40 41	syl2anc	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F ({inv}_{r} (R) (x)) \cdot_{S} \underset{˙}{0} = \underset{˙}{0}$
43	24 36 42	3eqtrd	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F ({inv}_{r} (R) (x) \cdot_{R} x) = \underset{˙}{0}$
44	10 3	rhm1	$⊢ F \in (R RingHom S) \to F (1_{R}) = \underset{˙}{1}$
45	44	adantr	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to F (1_{R}) = \underset{˙}{1}$
46	14 43 45	3eqtr3rd	$⊢ (F \in (R RingHom S) \land x \in (U \cap F^{-1} [\{\underset{˙}{0}\}])) \to \underset{˙}{1} = \underset{˙}{0}$
47	46	reximdva0	$⊢ (F \in (R RingHom S) \land U \cap F^{-1} [\{\underset{˙}{0}\}] \neq \emptyset) \to \exists x \in (U \cap F^{-1} [\{\underset{˙}{0}\}]) \underset{˙}{1} = \underset{˙}{0}$
48		id	$⊢ \underset{˙}{1} = \underset{˙}{0} \to \underset{˙}{1} = \underset{˙}{0}$
49	48	rexlimivw	$⊢ \exists x \in (U \cap F^{-1} [\{\underset{˙}{0}\}]) \underset{˙}{1} = \underset{˙}{0} \to \underset{˙}{1} = \underset{˙}{0}$
50	47 49	syl	$⊢ (F \in (R RingHom S) \land U \cap F^{-1} [\{\underset{˙}{0}\}] \neq \emptyset) \to \underset{˙}{1} = \underset{˙}{0}$

Metamath Proof Explorer

Theorem kerunit

Proof