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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
submnd0.z ⊢ 0 = ( 0g ‘ 𝐺 )
submnd0.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
Assertion submnd0OLD ( ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ) ) → 0 = ( 0g ‘ 𝐻 ) )

Proof

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