Metamath Proof Explorer

Theorem rrgsubm

Description: The left regular elements of a ring form a submonoid of the multiplicative group. (Contributed by Thierry Arnoux, 10-May-2025)

Ref Expression
Hypotheses rrgsubm.1 ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
rrgsubm.2 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
rrgsubm.3 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion rrgsubm ( 𝜑 → 𝐸 ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 rrgsubm.1 ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
2 rrgsubm.2 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
3 rrgsubm.3 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 2 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
5 3 4 syl ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 1 6 rrgss ⊢ 𝐸 ⊆ ( Base ‘ 𝑅 )
8 7 a1i ⊢ ( 𝜑 → 𝐸 ⊆ ( Base ‘ 𝑅 ) )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 9 1 3 1rrg ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐸 )
11 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) → 𝑅 ∈ Ring )
13 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) → 𝑥 ∈ 𝐸 )
14 7 13 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
15 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) → 𝑦 ∈ 𝐸 )
16 7 15 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
17 6 11 12 14 16 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
18 15 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → 𝑦 ∈ 𝐸 )
19 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
20 13 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → 𝑥 ∈ 𝐸 )
21 12 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
22 16 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
23 6 11 21 22 19 ringcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
24 14 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
25 6 11 21 24 22 19 ringassd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
26 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) )
27 25 26 eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( 0g ‘ 𝑅 ) )
28 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
29 1 6 11 28 rrgeq0i ⊢ ( ( 𝑥 ∈ 𝐸 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( 0g ‘ 𝑅 ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) )
30 29 imp ⊢ ( ( ( 𝑥 ∈ 𝐸 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) )
31 20 23 27 30 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) )
32 1 6 11 28 rrgeq0i ⊢ ( ( 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → 𝑧 = ( 0g ‘ 𝑅 ) ) )
33 32 imp ⊢ ( ( ( 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → 𝑧 = ( 0g ‘ 𝑅 ) )
34 18 19 31 33 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) ) → 𝑧 = ( 0g ‘ 𝑅 ) )
35 34 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → 𝑧 = ( 0g ‘ 𝑅 ) ) )
36 35 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) → ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → 𝑧 = ( 0g ‘ 𝑅 ) ) )
37 1 6 11 28 isrrg ⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐸 ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → 𝑧 = ( 0g ‘ 𝑅 ) ) ) )
38 17 36 37 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐸 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐸 )
39 38 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐸 )
40 39 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐸 )
41 2 6 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
42 2 9 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
43 2 11 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
44 41 42 43 issubm ⊢ ( 𝑀 ∈ Mnd → ( 𝐸 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝐸 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐸 ∧ ∀ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐸 ) ) )
45 44 biimpar ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝐸 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐸 ∧ ∀ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐸 ) ) → 𝐸 ∈ ( SubMnd ‘ 𝑀 ) )
46 5 8 10 40 45 syl13anc ⊢ ( 𝜑 → 𝐸 ∈ ( SubMnd ‘ 𝑀 ) )