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

Metamath Proof Explorer

Theorem isunit2

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 ‘ 𝑅 )
Assertion isunit2 ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐵 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 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 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
6 1 5 3 dvdsr ⊢ ( 𝑋 ( ∥r ‘ 𝑅 ) 1 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) )
7 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
8 7 1 opprbas ⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
9 eqid ⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
10 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
11 8 9 10 dvdsr ⊢ ( 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ) )
12 1 3 7 10 opprmul ⊢ ( 𝑢 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑋 · 𝑢 )
13 12 eqeq1i ⊢ ( ( 𝑢 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ↔ ( 𝑋 · 𝑢 ) = 1 )
14 13 rexbii ⊢ ( ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ↔ ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 )
15 14 anbi2i ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑢 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ) )
16 11 15 bitri ⊢ ( 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ) )
17 6 16 anbi12ci ⊢ ( ( 𝑋 ( ∥r ‘ 𝑅 ) 1 ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) )
18 2 4 5 7 9 isunit ⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ( ∥r ‘ 𝑅 ) 1 ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) )
19 anandi ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) )
20 17 18 19 3bitr4i ⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐵 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 · 𝑢 ) = 1 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 · 𝑋 ) = 1 ) ) )