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 ⊢ ( 𝜑 → 𝑀 ∈ Grp )
grpidssd.s ⊢ ( 𝜑 → 𝑆 ∈ Grp )
grpidssd.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
grpidssd.c ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑀 ) )
grpidssd.o ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
Assertion grpidssd ( 𝜑 → ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑆 ) )

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 ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
7 3 6 grpidcl ⊢ ( 𝑆 ∈ Grp → ( 0g ‘ 𝑆 ) ∈ 𝐵 )
8 2 7 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ 𝐵 )
9 oveq1 ⊢ ( 𝑥 = ( 0g ‘ 𝑆 ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) 𝑦 ) )
10 oveq1 ⊢ ( 𝑥 = ( 0g ‘ 𝑆 ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) 𝑦 ) )
11 9 10 eqeq12d ⊢ ( 𝑥 = ( 0g ‘ 𝑆 ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ↔ ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) 𝑦 ) ) )
12 oveq2 ⊢ ( 𝑦 = ( 0g ‘ 𝑆 ) → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑆 ) ) )
13 oveq2 ⊢ ( 𝑦 = ( 0g ‘ 𝑆 ) → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) 𝑦 ) = ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) )
14 12 13 eqeq12d ⊢ ( 𝑦 = ( 0g ‘ 𝑆 ) → ( ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) 𝑦 ) ↔ ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑆 ) ) = ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) ) )
15 11 14 rspc2va ⊢ ( ( ( ( 0g ‘ 𝑆 ) ∈ 𝐵 ∧ ( 0g ‘ 𝑆 ) ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑆 ) ) = ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) )
16 8 8 5 15 syl21anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑆 ) ) = ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) )
17 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
18 3 17 6 grplid ⊢ ( ( 𝑆 ∈ Grp ∧ ( 0g ‘ 𝑆 ) ∈ 𝐵 ) → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑆 ) )
19 2 7 18 syl2anc2 ⊢ ( 𝜑 → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑆 ) )
20 16 19 eqtrd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑆 ) )
21 4 8 sseldd ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑀 ) )
22 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
23 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
24 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
25 22 23 24 grpidlcan ⊢ ( ( 𝑀 ∈ Grp ∧ ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑀 ) ) → ( ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑆 ) ↔ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑀 ) ) )
26 1 21 21 25 syl3anc ⊢ ( 𝜑 → ( ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑆 ) ↔ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑀 ) ) )
27 20 26 mpbid ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑀 ) )
28 27 eqcomd ⊢ ( 𝜑 → ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑆 ) )