Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Ring homomorphisms
rngogrphom
Next ⟩
rngohom0
Metamath Proof Explorer
Ascii
Unicode
Theorem
rngogrphom
Description:
A ring homomorphism is a group homomorphism.
(Contributed by
Jeff Madsen
, 2-Jan-2011)
Ref
Expression
Hypotheses
rnggrphom.1
⊢
G
=
1
st
⁡
R
rnggrphom.2
⊢
J
=
1
st
⁡
S
Assertion
rngogrphom
⊢
R
∈
RingOps
∧
S
∈
RingOps
∧
F
∈
R
RngHom
S
→
F
∈
G
GrpOpHom
J
Proof
Step
Hyp
Ref
Expression
1
rnggrphom.1
⊢
G
=
1
st
⁡
R
2
rnggrphom.2
⊢
J
=
1
st
⁡
S
3
eqid
⊢
ran
⁡
G
=
ran
⁡
G
4
eqid
⊢
ran
⁡
J
=
ran
⁡
J
5
1
3
2
4
rngohomf
⊢
R
∈
RingOps
∧
S
∈
RingOps
∧
F
∈
R
RngHom
S
→
F
:
ran
⁡
G
⟶
ran
⁡
J
6
1
3
2
rngohomadd
⊢
R
∈
RingOps
∧
S
∈
RingOps
∧
F
∈
R
RngHom
S
∧
x
∈
ran
⁡
G
∧
y
∈
ran
⁡
G
→
F
⁡
x
G
y
=
F
⁡
x
J
F
⁡
y
7
6
eqcomd
⊢
R
∈
RingOps
∧
S
∈
RingOps
∧
F
∈
R
RngHom
S
∧
x
∈
ran
⁡
G
∧
y
∈
ran
⁡
G
→
F
⁡
x
J
F
⁡
y
=
F
⁡
x
G
y
8
7
ralrimivva
⊢
R
∈
RingOps
∧
S
∈
RingOps
∧
F
∈
R
RngHom
S
→
∀
x
∈
ran
⁡
G
∀
y
∈
ran
⁡
G
F
⁡
x
J
F
⁡
y
=
F
⁡
x
G
y
9
1
rngogrpo
⊢
R
∈
RingOps
→
G
∈
GrpOp
10
2
rngogrpo
⊢
S
∈
RingOps
→
J
∈
GrpOp
11
3
4
elghomOLD
⊢
G
∈
GrpOp
∧
J
∈
GrpOp
→
F
∈
G
GrpOpHom
J
↔
F
:
ran
⁡
G
⟶
ran
⁡
J
∧
∀
x
∈
ran
⁡
G
∀
y
∈
ran
⁡
G
F
⁡
x
J
F
⁡
y
=
F
⁡
x
G
y
12
9
10
11
syl2an
⊢
R
∈
RingOps
∧
S
∈
RingOps
→
F
∈
G
GrpOpHom
J
↔
F
:
ran
⁡
G
⟶
ran
⁡
J
∧
∀
x
∈
ran
⁡
G
∀
y
∈
ran
⁡
G
F
⁡
x
J
F
⁡
y
=
F
⁡
x
G
y
13
12
3adant3
⊢
R
∈
RingOps
∧
S
∈
RingOps
∧
F
∈
R
RngHom
S
→
F
∈
G
GrpOpHom
J
↔
F
:
ran
⁡
G
⟶
ran
⁡
J
∧
∀
x
∈
ran
⁡
G
∀
y
∈
ran
⁡
G
F
⁡
x
J
F
⁡
y
=
F
⁡
x
G
y
14
5
8
13
mpbir2and
⊢
R
∈
RingOps
∧
S
∈
RingOps
∧
F
∈
R
RngHom
S
→
F
∈
G
GrpOpHom
J