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 ‘ 𝑀 ) ‘ 𝑋 ) ) )