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