Description: In a unital ring the range 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 | ⊢ 𝐻 = ( 2^{nd} ‘ 𝑅 ) | |
rnplrnml0.2 | ⊢ 𝐺 = ( 1^{st} ‘ 𝑅 ) | ||
Assertion | rngorn1 | ⊢ ( 𝑅 ∈ RingOps → ran 𝐺 = dom dom 𝐻 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnplrnml0.1 | ⊢ 𝐻 = ( 2^{nd} ‘ 𝑅 ) | |
2 | rnplrnml0.2 | ⊢ 𝐺 = ( 1^{st} ‘ 𝑅 ) | |
3 | 2 | rngogrpo | ⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp ) |
4 | grporndm | ⊢ ( 𝐺 ∈ GrpOp → ran 𝐺 = dom dom 𝐺 ) | |
5 | 3 4 | syl | ⊢ ( 𝑅 ∈ RingOps → ran 𝐺 = dom dom 𝐺 ) |
6 | 1 2 | rngodm1dm2 | ⊢ ( 𝑅 ∈ RingOps → dom dom 𝐺 = dom dom 𝐻 ) |
7 | 5 6 | eqtrd | ⊢ ( 𝑅 ∈ RingOps → ran 𝐺 = dom dom 𝐻 ) |