Theorem 2sqlem1

Description: Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015)

	Ref	Expression
Hypothesis	2sq.1	|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
Assertion	2sqlem1	|- ( A e. S <-> E. x e. Z[i] A = ( ( abs ` x ) ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2sq.1	|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2	1	eleq2i	|- ( A e. S <-> A e. ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) ) )
3		fveq2	|- ( w = x -> ( abs ` w ) = ( abs ` x ) )
4	3	oveq1d	|- ( w = x -> ( ( abs ` w ) ^ 2 ) = ( ( abs ` x ) ^ 2 ) )
5	4	cbvmptv	|- ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) ) = ( x e. Z[i] |-> ( ( abs ` x ) ^ 2 ) )
6		ovex	|- ( ( abs ` x ) ^ 2 ) e. _V
7	5 6	elrnmpti	|- ( A e. ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) ) <-> E. x e. Z[i] A = ( ( abs ` x ) ^ 2 ) )
8	2 7	bitri	|- ( A e. S <-> E. x e. Z[i] A = ( ( abs ` x ) ^ 2 ) )