Theorem oddpwdcv

Description: Lemma for eulerpart : value of the F function. (Contributed by Thierry Arnoux, 9-Sep-2017)

	Ref	Expression
Hypotheses	oddpwdc.j	|- J = { z e. NN | -. 2 || z }
	oddpwdc.f	|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
Assertion	oddpwdcv	|- ( W e. ( J X. NN0 ) -> ( F ` W ) = ( ( 2 ^ ( 2nd ` W ) ) x. ( 1st ` W ) ) )

Proof

Step	Hyp	Ref	Expression
1		oddpwdc.j	|- J = { z e. NN | -. 2 || z }
2		oddpwdc.f	|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
3		1st2nd2	|- ( W e. ( J X. NN0 ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
4	3	fveq2d	|- ( W e. ( J X. NN0 ) -> ( F ` W ) = ( F ` <. ( 1st ` W ) , ( 2nd ` W ) >. ) )
5		df-ov	|- ( ( 1st ` W ) F ( 2nd ` W ) ) = ( F ` <. ( 1st ` W ) , ( 2nd ` W ) >. )
6	5	a1i	|- ( W e. ( J X. NN0 ) -> ( ( 1st ` W ) F ( 2nd ` W ) ) = ( F ` <. ( 1st ` W ) , ( 2nd ` W ) >. ) )
7		elxp6	|- ( W e. ( J X. NN0 ) <-> ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. /\ ( ( 1st ` W ) e. J /\ ( 2nd ` W ) e. NN0 ) ) )
8	7	simprbi	|- ( W e. ( J X. NN0 ) -> ( ( 1st ` W ) e. J /\ ( 2nd ` W ) e. NN0 ) )
9		oveq2	|- ( x = ( 1st ` W ) -> ( ( 2 ^ y ) x. x ) = ( ( 2 ^ y ) x. ( 1st ` W ) ) )
10		oveq2	|- ( y = ( 2nd ` W ) -> ( 2 ^ y ) = ( 2 ^ ( 2nd ` W ) ) )
11	10	oveq1d	|- ( y = ( 2nd ` W ) -> ( ( 2 ^ y ) x. ( 1st ` W ) ) = ( ( 2 ^ ( 2nd ` W ) ) x. ( 1st ` W ) ) )
12		ovex	|- ( ( 2 ^ ( 2nd ` W ) ) x. ( 1st ` W ) ) e. _V
13	9 11 2 12	ovmpo	|- ( ( ( 1st ` W ) e. J /\ ( 2nd ` W ) e. NN0 ) -> ( ( 1st ` W ) F ( 2nd ` W ) ) = ( ( 2 ^ ( 2nd ` W ) ) x. ( 1st ` W ) ) )
14	8 13	syl	|- ( W e. ( J X. NN0 ) -> ( ( 1st ` W ) F ( 2nd ` W ) ) = ( ( 2 ^ ( 2nd ` W ) ) x. ( 1st ` W ) ) )
15	4 6 14	3eqtr2d	|- ( W e. ( J X. NN0 ) -> ( F ` W ) = ( ( 2 ^ ( 2nd ` W ) ) x. ( 1st ` W ) ) )