Metamath Proof Explorer


Theorem grpinvssd

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 the elements of the first group have the same inverses in both groups. (Contributed by AV, 15-Mar-2019)

Ref Expression
Hypotheses grpidssd.m ( 𝜑𝑀 ∈ Grp )
grpidssd.s ( 𝜑𝑆 ∈ Grp )
grpidssd.b 𝐵 = ( Base ‘ 𝑆 )
grpidssd.c ( 𝜑𝐵 ⊆ ( Base ‘ 𝑀 ) )
grpidssd.o ( 𝜑 → ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 ( +g𝑀 ) 𝑦 ) = ( 𝑥 ( +g𝑆 ) 𝑦 ) )
Assertion grpinvssd ( 𝜑 → ( 𝑋𝐵 → ( ( invg𝑆 ) ‘ 𝑋 ) = ( ( invg𝑀 ) ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 grpidssd.m ( 𝜑𝑀 ∈ Grp )
2 grpidssd.s ( 𝜑𝑆 ∈ Grp )
3 grpidssd.b 𝐵 = ( Base ‘ 𝑆 )
4 grpidssd.c ( 𝜑𝐵 ⊆ ( Base ‘ 𝑀 ) )
5 grpidssd.o ( 𝜑 → ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 ( +g𝑀 ) 𝑦 ) = ( 𝑥 ( +g𝑆 ) 𝑦 ) )
6 eqid ( invg𝑆 ) = ( invg𝑆 )
7 3 6 grpinvcl ( ( 𝑆 ∈ Grp ∧ 𝑋𝐵 ) → ( ( invg𝑆 ) ‘ 𝑋 ) ∈ 𝐵 )
8 2 7 sylan ( ( 𝜑𝑋𝐵 ) → ( ( invg𝑆 ) ‘ 𝑋 ) ∈ 𝐵 )
9 simpr ( ( 𝜑𝑋𝐵 ) → 𝑋𝐵 )
10 5 adantr ( ( 𝜑𝑋𝐵 ) → ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 ( +g𝑀 ) 𝑦 ) = ( 𝑥 ( +g𝑆 ) 𝑦 ) )
11 oveq1 ( 𝑥 = ( ( invg𝑆 ) ‘ 𝑋 ) → ( 𝑥 ( +g𝑀 ) 𝑦 ) = ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑦 ) )
12 oveq1 ( 𝑥 = ( ( invg𝑆 ) ‘ 𝑋 ) → ( 𝑥 ( +g𝑆 ) 𝑦 ) = ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑆 ) 𝑦 ) )
13 11 12 eqeq12d ( 𝑥 = ( ( invg𝑆 ) ‘ 𝑋 ) → ( ( 𝑥 ( +g𝑀 ) 𝑦 ) = ( 𝑥 ( +g𝑆 ) 𝑦 ) ↔ ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑦 ) = ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑆 ) 𝑦 ) ) )
14 oveq2 ( 𝑦 = 𝑋 → ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑦 ) = ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) )
15 oveq2 ( 𝑦 = 𝑋 → ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑆 ) 𝑦 ) = ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑆 ) 𝑋 ) )
16 14 15 eqeq12d ( 𝑦 = 𝑋 → ( ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑦 ) = ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑆 ) 𝑦 ) ↔ ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) = ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑆 ) 𝑋 ) ) )
17 13 16 rspc2va ( ( ( ( ( invg𝑆 ) ‘ 𝑋 ) ∈ 𝐵𝑋𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 ( +g𝑀 ) 𝑦 ) = ( 𝑥 ( +g𝑆 ) 𝑦 ) ) → ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) = ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑆 ) 𝑋 ) )
18 8 9 10 17 syl21anc ( ( 𝜑𝑋𝐵 ) → ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) = ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑆 ) 𝑋 ) )
19 eqid ( +g𝑆 ) = ( +g𝑆 )
20 eqid ( 0g𝑆 ) = ( 0g𝑆 )
21 3 19 20 6 grplinv ( ( 𝑆 ∈ Grp ∧ 𝑋𝐵 ) → ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑆 ) 𝑋 ) = ( 0g𝑆 ) )
22 2 21 sylan ( ( 𝜑𝑋𝐵 ) → ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑆 ) 𝑋 ) = ( 0g𝑆 ) )
23 4 sselda ( ( 𝜑𝑋𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑀 ) )
24 eqid ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
25 eqid ( +g𝑀 ) = ( +g𝑀 )
26 eqid ( 0g𝑀 ) = ( 0g𝑀 )
27 eqid ( invg𝑀 ) = ( invg𝑀 )
28 24 25 26 27 grplinv ( ( 𝑀 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑀 ) ) → ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) = ( 0g𝑀 ) )
29 1 23 28 syl2an2r ( ( 𝜑𝑋𝐵 ) → ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) = ( 0g𝑀 ) )
30 1 2 3 4 5 grpidssd ( 𝜑 → ( 0g𝑀 ) = ( 0g𝑆 ) )
31 30 adantr ( ( 𝜑𝑋𝐵 ) → ( 0g𝑀 ) = ( 0g𝑆 ) )
32 29 31 eqtr2d ( ( 𝜑𝑋𝐵 ) → ( 0g𝑆 ) = ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) )
33 18 22 32 3eqtrd ( ( 𝜑𝑋𝐵 ) → ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) = ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) )
34 1 adantr ( ( 𝜑𝑋𝐵 ) → 𝑀 ∈ Grp )
35 4 adantr ( ( 𝜑𝑋𝐵 ) → 𝐵 ⊆ ( Base ‘ 𝑀 ) )
36 35 8 sseldd ( ( 𝜑𝑋𝐵 ) → ( ( invg𝑆 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑀 ) )
37 24 27 grpinvcl ( ( 𝑀 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑀 ) ) → ( ( invg𝑀 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑀 ) )
38 1 23 37 syl2an2r ( ( 𝜑𝑋𝐵 ) → ( ( invg𝑀 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑀 ) )
39 24 25 grprcan ( ( 𝑀 ∈ Grp ∧ ( ( ( invg𝑆 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑀 ) ∧ ( ( invg𝑀 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑀 ) ∧ 𝑋 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) = ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) ↔ ( ( invg𝑆 ) ‘ 𝑋 ) = ( ( invg𝑀 ) ‘ 𝑋 ) ) )
40 34 36 38 23 39 syl13anc ( ( 𝜑𝑋𝐵 ) → ( ( ( ( invg𝑆 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) = ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑋 ) ↔ ( ( invg𝑆 ) ‘ 𝑋 ) = ( ( invg𝑀 ) ‘ 𝑋 ) ) )
41 33 40 mpbid ( ( 𝜑𝑋𝐵 ) → ( ( invg𝑆 ) ‘ 𝑋 ) = ( ( invg𝑀 ) ‘ 𝑋 ) )
42 41 ex ( 𝜑 → ( 𝑋𝐵 → ( ( invg𝑆 ) ‘ 𝑋 ) = ( ( invg𝑀 ) ‘ 𝑋 ) ) )