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 E = RLReg R
rrgval.b B = Base R
rrgval.t · ˙ = R
rrgval.z 0 ˙ = 0 R
Assertion rrgval E = x B | y B x · ˙ y = 0 ˙ y = 0 ˙

Proof

Step Hyp Ref Expression
1 rrgval.e E = RLReg R
2 rrgval.b B = Base R
3 rrgval.t · ˙ = R
4 rrgval.z 0 ˙ = 0 R
5 fveq2 r = R Base r = Base R
6 5 2 eqtr4di r = R Base r = B
7 fveq2 r = R r = R
8 7 3 eqtr4di r = R r = · ˙
9 8 oveqd r = R x r y = x · ˙ y
10 fveq2 r = R 0 r = 0 R
11 10 4 eqtr4di r = R 0 r = 0 ˙
12 9 11 eqeq12d r = R x r y = 0 r x · ˙ y = 0 ˙
13 11 eqeq2d r = R y = 0 r y = 0 ˙
14 12 13 imbi12d r = R x r y = 0 r y = 0 r x · ˙ y = 0 ˙ y = 0 ˙
15 6 14 raleqbidv r = R y Base r x r y = 0 r y = 0 r y B x · ˙ y = 0 ˙ y = 0 ˙
16 6 15 rabeqbidv r = R x Base r | y Base r x r y = 0 r y = 0 r = x B | y B x · ˙ y = 0 ˙ y = 0 ˙
17 df-rlreg RLReg = r V x Base r | y Base r x r y = 0 r y = 0 r
18 2 fvexi B V
19 18 rabex x B | y B x · ˙ y = 0 ˙ y = 0 ˙ V
20 16 17 19 fvmpt R V RLReg R = x B | y B x · ˙ y = 0 ˙ y = 0 ˙
21 fvprc ¬ R V RLReg R =
22 fvprc ¬ R V Base R =
23 2 22 eqtrid ¬ R V B =
24 23 rabeqdv ¬ R V x B | y B x · ˙ y = 0 ˙ y = 0 ˙ = x | y B x · ˙ y = 0 ˙ y = 0 ˙
25 rab0 x | y B x · ˙ y = 0 ˙ y = 0 ˙ =
26 24 25 eqtrdi ¬ R V x B | y B x · ˙ y = 0 ˙ y = 0 ˙ =
27 21 26 eqtr4d ¬ R V RLReg R = x B | y B x · ˙ y = 0 ˙ y = 0 ˙
28 20 27 pm2.61i RLReg R = x B | y B x · ˙ y = 0 ˙ y = 0 ˙
29 1 28 eqtri E = x B | y B x · ˙ y = 0 ˙ y = 0 ˙