Theorem icoshftf1olem 6410

Description: Lemma for icoshftf1o 6411.

Hypotheses

Ref	Expression
icoshftf1o.1	|- F = {<.x, y>. | (x e. (A[,)B) /\ y = (x + C))}
icoshftf1olem.1	|- G = {<.x, y>. | (x e. (if(A e. RR, A, 0)[,)if(B e. RR, B, 0)) /\ y = (x + if(C e. RR, C, 0)))}

Assertion

Ref	Expression
icoshftf1olem	|- ((A e. RR /\ B e. RR /\ C e. RR) -> F:(A[,)B)-1-1-onto->((A + C)[,)(B + C)))

Distinct variable groups:   x,A,y   x,B,y   x,C,y

Proof of Theorem icoshftf1olem

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . . 5 |- (A = if(A e. RR, A, 0) -> (A[,)B) = (if(A e. RR, A, 0)[,)B))
2		f1oeq2 3685	. . . . 5 |- ((A[,)B) = (if(A e. RR, A, 0)[,)B) -> (G:(A[,)B)-1-1-onto->((A + C)[,)(B + C)) <-> G:(if(A e. RR, A, 0)[,)B)-1-1-onto->((A + C)[,)(B + C))))
3	1, 2	syl 10	. . . 4 |- (A = if(A e. RR, A, 0) -> (G:(A[,)B)-1-1-onto->((A + C)[,)(B + C)) <-> G:(if(A e. RR, A, 0)[,)B)-1-1-onto->((A + C)[,)(B + C))))
4		opreq1 3968	. . . . . 6 |- (A = if(A e. RR, A, 0) -> (A + C) = (if(A e. RR, A, 0) + C))
5	4	opreq1d 3975	. . . . 5 |- (A = if(A e. RR, A, 0) -> ((A + C)[,)(B + C)) = ((if(A e. RR, A, 0) + C)[,)(B + C)))
6		f1oeq3 3686	. . . . 5 |- (((A + C)[,)(B + C)) = ((if(A e. RR, A, 0) + C)[,)(B + C)) -> (G:(if(A e. RR, A, 0)[,)B)-1-1-onto->((A + C)[,)(B + C)) <-> G:(if(A e. RR, A, 0)[,)B)-1-1-onto->((if(A e. RR, A, 0) + C)[,)(B + C))))
7	5, 6	syl 10	. . . 4 |- (A = if(A e. RR, A, 0) -> (G:(if(A e. RR, A, 0)[,)B)-1-1-onto->((A + C)[,)(B + C)) <-> G:(if(A e. RR, A, 0)[,)B)-1-1-onto->((if(A e. RR, A, 0) + C)[,)(B + C))))
8	3, 7	bitrd 528	. . 3 |- (A = if(A e. RR, A, 0) -> (G:(A[,)B)-1-1-onto->((A + C)[,)(B + C)) <-> G:(if(A e. RR, A, 0)[,)B)-1-1-onto->((if(A e. RR, A, 0) + C)[,)(B + C))))
9		opreq2 3969	. . . . 5 |- (B = if(B e. RR, B, 0) -> (if(A e. RR, A, 0)[,)B) = (if(A e. RR, A, 0)[,)if(B e. RR, B, 0)))
10		f1oeq2 3685	. . . . 5 |- ((if(A e. RR, A, 0)[,)B) = (if(A e. RR, A, 0)[,)if(B e. RR, B, 0)) -> (G:(if(A e. RR, A, 0)[,)B)-1-1-onto->((if(A e. RR, A, 0) + C)[,)(B + C)) <-> G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + C)[,)(B + C))))
11	9, 10	syl 10	. . . 4 |- (B = if(B e. RR, B, 0) -> (G:(if(A e. RR, A, 0)[,)B)-1-1-onto->((if(A e. RR, A, 0) + C)[,)(B + C)) <-> G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + C)[,)(B + C))))
12		opreq1 3968	. . . . . 6 |- (B = if(B e. RR, B, 0) -> (B + C) = (if(B e. RR, B, 0) + C))
13	12	opreq2d 3976	. . . . 5 |- (B = if(B e. RR, B, 0) -> ((if(A e. RR, A, 0) + C)[,)(B + C)) = ((if(A e. RR, A, 0) + C)[,)(if(B e. RR, B, 0) + C)))
14		f1oeq3 3686	. . . . 5 |- (((if(A e. RR, A, 0) + C)[,)(B + C)) = ((if(A e. RR, A, 0) + C)[,)(if(B e. RR, B, 0) + C)) -> (G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + C)[,)(B + C)) <-> G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + C)[,)(if(B e. RR, B, 0) + C))))
15	13, 14	syl 10	. . . 4 |- (B = if(B e. RR, B, 0) -> (G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + C)[,)(B + C)) <-> G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + C)[,)(if(B e. RR, B, 0) + C))))
16	11, 15	bitrd 528	. . 3 |- (B = if(B e. RR, B, 0) -> (G:(if(A e. RR, A, 0)[,)B)-1-1-onto->((if(A e. RR, A, 0) + C)[,)(B + C)) <-> G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + C)[,)(if(B e. RR, B, 0) + C))))
17		opreq2 3969	. . . . 5 |- (C = if(C e. RR, C, 0) -> (if(A e. RR, A, 0) + C) = (if(A e. RR, A, 0) + if(C e. RR, C, 0)))
18		opreq2 3969	. . . . 5 |- (C = if(C e. RR, C, 0) -> (if(B e. RR, B, 0) + C) = (if(B e. RR, B, 0) + if(C e. RR, C, 0)))
19	17, 18	opreq12d 3978	. . . 4 |- (C = if(C e. RR, C, 0) -> ((if(A e. RR, A, 0) + C)[,)(if(B e. RR, B, 0) + C)) = ((if(A e. RR, A, 0) + if(C e. RR, C, 0))[,)(if(B e. RR, B, 0) + if(C e. RR, C, 0))))
20		f1oeq3 3686	. . . 4 |- (((if(A e. RR, A, 0) + C)[,)(if(B e. RR, B, 0) + C)) = ((if(A e. RR, A, 0) + if(C e. RR, C, 0))[,)(if(B e. RR, B, 0) + if(C e. RR, C, 0))) -> (G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + C)[,)(if(B e. RR, B, 0) + C)) <-> G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + if(C e. RR, C, 0))[,)(if(B e. RR, B, 0) + if(C e. RR, C, 0)))))
21	19, 20	syl 10	. . 3 |- (C = if(C e. RR, C, 0) -> (G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + C)[,)(if(B e. RR, B, 0) + C)) <-> G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + if(C e. RR, C, 0))[,)(if(B e. RR, B, 0) + if(C e. RR, C, 0)))))
22		icoshftf1olem.1	. . . 4 |- G = {<.x, y>. | (x e. (if(A e. RR, A, 0)[,)if(B e. RR, B, 0)) /\ y = (x + if(C e. RR, C, 0)))}
23		0re 5440	. . . . 5 |- 0 e. RR
24	23	elimel 2394	. . . 4 |- if(A e. RR, A, 0) e. RR
25	23	elimel 2394	. . . 4 |- if(B e. RR, B, 0) e. RR
26	23	elimel 2394	. . . 4 |- if(C e. RR, C, 0) e. RR
27	22, 24, 25, 26	icoshftf1oi 6409	. . 3 |- G:(if(A e. RR, A, 0)[,)if(B e. RR, B, 0))-1-1-onto->((if(A e. RR, A, 0) + if(C e. RR, C, 0))[,)(if(B e. RR, B, 0) + if(C e. RR, C,