Metamath Proof Explorer


Theorem isrhm2d

Description: Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015)

Ref Expression
Hypotheses isrhmd.b B = Base R
isrhmd.o 1 ˙ = 1 R
isrhmd.n N = 1 S
isrhmd.t · ˙ = R
isrhmd.u × ˙ = S
isrhmd.r φ R Ring
isrhmd.s φ S Ring
isrhmd.ho φ F 1 ˙ = N
isrhmd.ht φ x B y B F x · ˙ y = F x × ˙ F y
isrhm2d.f φ F R GrpHom S
Assertion isrhm2d φ F R RingHom S

Proof

Step Hyp Ref Expression
1 isrhmd.b B = Base R
2 isrhmd.o 1 ˙ = 1 R
3 isrhmd.n N = 1 S
4 isrhmd.t · ˙ = R
5 isrhmd.u × ˙ = S
6 isrhmd.r φ R Ring
7 isrhmd.s φ S Ring
8 isrhmd.ho φ F 1 ˙ = N
9 isrhmd.ht φ x B y B F x · ˙ y = F x × ˙ F y
10 isrhm2d.f φ F R GrpHom S
11 eqid mulGrp R = mulGrp R
12 11 ringmgp R Ring mulGrp R Mnd
13 6 12 syl φ mulGrp R Mnd
14 eqid mulGrp S = mulGrp S
15 14 ringmgp S Ring mulGrp S Mnd
16 7 15 syl φ mulGrp S Mnd
17 eqid Base S = Base S
18 1 17 ghmf F R GrpHom S F : B Base S
19 10 18 syl φ F : B Base S
20 9 ralrimivva φ x B y B F x · ˙ y = F x × ˙ F y
21 11 2 ringidval 1 ˙ = 0 mulGrp R
22 21 fveq2i F 1 ˙ = F 0 mulGrp R
23 14 3 ringidval N = 0 mulGrp S
24 8 22 23 3eqtr3g φ F 0 mulGrp R = 0 mulGrp S
25 19 20 24 3jca φ F : B Base S x B y B F x · ˙ y = F x × ˙ F y F 0 mulGrp R = 0 mulGrp S
26 11 1 mgpbas B = Base mulGrp R
27 14 17 mgpbas Base S = Base mulGrp S
28 11 4 mgpplusg · ˙ = + mulGrp R
29 14 5 mgpplusg × ˙ = + mulGrp S
30 eqid 0 mulGrp R = 0 mulGrp R
31 eqid 0 mulGrp S = 0 mulGrp S
32 26 27 28 29 30 31 ismhm F mulGrp R MndHom mulGrp S mulGrp R Mnd mulGrp S Mnd F : B Base S x B y B F x · ˙ y = F x × ˙ F y F 0 mulGrp R = 0 mulGrp S
33 13 16 25 32 syl21anbrc φ F mulGrp R MndHom mulGrp S
34 10 33 jca φ F R GrpHom S F mulGrp R MndHom mulGrp S
35 11 14 isrhm F R RingHom S R Ring S Ring F R GrpHom S F mulGrp R MndHom mulGrp S
36 6 7 34 35 syl21anbrc φ F R RingHom S