Metamath Proof Explorer

Theorem islring

Description: The predicate "is a local ring". (Contributed by SN, 23-Feb-2025)

Ref Expression
Hypotheses islring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
islring.a ⊢ + = ( +g ‘ 𝑅 )
islring.1 ⊢ 1 = ( 1r ‘ 𝑅 )
islring.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion islring ( 𝑅 ∈ LRing ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )

Proof

Step Hyp Ref Expression
1 islring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 islring.a ⊢ + = ( +g ‘ 𝑅 )
3 islring.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 islring.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
5 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
6 5 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
7 fveq2 ⊢ ( 𝑟 = 𝑅 → ( +g ‘ 𝑟 ) = ( +g ‘ 𝑅 ) )
8 7 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( +g ‘ 𝑟 ) = + )
9 8 oveqd ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
10 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = ( 1r ‘ 𝑅 ) )
11 10 3 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = 1 )
12 9 11 eqeq12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) ↔ ( 𝑥 + 𝑦 ) = 1 ) )
13 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) )
14 13 4 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = 𝑈 )
15 14 eleq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ↔ 𝑥 ∈ 𝑈 ) )
16 14 eleq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑦 ∈ ( Unit ‘ 𝑟 ) ↔ 𝑦 ∈ 𝑈 ) )
17 15 16 orbi12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) ↔ ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) )
18 12 17 imbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) ) ↔ ( ( 𝑥 + 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
19 6 18 raleqbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
20 6 19 raleqbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
21 df-lring ⊢ LRing = { 𝑟 ∈ NzRing ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) ) }
22 20 21 elrab2 ⊢ ( 𝑅 ∈ LRing ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )