Metamath Proof Explorer

Theorem rngodm1dm2

Description: In a unital ring the domain of the first variable of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	rnplrnml0.1	$⊢ H = 2^{nd} (R)$
		rnplrnml0.2	$⊢ G = 1^{st} (R)$
	Assertion	rngodm1dm2	$⊢ R \in RingOps \to dom dom G = dom dom H$

Proof

Step	Hyp	Ref	Expression
1		rnplrnml0.1	$⊢ H = 2^{nd} (R)$
2		rnplrnml0.2	$⊢ G = 1^{st} (R)$
3	2	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$
4		eqid	$⊢ ran G = ran G$
5	4	grpofo	$⊢ G \in GrpOp \to G : ran G \times ran G \underset{onto}{⟶} ran G$
6	3 5	syl	$⊢ R \in RingOps \to G : ran G \times ran G \underset{onto}{⟶} ran G$
7	2 1 4	rngosm	$⊢ R \in RingOps \to H : ran G \times ran G ⟶ ran G$
8		fof	$⊢ G : ran G \times ran G \underset{onto}{⟶} ran G \to G : ran G \times ran G ⟶ ran G$
9	8	fdmd	$⊢ G : ran G \times ran G \underset{onto}{⟶} ran G \to dom G = ran G \times ran G$
10		fdm	$⊢ H : ran G \times ran G ⟶ ran G \to dom H = ran G \times ran G$
11		eqtr	$⊢ (dom G = ran G \times ran G \land ran G \times ran G = dom H) \to dom G = dom H$
12	11	dmeqd	$⊢ (dom G = ran G \times ran G \land ran G \times ran G = dom H) \to dom dom G = dom dom H$
13	12	expcom	$⊢ ran G \times ran G = dom H \to (dom G = ran G \times ran G \to dom dom G = dom dom H)$
14	13	eqcoms	$⊢ dom H = ran G \times ran G \to (dom G = ran G \times ran G \to dom dom G = dom dom H)$
15	10 14	syl	$⊢ H : ran G \times ran G ⟶ ran G \to (dom G = ran G \times ran G \to dom dom G = dom dom H)$
16	9 15	syl5com	$⊢ G : ran G \times ran G \underset{onto}{⟶} ran G \to (H : ran G \times ran G ⟶ ran G \to dom dom G = dom dom H)$
17	6 7 16	sylc	$⊢ R \in RingOps \to dom dom G = dom dom H$