Metamath Proof Explorer

Theorem rrgval

Description: Value of the set or left-regular elements in a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

Ref Expression
Hypotheses rrgval.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
rrgval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rrgval.t ⊢ · = ( .r ‘ 𝑅 )
rrgval.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion rrgval 𝐸 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) }

Proof

Step Hyp Ref Expression
1 rrgval.e ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
2 rrgval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 rrgval.t ⊢ · = ( .r ‘ 𝑅 )
4 rrgval.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
6 5 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
7 fveq2 ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
8 7 3 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = · )
9 8 oveqd ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
10 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
11 10 4 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
12 9 11 eqeq12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 ) ↔ ( 𝑥 · 𝑦 ) = 0 ) )
13 11 eqeq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑦 = ( 0g ‘ 𝑟 ) ↔ 𝑦 = 0 ) )
14 12 13 imbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 ) → 𝑦 = ( 0g ‘ 𝑟 ) ) ↔ ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) ) )
15 6 14 raleqbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 ) → 𝑦 = ( 0g ‘ 𝑟 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) ) )
16 6 15 rabeqbidv ⊢ ( 𝑟 = 𝑅 → { 𝑥 ∈ ( Base ‘ 𝑟 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 ) → 𝑦 = ( 0g ‘ 𝑟 ) ) } = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) } )
17 df-rlreg ⊢ RLReg = ( 𝑟 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑟 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 ) → 𝑦 = ( 0g ‘ 𝑟 ) ) } )
18 2 fvexi ⊢ 𝐵 ∈ V
19 18 rabex ⊢ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) } ∈ V
20 16 17 19 fvmpt ⊢ ( 𝑅 ∈ V → ( RLReg ‘ 𝑅 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) } )
21 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( RLReg ‘ 𝑅 ) = ∅ )
22 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝑅 ) = ∅ )
23 2 22 eqtrid ⊢ ( ¬ 𝑅 ∈ V → 𝐵 = ∅ )
24 23 rabeqdv ⊢ ( ¬ 𝑅 ∈ V → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) } = { 𝑥 ∈ ∅ ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) } )
25 rab0 ⊢ { 𝑥 ∈ ∅ ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) } = ∅
26 24 25 eqtrdi ⊢ ( ¬ 𝑅 ∈ V → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) } = ∅ )
27 21 26 eqtr4d ⊢ ( ¬ 𝑅 ∈ V → ( RLReg ‘ 𝑅 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) } )
28 20 27 pm2.61i ⊢ ( RLReg ‘ 𝑅 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) }
29 1 28 eqtri ⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → 𝑦 = 0 ) }