Metamath Proof Explorer


Theorem grpidssd

Description: If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then both groups have the same identity element. (Contributed by AV, 15-Mar-2019)

Ref Expression
Hypotheses grpidssd.m φ M Grp
grpidssd.s φ S Grp
grpidssd.b B = Base S
grpidssd.c φ B Base M
grpidssd.o φ x B y B x + M y = x + S y
Assertion grpidssd φ 0 M = 0 S

Proof

Step Hyp Ref Expression
1 grpidssd.m φ M Grp
2 grpidssd.s φ S Grp
3 grpidssd.b B = Base S
4 grpidssd.c φ B Base M
5 grpidssd.o φ x B y B x + M y = x + S y
6 eqid 0 S = 0 S
7 3 6 grpidcl S Grp 0 S B
8 2 7 syl φ 0 S B
9 oveq1 x = 0 S x + M y = 0 S + M y
10 oveq1 x = 0 S x + S y = 0 S + S y
11 9 10 eqeq12d x = 0 S x + M y = x + S y 0 S + M y = 0 S + S y
12 oveq2 y = 0 S 0 S + M y = 0 S + M 0 S
13 oveq2 y = 0 S 0 S + S y = 0 S + S 0 S
14 12 13 eqeq12d y = 0 S 0 S + M y = 0 S + S y 0 S + M 0 S = 0 S + S 0 S
15 11 14 rspc2va 0 S B 0 S B x B y B x + M y = x + S y 0 S + M 0 S = 0 S + S 0 S
16 8 8 5 15 syl21anc φ 0 S + M 0 S = 0 S + S 0 S
17 eqid + S = + S
18 3 17 6 grplid S Grp 0 S B 0 S + S 0 S = 0 S
19 2 7 18 syl2anc2 φ 0 S + S 0 S = 0 S
20 16 19 eqtrd φ 0 S + M 0 S = 0 S
21 4 8 sseldd φ 0 S Base M
22 eqid Base M = Base M
23 eqid + M = + M
24 eqid 0 M = 0 M
25 22 23 24 grpidlcan M Grp 0 S Base M 0 S Base M 0 S + M 0 S = 0 S 0 S = 0 M
26 1 21 21 25 syl3anc φ 0 S + M 0 S = 0 S 0 S = 0 M
27 20 26 mpbid φ 0 S = 0 M
28 27 eqcomd φ 0 M = 0 S