Theorem dchr1cl

Description: Closure of the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	dchrmhm.g	|- G = ( DChr ` N )
	dchrmhm.z	|- Z = ( Z/nZ ` N )
	dchrmhm.b	|- D = ( Base ` G )
	dchrn0.b	|- B = ( Base ` Z )
	dchrn0.u	|- U = ( Unit ` Z )
	dchr1cl.o	|- .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) )
	dchr1cl.n	|- ( ph -> N e. NN )
Assertion	dchr1cl	|- ( ph -> .1. e. D )

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	|- G = ( DChr ` N )
2		dchrmhm.z	|- Z = ( Z/nZ ` N )
3		dchrmhm.b	|- D = ( Base ` G )
4		dchrn0.b	|- B = ( Base ` Z )
5		dchrn0.u	|- U = ( Unit ` Z )
6		dchr1cl.o	|- .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) )
7		dchr1cl.n	|- ( ph -> N e. NN )
8		eqidd	|- ( k = x -> 1 = 1 )
9		eqidd	|- ( k = y -> 1 = 1 )
10		eqidd	|- ( k = ( x ( .r ` Z ) y ) -> 1 = 1 )
11		eqidd	|- ( k = ( 1r ` Z ) -> 1 = 1 )
12		1cnd	|- ( ( ph /\ k e. U ) -> 1 e. CC )
13		1t1e1	|- ( 1 x. 1 ) = 1
14	13	eqcomi	|- 1 = ( 1 x. 1 )
15	14	a1i	|- ( ( ph /\ ( x e. U /\ y e. U ) ) -> 1 = ( 1 x. 1 ) )
16		eqidd	|- ( ph -> 1 = 1 )
17	1 2 4 5 7 3 8 9 10 11 12 15 16	dchrelbasd	|- ( ph -> ( k e. B |-> if ( k e. U , 1 , 0 ) ) e. D )
18	6 17	eqeltrid	|- ( ph -> .1. e. D )