Metamath Proof Explorer

Theorem submnd0OLD

Description: Obsolete version of submnd0 as of 12-Aug-2026. The zero of a submonoid is the same as the zero in the parent monoid. (Contributed by Mario Carneiro, 10-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses submnd0.b ⊢ B = Base G
submnd0.z ⊢ 0 ˙ = 0 G
submnd0.h ⊢ H = G ↾ 𝑠 S
Assertion submnd0OLD ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S → 0 ˙ = 0 H

Proof

Step Hyp Ref Expression
1 submnd0.b ⊢ B = Base G
2 submnd0.z ⊢ 0 ˙ = 0 G
3 submnd0.h ⊢ H = G ↾ 𝑠 S
4 eqid ⊢ Base H = Base H
5 eqid ⊢ 0 H = 0 H
6 eqid ⊢ + H = + H
7 simprr ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S → 0 ˙ ∈ S
8 3 1 ressbas2 ⊢ S ⊆ B → S = Base H
9 8 ad2antrl ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S → S = Base H
10 7 9 eleqtrd ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S → 0 ˙ ∈ Base H
11 fvex ⊢ Base H ∈ V
12 9 11 eqeltrdi ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S → S ∈ V
13 12 adantr ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ∧ x ∈ Base H → S ∈ V
14 eqid ⊢ + G = + G
15 3 14 ressplusg ⊢ S ∈ V → + G = + H
16 13 15 syl ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ∧ x ∈ Base H → + G = + H
17 16 oveqd ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ∧ x ∈ Base H → 0 ˙ + G x = 0 ˙ + H x
18 simpll ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S → G ∈ Mnd
19 3 1 ressbasss ⊢ Base H ⊆ B
20 19 sseli ⊢ x ∈ Base H → x ∈ B
21 1 14 2 mndlid ⊢ G ∈ Mnd ∧ x ∈ B → 0 ˙ + G x = x
22 18 20 21 syl2an ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ∧ x ∈ Base H → 0 ˙ + G x = x
23 17 22 eqtr3d ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ∧ x ∈ Base H → 0 ˙ + H x = x
24 16 oveqd ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ∧ x ∈ Base H → x + G 0 ˙ = x + H 0 ˙
25 1 14 2 mndrid ⊢ G ∈ Mnd ∧ x ∈ B → x + G 0 ˙ = x
26 18 20 25 syl2an ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ∧ x ∈ Base H → x + G 0 ˙ = x
27 24 26 eqtr3d ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S ∧ x ∈ Base H → x + H 0 ˙ = x
28 4 5 6 10 23 27 ismgmid2 ⊢ G ∈ Mnd ∧ H ∈ Mnd ∧ S ⊆ B ∧ 0 ˙ ∈ S → 0 ˙ = 0 H