# 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}\left({R}\right)$
rnplrnml0.2 ${⊢}{G}={1}^{st}\left({R}\right)$
Assertion rngodm1dm2 ${⊢}{R}\in \mathrm{RingOps}\to \mathrm{dom}\mathrm{dom}{G}=\mathrm{dom}\mathrm{dom}{H}$

### Proof

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