Theorem ruclem12 7521

Description: Lemma for ruc 7549. 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:   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 1534	. . . . 5 |- (x = w -> (x e. (RR X. RR) <-> w e. (RR X. RR)))
3		eleq1 1534	. . . . 5 |- (y = v -> (y e. RR <-> v e. RR))
4	2, 3	bi2anan9 632	. . . 4 |- ((x = w /\ y = v) -> ((x e. (RR X. RR) /\ y e. RR) <-> (w e. (RR X. RR) /\ v e. RR)))
5		ruclem4 7513	. . . . 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)>.))
6	5	eqeq2d 1486	. . . 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)>.)))
7	4, 6	anbi12d 628	. . 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)>.))))
8	7	cbvoprab12v 3999	. 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)>.))}
9		eqeq1 1481	. . . 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)>.)))
10	9	anbi2d 616	. . 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)>.))))
11	10	cbvoprab3v 4000	. 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 + (2 x. (2nd` w))) / 3)>., <.(((2 x. (1st` w)) + (2nd` w)) / 3), (((1st` w) + (2 x. (2nd` w))) / 3)>.))}
12	1, 8, 11	3eqtr