Metamath Proof Explorer

Theorem ringidss

Description: A subset of the multiplicative group has the multiplicative identity as its identity if the identity is in the subset. (Contributed by Mario Carneiro, 27-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses ringidss.g ⊢ 𝑀 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝐴 )
ringidss.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringidss.u ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion ringidss ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) → 1 = ( 0g ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 ringidss.g ⊢ 𝑀 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝐴 )
2 ringidss.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 ringidss.u ⊢ 1 = ( 1r ‘ 𝑅 )
4 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
5 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
6 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
7 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) → 1 ∈ 𝐴 )
8 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
9 8 2 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
10 1 9 ressbas2 ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ 𝑀 ) )
11 10 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) → 𝐴 = ( Base ‘ 𝑀 ) )
12 7 11 eleqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) → 1 ∈ ( Base ‘ 𝑀 ) )
13 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) → 𝐴 ⊆ 𝐵 )
14 11 13 eqsstrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) → ( Base ‘ 𝑀 ) ⊆ 𝐵 )
15 14 sselda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → 𝑦 ∈ 𝐵 )
16 fvex ⊢ ( Base ‘ 𝑀 ) ∈ V
17 11 16 eqeltrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) → 𝐴 ∈ V )
18 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
19 8 18 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
20 1 19 ressplusg ⊢ ( 𝐴 ∈ V → ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 ) )
21 17 20 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) → ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 ) )
22 21 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 ) )
23 22 oveqd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) 𝑦 ) = ( 1 ( +g ‘ 𝑀 ) 𝑦 ) )
24 2 18 3 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 )
25 24 3ad2antl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 )
26 23 25 eqtr3d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 1 ( +g ‘ 𝑀 ) 𝑦 ) = 𝑦 )
27 15 26 syldan ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 1 ( +g ‘ 𝑀 ) 𝑦 ) = 𝑦 )
28 22 oveqd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( .r ‘ 𝑅 ) 1 ) = ( 𝑦 ( +g ‘ 𝑀 ) 1 ) )
29 2 18 3 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( .r ‘ 𝑅 ) 1 ) = 𝑦 )
30 29 3ad2antl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( .r ‘ 𝑅 ) 1 ) = 𝑦 )
31 28 30 eqtr3d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑀 ) 1 ) = 𝑦 )
32 15 31 syldan ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑦 ( +g ‘ 𝑀 ) 1 ) = 𝑦 )
33 4 5 6 12 27 32 ismgmid2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) → 1 = ( 0g ‘ 𝑀 ) )