Theorem dchrmul

Description: Group operation on the group of Dirichlet characters. (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 )
	dchrmul.t	|- .x. = ( +g ` G )
	dchrmul.x	|- ( ph -> X e. D )
	dchrmul.y	|- ( ph -> Y e. D )
Assertion	dchrmul	|- ( ph -> ( X .x. Y ) = ( X oF x. Y ) )

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		dchrmul.t	|- .x. = ( +g ` G )
5		dchrmul.x	|- ( ph -> X e. D )
6		dchrmul.y	|- ( ph -> Y e. D )
7	1 3	dchrrcl	|- ( X e. D -> N e. NN )
8	5 7	syl	|- ( ph -> N e. NN )
9	1 2 3 4 8	dchrplusg	|- ( ph -> .x. = ( oF x. |` ( D X. D ) ) )
10	9	oveqd	|- ( ph -> ( X .x. Y ) = ( X ( oF x. |` ( D X. D ) ) Y ) )
11	5 6	ofmresval	|- ( ph -> ( X ( oF x. |` ( D X. D ) ) Y ) = ( X oF x. Y ) )
12	10 11	eqtrd	|- ( ph -> ( X .x. Y ) = ( X oF x. Y ) )