Theorem 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	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	kerunit.2	⊢ 0 = ( 0g ‘ 𝑆 )
	kerunit.3	⊢ 1 = ( 1r ‘ 𝑆 )
Assertion	kerunit	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ≠ ∅ ) → 1 = 0 )

Proof

Step	Hyp	Ref	Expression
1		kerunit.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		kerunit.2	⊢ 0 = ( 0g ‘ 𝑆 )
3		kerunit.3	⊢ 1 = ( 1r ‘ 𝑆 )
4		elin	⊢ ( 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ↔ ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) )
5	4	bilani	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) )
6	5	simpld	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → 𝑥 ∈ 𝑈 )
7		rhmrcl1	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
8		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
9		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
10		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
11	1 8 9 10	unitlinv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
12	11	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( 𝐹 ‘ ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ) = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) )
13	7 12	sylan	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝐹 ‘ ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ) = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) )
14	6 13	syldan	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( 𝐹 ‘ ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ) = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) )
15		simpl	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
16	7	adantr	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → 𝑅 ∈ Ring )
17		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18	1 8 17	ringinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
19	16 6 18	syl2anc	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
20	17 1	unitcl	⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( Base ‘ 𝑅 ) )
21	6 20	syl	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
22		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
23	17 9 22	rhmmul	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ) = ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) )
24	15 19 21 23	syl3anc	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( 𝐹 ‘ ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ) = ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) )
25	5	simprd	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) )
26		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
27	17 26	rhmf	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
28		ffn	⊢ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) → 𝐹 Fn ( Base ‘ 𝑅 ) )
29		elpreima	⊢ ( 𝐹 Fn ( Base ‘ 𝑅 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ) ) )
30	27 28 29	3syl	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ) ) )
31	30	simplbda	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
32	25 31	syldan	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
33		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
34	33	elsn	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ↔ ( 𝐹 ‘ 𝑥 ) = 0 )
35	32 34	sylib	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
36	35	oveq2d	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ( .r ‘ 𝑆 ) 0 ) )
37		rhmrcl2	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
38	37	adantr	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → 𝑆 ∈ Ring )
39	27	adantr	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
40	39 19	ffvelcdmd	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑆 ) )
41	26 22 2	ringrz	⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ( .r ‘ 𝑆 ) 0 ) = 0 )
42	38 40 41	syl2anc	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ( .r ‘ 𝑆 ) 0 ) = 0 )
43	24 36 42	3eqtrd	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( 𝐹 ‘ ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ) = 0 )
44	10 3	rhm1	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = 1 )
45	44	adantr	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = 1 )
46	14 43 45	3eqtr3rd	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ) → 1 = 0 )
47	46	reximdva0	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ≠ ∅ ) → ∃ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) 1 = 0 )
48		id	⊢ ( 1 = 0 → 1 = 0 )
49	48	rexlimivw	⊢ ( ∃ 𝑥 ∈ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) 1 = 0 → 1 = 0 )
50	47 49	syl	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝑈 ∩ ( ◡ 𝐹 “ { 0 } ) ) ≠ ∅ ) → 1 = 0 )