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