This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
rnplrnml0.2 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
Assertion rngodm1dm2 ( 𝑅 ∈ RingOps → dom dom 𝐺 = dom dom 𝐻 )

Proof

Step Hyp Ref Expression
1 rnplrnml0.1 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
2 rnplrnml0.2 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
3 2 rngogrpo ⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )
4 eqid ⊢ ran 𝐺 = ran 𝐺
5 4 grpofo ⊢ ( 𝐺 ∈ GrpOp → 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 )
6 3 5 syl ⊢ ( 𝑅 ∈ RingOps → 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 )
7 2 1 4 rngosm ⊢ ( 𝑅 ∈ RingOps → 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 )
8 fof ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 → 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 )
9 8 fdmd ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 → dom 𝐺 = ( ran 𝐺 × ran 𝐺 ) )
10 fdm ⊢ ( 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 → dom 𝐻 = ( ran 𝐺 × ran 𝐺 ) )
11 eqtr ⊢ ( ( dom 𝐺 = ( ran 𝐺 × ran 𝐺 ) ∧ ( ran 𝐺 × ran 𝐺 ) = dom 𝐻 ) → dom 𝐺 = dom 𝐻 )
12 11 dmeqd ⊢ ( ( dom 𝐺 = ( ran 𝐺 × ran 𝐺 ) ∧ ( ran 𝐺 × ran 𝐺 ) = dom 𝐻 ) → dom dom 𝐺 = dom dom 𝐻 )
13 12 expcom ⊢ ( ( ran 𝐺 × ran 𝐺 ) = dom 𝐻 → ( dom 𝐺 = ( ran 𝐺 × ran 𝐺 ) → dom dom 𝐺 = dom dom 𝐻 ) )
14 13 eqcoms ⊢ ( dom 𝐻 = ( ran 𝐺 × ran 𝐺 ) → ( dom 𝐺 = ( ran 𝐺 × ran 𝐺 ) → dom dom 𝐺 = dom dom 𝐻 ) )
15 10 14 syl ⊢ ( 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 → ( dom 𝐺 = ( ran 𝐺 × ran 𝐺 ) → dom dom 𝐺 = dom dom 𝐻 ) )
16 9 15 syl5com ⊢ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) –onto→ ran 𝐺 → ( 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 → dom dom 𝐺 = dom dom 𝐻 ) )
17 6 7 16 sylc ⊢ ( 𝑅 ∈ RingOps → dom dom 𝐺 = dom dom 𝐻 )