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

Metamath Proof Explorer

Theorem isunit3

Description: Alternate definition of being a unit. (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses isunit2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isunit2.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
isunit2.m ⊢ · = ( .r ‘ 𝑅 )
isunit2.1 ⊢ 1 = ( 1r ‘ 𝑅 )
isunit3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
isunit3.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion isunit3 ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑋 ) = 1 ) ) )

Proof

Step Hyp Ref Expression
1 isunit2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isunit2.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 isunit2.m ⊢ · = ( .r ‘ 𝑅 )
4 isunit2.1 ⊢ 1 = ( 1r ‘ 𝑅 )
5 isunit3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 isunit3.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 1 2 3 4 isunit2 ⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐵 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) )
8 5 biantrurd ⊢ ( 𝜑 → ( ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) ) )
9 7 8 bitr4id ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) )
10 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
11 10 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
12 10 4 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
13 10 3 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
14 10 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
15 6 14 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
16 11 12 13 15 5 mndlrinvb ⊢ ( 𝜑 → ( ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑋 ) = 1 ) ) )
17 9 16 bitrd ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑋 ) = 1 ) ) )