This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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