Theorem ruclem12 4896

Description: Lemma for ruc 4924. A helper lemma that changes bound variables.

Hypothesis

Ref	Expression
ruclem12.2	|- D = {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.))}

Assertion

Ref	Expression
ruclem12	|- D = {<.<.w, v>., u>. | ((w e. (RR X. RR) /\ v e. RR) /\ u = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.))}

Distinct variable group(s):   x,y,z,w,v,u

Proof of Theorem ruclem12

Step	Hyp	Ref	Expression
1		ruclem12.2	. 2 |- D = {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.))}
2		eleq1 1149	. . . . . 6 |- (x = w -> (x e. (RR X. RR) <-> w e. (RR X. RR)))
3	2	anbi1d 469	. . . . 5 |- (x = w -> ((x e. (RR X. RR) /\ y e. RR) <-> (w e. (RR X. RR) /\ y e. RR)))
4		eleq1 1149	. . . . . 6 |- (y = v -> (y e. RR <-> v e. RR))
5	4	anbi2d 468	. . . . 5 |- (y = v -> ((w e. (RR X. RR) /\ y e. RR) <-> (w e. (RR X. RR) /\ v e. RR)))
6	3, 5	sylan9bb 418	. . . 4 |- ((x = w /\ y = v) -> ((x e. (RR X. RR) /\ y e. RR) <-> (w e. (RR X. RR) /\ v e. RR)))
7		ruclem4 4888	. . . . 5 |- ((x = w /\ y = v) -> if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.) = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.))
8	7	cleq2d 1112	. . . 4 |- ((x = w /\ y = v) -> (z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.) <-> z = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.)))
9	6, 8	anbi12d 476	. . 3 |- ((x = w /\ y = v) -> (((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.)) <-> ((w e. (RR X. RR) /\ v e. RR) /\ z = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.))))
10	9	cbvoprab12v 3029	. 2 |- {<.<.x, y>., z>. | ((x e. (RR X. RR) /\ y e. RR) /\ z = if(((1st` x) < y /\ y < (2nd` x)), <.(((2 x. y) + (2nd` x)) / 3), ((y + (2 x. (2nd` x))) / 3)>., <.(((2 x. (1st` x)) + (2nd` x)) / 3), (((1st` x) + (2 x. (2nd` x))) / 3)>.))} = {<.<.w, v>., z>. | ((w e. (RR X. RR) /\ v e. RR) /\ z = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.))}
11		cleq1 1107	. . . 4 |- (z = u -> (z = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.) <-> u = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.)))
12	11	anbi2d 468	. . 3 |- (z = u -> (((w e. (RR X. RR) /\ v e. RR) /\ z = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.)) <-> ((w e. (RR X. RR) /\ v e. RR) /\ u = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.))))
13	12	cbvoprab3v 3030	. 2 |- {<.<.w, v>., z>. | ((w e. (RR X. RR) /\ v e. RR) /\ z = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.))} = {<.<.w, v>., u>. | ((w e. (RR X. RR) /\ v e. RR) /\ u = if(((1st` w) < v /\ v < (2nd` w)), <.(((2 x. v) + (2nd` w)) / 3), ((v + (