This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem unitrrg

Description: Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015)

Ref Expression
Hypotheses unitrrg.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
unitrrg.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion unitrrg ( 𝑅 ∈ Ring → 𝑈 ⊆ 𝐸 )

Proof

Step Hyp Ref Expression
1 unitrrg.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
2 unitrrg.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 3 2 unitcl ⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( Base ‘ 𝑅 ) )
5 4 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
6 oveq2 ⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
7 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
8 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 2 7 8 9 unitlinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
11 10 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
12 11 oveq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑦 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) )
13 simpll ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
14 2 7 3 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
15 14 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
16 5 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
17 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
18 3 8 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑦 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
19 13 15 16 17 18 syl13anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑦 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
20 3 8 9 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 )
21 20 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 )
22 12 19 21 3eqtr3d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = 𝑦 )
23 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
24 3 8 23 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
25 13 15 24 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
26 22 25 eqeq12d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) ↔ 𝑦 = ( 0g ‘ 𝑅 ) ) )
27 6 26 imbitrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → 𝑦 = ( 0g ‘ 𝑅 ) ) )
28 27 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → 𝑦 = ( 0g ‘ 𝑅 ) ) )
29 1 3 8 23 isrrg ⊢ ( 𝑥 ∈ 𝐸 ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → 𝑦 = ( 0g ‘ 𝑅 ) ) ) )
30 5 28 29 sylanbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝐸 )
31 30 ex ⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ 𝑈 → 𝑥 ∈ 𝐸 ) )
32 31 ssrdv ⊢ ( 𝑅 ∈ Ring → 𝑈 ⊆ 𝐸 )