rngokerinj

Description: A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	rngkerinj.1	$⊢ G = 1^{st} (R)$
	rngkerinj.2	$⊢ X = ran G$
	rngkerinj.3	$⊢ W = GId (G)$
	rngkerinj.4	$⊢ J = 1^{st} (S)$
	rngkerinj.5	$⊢ Y = ran J$
	rngkerinj.6	$⊢ Z = GId (J)$
Assertion	rngokerinj	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (F : X \underset{1-1}{⟶} Y \leftrightarrow F^{-1} [\{Z\}] = \{W\})$

Step	Hyp	Ref	Expression
1		rngkerinj.1	$⊢ G = 1^{st} (R)$
2		rngkerinj.2	$⊢ X = ran G$
3		rngkerinj.3	$⊢ W = GId (G)$
4		rngkerinj.4	$⊢ J = 1^{st} (S)$
5		rngkerinj.5	$⊢ Y = ran J$
6		rngkerinj.6	$⊢ Z = GId (J)$
7		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
8	7	rngogrpo	$⊢ R \in RingOps \to 1^{st} (R) \in GrpOp$
9	8	3ad2ant1	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to 1^{st} (R) \in GrpOp$
10		eqid	$⊢ 1^{st} (S) = 1^{st} (S)$
11	10	rngogrpo	$⊢ S \in RingOps \to 1^{st} (S) \in GrpOp$
12	11	3ad2ant2	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to 1^{st} (S) \in GrpOp$
13	7 10	rngogrphom	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to F \in (1^{st} (R) GrpOpHom 1^{st} (S))$
14	1	rneqi	$⊢ ran G = ran 1^{st} (R)$
15	2 14	eqtri	$⊢ X = ran 1^{st} (R)$
16	1	fveq2i	$⊢ GId (G) = GId (1^{st} (R))$
17	3 16	eqtri	$⊢ W = GId (1^{st} (R))$
18	4	rneqi	$⊢ ran J = ran 1^{st} (S)$
19	5 18	eqtri	$⊢ Y = ran 1^{st} (S)$
20	4	fveq2i	$⊢ GId (J) = GId (1^{st} (S))$
21	6 20	eqtri	$⊢ Z = GId (1^{st} (S))$
22	15 17 19 21	grpokerinj	$⊢ (1^{st} (R) \in GrpOp \land 1^{st} (S) \in GrpOp \land F \in (1^{st} (R) GrpOpHom 1^{st} (S))) \to (F : X \underset{1-1}{⟶} Y \leftrightarrow F^{-1} [\{Z\}] = \{W\})$
23	9 12 13 22	syl3anc	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngHom S)) \to (F : X \underset{1-1}{⟶} Y \leftrightarrow F^{-1} [\{Z\}] = \{W\})$

Metamath Proof Explorer