Theorem dchrinv 21006

Description: The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of X are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016.)

Hypotheses

Ref	Expression
dchrabs.g	|- G = (DChr ` N )
dchrabs.d	|- D = ( Base ` G )
dchrabs.x	|- ( ph -> X e. D )
dchrinv.i	|- I = ( inv g ` G )

Assertion

Ref	Expression
dchrinv	|- ( ph -> ( I ` X ) = ( * o. X ) )

Proof of Theorem dchrinv

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dchrabs.g	. . . . . . . 8 |- G = (DChr ` N )
2		eqid 2412	. . . . . . . 8 |- (ℤ/nℤ ` N ) = (ℤ/nℤ ` N )
3		dchrabs.d	. . . . . . . 8 |- D = ( Base ` G )
4		eqid 2412	. . . . . . . 8 |- ( +g ` G ) = ( +g ` G )
5		dchrabs.x	. . . . . . . 8 |- ( ph -> X e. D )
6		cjf 11872	. . . . . . . . . 10 |- * : CC --> CC
7		eqid 2412	. . . . . . . . . . 11 |- ( Base ` (ℤ/nℤ ` N ) ) = ( Base ` (ℤ/nℤ ` N ) )
8	1, 2, 3, 7, 5	dchrf 20987	. . . . . . . . . 10 |- ( ph -> X : ( Base ` (ℤ/nℤ ` N ) ) --> CC )
9		fco 5567	. . . . . . . . . 10 |- ( ( * : CC --> CC /\ X : ( Base ` (ℤ/nℤ ` N ) ) --> CC ) -> ( * o. X ) : ( Base ` (ℤ/nℤ ` N ) ) --> CC )
10	6, 8, 9	sylancr 645	. . . . . . . . 9 |- ( ph -> ( * o. X ) : ( Base ` (ℤ/nℤ ` N ) ) --> CC )
11		eqid 2412	. . . . . . . . . . . . . . . . . . . . 21 |- (Unit ` (ℤ/nℤ ` N ) ) = (Unit ` (ℤ/nℤ ` N ) )
12	1, 3	dchrrcl 20985	. . . . . . . . . . . . . . . . . . . . . 22 |- ( X e. D -> N e. NN )
13	5, 12	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> N e. NN )
14	1, 2, 7, 11, 13, 3	dchrelbas3 20983	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( X e. D <-> ( X : ( Base ` (ℤ/nℤ ` N ) ) --> CC /\ ( A. x e. (Unit ` (ℤ/nℤ ` N ) ) A. y e. (Unit ` (ℤ/nℤ ` N ) ) ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` (ℤ/nℤ ` N ) ) ) = 1 /\ A. x e. ( Base ` (ℤ/nℤ ` N ) ) ( ( X ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) ) ) ) )
15	5, 14	mpbid 202	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( X : ( Base ` (ℤ/nℤ ` N ) ) --> CC /\ ( A. x e. (Unit ` (ℤ/nℤ ` N ) ) A. y e. (Unit ` (ℤ/nℤ ` N ) ) ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` (ℤ/nℤ ` N ) ) ) = 1 /\ A. x e. ( Base ` (ℤ/nℤ ` N ) ) ( ( X ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) ) ) )
16	15	simprd 450	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( A. x e. (Unit ` (ℤ/nℤ ` N ) ) A. y e. (Unit ` (ℤ/nℤ ` N ) ) ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` (ℤ/nℤ ` N ) ) ) = 1 /\ A. x e. ( Base ` (ℤ/nℤ ` N ) ) ( ( X ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) ) )
17	16	simp1d 969	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. x e. (Unit ` (ℤ/nℤ ` N ) ) A. y e. (Unit ` (ℤ/nℤ ` N ) ) ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
18	17	r19.21bi 2772	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> A. y e. (Unit ` (ℤ/nℤ ` N ) ) ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
19	18	r19.21bi 2772	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
20	19	anasss 629	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
21	20	fveq2d 5699	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( * ` ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) ) = ( * ` ( ( X ` x ) x. ( X ` y ) ) ) )
22	8	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> X : ( Base ` (ℤ/nℤ ` N ) ) --> CC )
23	7, 11	unitss 15728	. . . . . . . . . . . . . . . 16 |- (Unit ` (ℤ/nℤ ` N ) ) C_ ( Base ` (ℤ/nℤ ` N ) )
24		simprl 733	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> x e. (Unit ` (ℤ/nℤ ` N ) ) )
25	23, 24	sseldi 3314	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> x e. ( Base ` (ℤ/nℤ ` N ) ) )
26	22, 25	ffvelrnd 5838	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( X ` x ) e. CC )
27		simprr 734	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> y e. (Unit ` (ℤ/nℤ ` N ) ) )
28	23, 27	sseldi 3314	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> y e. ( Base ` (ℤ/nℤ ` N ) ) )
29	22, 28	ffvelrnd 5838	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( X ` y ) e. CC )
30	26, 29	cjmuld 11989	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( * ` ( ( X ` x ) x. ( X ` y ) ) ) = ( ( * ` ( X ` x ) ) x. ( * ` ( X ` y ) ) ) )
31	21, 30	eqtrd 2444	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( * ` ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) ) = ( ( * ` ( X ` x ) ) x. ( * ` ( X ` y ) ) ) )
32	13	nnnn0d 10238	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. NN0 )
33	2	zncrng 16788	. . . . . . . . . . . . . . . 16 |- ( N e. NN0 -> (ℤ/nℤ ` N ) e. CRing )
34		crngrng 15637	. . . . . . . . . . . . . . . 16 |- ( (ℤ/nℤ ` N ) e. CRing -> (ℤ/nℤ ` N ) e. Ring )
35	32, 33, 34	3syl 19	. . . . . . . . . . . . . . 15 |- ( ph -> (ℤ/nℤ ` N ) e. Ring )
36	35	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> (ℤ/nℤ ` N ) e. Ring )
37		eqid 2412	. . . . . . . . . . . . . . 15 |- ( .r ` (ℤ/nℤ ` N ) ) = ( .r ` (ℤ/nℤ ` N ) )
38	7, 37	rngcl 15640	. . . . . . . . . . . . . 14 |- ( ( (ℤ/nℤ ` N ) e. Ring /\ x e. ( Base ` (ℤ/nℤ ` N ) ) /\ y e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( x ( .r ` (ℤ/nℤ ` N ) ) y ) e. ( Base ` (ℤ/nℤ ` N ) ) )
39	36, 25, 28, 38	syl3anc 1184	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( x ( .r ` (ℤ/nℤ ` N ) ) y ) e. ( Base ` (ℤ/nℤ ` N ) ) )
40		fvco3 5767	. . . . . . . . . . . . 13 |- ( ( X : ( Base ` (ℤ/nℤ ` N ) ) --> CC /\ ( x ( .r ` (ℤ/nℤ ` N ) ) y ) e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( ( * o. X ) ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( * ` ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) ) )
41	22, 39, 40	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( ( * o. X ) ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( * ` ( X ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) ) )
42		fvco3 5767	. . . . . . . . . . . . . 14 |- ( ( X : ( Base ` (ℤ/nℤ ` N ) ) --> CC /\ x e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( ( * o. X ) ` x ) = ( * ` ( X ` x ) ) )
43	22, 25, 42	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( ( * o. X ) ` x ) = ( * ` ( X ` x ) ) )
44		fvco3 5767	. . . . . . . . . . . . . 14 |- ( ( X : ( Base ` (ℤ/nℤ ` N ) ) --> CC /\ y e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( ( * o. X ) ` y ) = ( * ` ( X ` y ) ) )
45	22, 28, 44	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( ( * o. X ) ` y ) = ( * ` ( X ` y ) ) )
46	43, 45	oveq12d 6066	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( ( ( * o. X ) ` x ) x. ( ( * o. X ) ` y ) ) = ( ( * ` ( X ` x ) ) x. ( * ` ( X ` y ) ) ) )
47	31, 41, 46	3eqtr4d 2454	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. (Unit ` (ℤ/nℤ ` N ) ) /\ y e. (Unit ` (ℤ/nℤ ` N ) ) ) ) -> ( ( * o. X ) ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( ( * o. X ) ` x ) x. ( ( * o. X ) ` y ) ) )
48	47	ralrimivva 2766	. . . . . . . . . 10 |- ( ph -> A. x e. (Unit ` (ℤ/nℤ ` N ) ) A. y e. (Unit ` (ℤ/nℤ ` N ) ) ( ( * o. X ) ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( ( * o. X ) ` x ) x. ( ( * o. X ) ` y ) ) )
49		eqid 2412	. . . . . . . . . . . . . 14 |- ( 1r ` (ℤ/nℤ ` N ) ) = ( 1r ` (ℤ/nℤ ` N ) )
50	7, 49	rngidcl 15647	. . . . . . . . . . . . 13 |- ( (ℤ/nℤ ` N ) e. Ring -> ( 1r ` (ℤ/nℤ ` N ) ) e. ( Base ` (ℤ/nℤ ` N ) ) )
51	35, 50	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( 1r ` (ℤ/nℤ ` N ) ) e. ( Base ` (ℤ/nℤ ` N ) ) )
52		fvco3 5767	. . . . . . . . . . . 12 |- ( ( X : ( Base ` (ℤ/nℤ ` N ) ) --> CC /\ ( 1r ` (ℤ/nℤ ` N ) ) e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( ( * o. X ) ` ( 1r ` (ℤ/nℤ ` N ) ) ) = ( * ` ( X ` ( 1r ` (ℤ/nℤ ` N ) ) ) ) )
53	8, 51, 52	syl2anc 643	. . . . . . . . . . 11 |- ( ph -> ( ( * o. X ) ` ( 1r ` (ℤ/nℤ ` N ) ) ) = ( * ` ( X ` ( 1r ` (ℤ/nℤ ` N ) ) ) ) )
54	16	simp2d 970	. . . . . . . . . . . . 13 |- ( ph -> ( X ` ( 1r ` (ℤ/nℤ ` N ) ) ) = 1 )
55	54	fveq2d 5699	. . . . . . . . . . . 12 |- ( ph -> ( * ` ( X ` ( 1r ` (ℤ/nℤ ` N ) ) ) ) = ( * ` 1 ) )
56		1re 9054	. . . . . . . . . . . . 13 |- 1 e. RR
57		cjre 11907	. . . . . . . . . . . . 13 |- ( 1 e. RR -> ( * ` 1 ) = 1 )
58	56, 57	ax-mp 8	. . . . . . . . . . . 12 |- ( * ` 1 ) = 1
59	55, 58	syl6eq 2460	. . . . . . . . . . 11 |- ( ph -> ( * ` ( X ` ( 1r ` (ℤ/nℤ ` N ) ) ) ) = 1 )
60	53, 59	eqtrd 2444	. . . . . . . . . 10 |- ( ph -> ( ( * o. X ) ` ( 1r ` (ℤ/nℤ ` N ) ) ) = 1 )
61	16	simp3d 971	. . . . . . . . . . 11 |- ( ph -> A. x e. ( Base ` (ℤ/nℤ ` N ) ) ( ( X ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) )
62	8, 42	sylan 458	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( ( * o. X ) ` x ) = ( * ` ( X ` x ) ) )
63		cj0 11926	. . . . . . . . . . . . . . . . . 18 |- ( * ` 0 ) = 0
64	63	eqcomi 2416	. . . . . . . . . . . . . . . . 17 |- 0 = ( * ` 0 )
65	64	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( Base ` (ℤ/nℤ ` N ) ) ) -> 0 = ( * ` 0 ) )
66	62, 65	eqeq12d 2426	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( ( ( * o. X ) ` x ) = 0 <-> ( * ` ( X ` x ) ) = ( * ` 0 ) ) )
67	8	ffvelrnda 5837	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( X ` x ) e. CC )
68		0cn 9048	. . . . . . . . . . . . . . . 16 |- 0 e. CC
69		cj11 11930	. . . . . . . . . . . . . . . 16 |- ( ( ( X ` x ) e. CC /\ 0 e. CC ) -> ( ( * ` ( X ` x ) ) = ( * ` 0 ) <-> ( X ` x ) = 0 ) )
70	67, 68, 69	sylancl 644	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( ( * ` ( X ` x ) ) = ( * ` 0 ) <-> ( X ` x ) = 0 ) )
71	66, 70	bitrd 245	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( ( ( * o. X ) ` x ) = 0 <-> ( X ` x ) = 0 ) )
72	71	necon3bid 2610	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( ( ( * o. X ) ` x ) =/= 0 <-> ( X ` x ) =/= 0 ) )
73	72	imbi1d 309	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( Base ` (ℤ/nℤ ` N ) ) ) -> ( ( ( ( * o. X ) ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) <-> ( ( X ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) ) )
74	73	ralbidva 2690	. . . . . . . . . . 11 |- ( ph -> ( A. x e. ( Base ` (ℤ/nℤ ` N ) ) ( ( ( * o. X ) ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) <-> A. x e. ( Base ` (ℤ/nℤ ` N ) ) ( ( X ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) ) )
75	61, 74	mpbird 224	. . . . . . . . . 10 |- ( ph -> A. x e. ( Base ` (ℤ/nℤ ` N ) ) ( ( ( * o. X ) ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) )
76	48, 60, 75	3jca 1134	. . . . . . . . 9 |- ( ph -> ( A. x e. (Unit ` (ℤ/nℤ ` N ) ) A. y e. (Unit ` (ℤ/nℤ ` N ) ) ( ( * o. X ) ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( ( * o. X ) ` x ) x. ( ( * o. X ) ` y ) ) /\ ( ( * o. X ) ` ( 1r ` (ℤ/nℤ ` N ) ) ) = 1 /\ A. x e. ( Base ` (ℤ/nℤ ` N ) ) ( ( ( * o. X ) ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) ) )
77	1, 2, 7, 11, 13, 3	dchrelbas3 20983	. . . . . . . . 9 |- ( ph -> ( ( * o. X ) e. D <-> ( ( * o. X ) : ( Base ` (ℤ/nℤ ` N ) ) --> CC /\ ( A. x e. (Unit ` (ℤ/nℤ ` N ) ) A. y e. (Unit ` (ℤ/nℤ ` N ) ) ( ( * o. X ) ` ( x ( .r ` (ℤ/nℤ ` N ) ) y ) ) = ( ( ( * o. X ) ` x ) x. ( ( * o. X ) ` y ) ) /\ ( ( * o. X ) ` ( 1r ` (ℤ/nℤ ` N ) ) ) = 1 /\ A. x e. ( Base ` (ℤ/nℤ ` N ) ) ( ( ( * o. X ) ` x ) =/= 0 -> x e. (Unit ` (ℤ/nℤ ` N ) ) ) ) ) ) )
78	10, 76, 77	mpbir2and 889	. . . . . . . 8 |- ( ph -> ( * o. X ) e. D )
79	1, 2, 3, 4, 5, 78	dchrmul 20993	. . . . . . 7 |- ( ph -> ( X ( +g ` G ) ( * o. X ) ) = ( X o F x. ( * o. X ) ) )
80	79	adantr 452	. . . . . 6 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( X ( +g ` G ) ( * o. X ) ) = ( X o F x. ( * o. X ) ) )
81	80	fveq1d 5697	. . . . 5 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( X ( +g ` G ) ( * o. X ) ) ` x ) = ( ( X o F x. ( * o. X ) ) ` x ) )
82	23	sseli 3312	. . . . . . . . 9 |- ( x e. (Unit ` (ℤ/nℤ ` N ) ) -> x e. ( Base ` (ℤ/nℤ ` N ) ) )
83	82, 62	sylan2 461	. . . . . . . 8 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( * o. X ) ` x ) = ( * ` ( X ` x ) ) )
84	83	oveq2d 6064	. . . . . . 7 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( X ` x ) x. ( ( * o. X ) ` x ) ) = ( ( X ` x ) x. ( * ` ( X ` x ) ) ) )
85	82, 67	sylan2 461	. . . . . . . 8 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( X ` x ) e. CC )
86	85	absvalsqd 12207	. . . . . . 7 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( abs ` ( X ` x ) ) ^ 2 ) = ( ( X ` x ) x. ( * ` ( X ` x ) ) ) )
87	5	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> X e. D )
88		simpr 448	. . . . . . . . . 10 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> x e. (Unit ` (ℤ/nℤ ` N ) ) )
89	1, 3, 87, 2, 11, 88	dchrabs 21005	. . . . . . . . 9 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( abs ` ( X ` x ) ) = 1 )
90	89	oveq1d 6063	. . . . . . . 8 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( abs ` ( X ` x ) ) ^ 2 ) = ( 1 ^ 2 ) )
91		sq1 11439	. . . . . . . 8 |- ( 1 ^ 2 ) = 1
92	90, 91	syl6eq 2460	. . . . . . 7 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( abs ` ( X ` x ) ) ^ 2 ) = 1 )
93	84, 86, 92	3eqtr2d 2450	. . . . . 6 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( X ` x ) x. ( ( * o. X ) ` x ) ) = 1 )
94	8	adantr 452	. . . . . . . 8 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> X : ( Base ` (ℤ/nℤ ` N ) ) --> CC )
95		ffn 5558	. . . . . . . 8 |- ( X : ( Base ` (ℤ/nℤ ` N ) ) --> CC -> X Fn ( Base ` (ℤ/nℤ ` N ) ) )
96	94, 95	syl 16	. . . . . . 7 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> X Fn ( Base ` (ℤ/nℤ ` N ) ) )
97		ffn 5558	. . . . . . . . 9 |- ( ( * o. X ) : ( Base ` (ℤ/nℤ ` N ) ) --> CC -> ( * o. X ) Fn ( Base ` (ℤ/nℤ ` N ) ) )
98	10, 97	syl 16	. . . . . . . 8 |- ( ph -> ( * o. X ) Fn ( Base ` (ℤ/nℤ ` N ) ) )
99	98	adantr 452	. . . . . . 7 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( * o. X ) Fn ( Base ` (ℤ/nℤ ` N ) ) )
100		fvex 5709	. . . . . . . 8 |- ( Base ` (ℤ/nℤ ` N ) ) e. _V
101	100	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( Base ` (ℤ/nℤ ` N ) ) e. _V )
102	82	adantl 453	. . . . . . 7 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> x e. ( Base ` (ℤ/nℤ ` N ) ) )
103		fnfvof 6284	. . . . . . 7 |- ( ( ( X Fn ( Base ` (ℤ/nℤ ` N ) ) /\ ( * o. X ) Fn ( Base ` (ℤ/nℤ ` N ) ) ) /\ ( ( Base ` (ℤ/nℤ ` N ) ) e. _V /\ x e. ( Base ` (ℤ/nℤ ` N ) ) ) ) -> ( ( X o F x. ( * o. X ) ) ` x ) = ( ( X ` x ) x. ( ( * o. X ) ` x ) ) )
104	96, 99, 101, 102, 103	syl22anc 1185	. . . . . 6 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( X o F x. ( * o. X ) ) ` x ) = ( ( X ` x ) x. ( ( * o. X ) ` x ) ) )
105		eqid 2412	. . . . . . 7 |- ( 0g ` G ) = ( 0g ` G )
106	13	adantr 452	. . . . . . 7 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> N e. NN )
107	1, 2, 105, 11, 106, 88	dchr1 21002	. . . . . 6 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( 0g ` G ) ` x ) = 1 )
108	93, 104, 107	3eqtr4d 2454	. . . . 5 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( X o F x. ( * o. X ) ) ` x ) = ( ( 0g ` G ) ` x ) )
109	81, 108	eqtrd 2444	. . . 4 |- ( ( ph /\ x e. (Unit ` (ℤ/nℤ ` N ) ) ) -> ( ( X ( +g ` G ) ( * o. X ) ) ` x ) = ( ( 0g ` G ) ` x ) )
110	109	ralrimiva 2757	. . 3 |- ( ph -> A. x e. (Unit ` (ℤ/nℤ ` N ) ) ( ( X ( +g ` G ) ( * o. X ) ) ` x ) = ( ( 0g ` G ) ` x ) )
111	1, 2, 3, 4, 5, 78	dchrmulcl 20994	. . . 4 |- ( ph -> ( X ( +g ` G ) ( * o. X ) ) e. D )
112	1	dchrabl 20999	. . . . . 6 |- ( N e. NN -> G e. Abel )
113		ablgrp 15380	. . . . . 6 |- ( G e. Abel -> G e. Grp )
114	13, 112, 113	3syl 19	. . . . 5 |- ( ph -> G e. Grp )
115	3, 105	grpidcl 14796	. . . . 5 |- ( G e. Grp -> ( 0g ` G ) e. D )
116	114, 115	syl 16	. . . 4 |- ( ph -> ( 0g ` G ) e. D )
117	1, 2, 3, 11, 111, 116	dchreq 21003	. . 3 |- ( ph -> ( ( X ( +g ` G ) ( * o. X ) ) = ( 0g ` G ) <-> A. x e. (Unit ` (ℤ/nℤ ` N ) ) ( ( X ( +g ` G ) ( * o. X ) ) ` x ) = ( ( 0g ` G ) ` x ) ) )
118	110, 117	mpbird 224	. 2 |- ( ph -> ( X ( +g ` G ) ( * o. X ) ) = ( 0g ` G ) )
119		dchrinv.i	. . . 4 |- I = ( inv g ` G )
120	3, 4, 105, 119	grpinvid1 14816	. . 3 |- ( ( G e. Grp /\ X e. D /\ ( * o. X ) e. D ) -> ( ( I ` X ) = ( * o. X ) <-> ( X ( +g ` G ) ( * o. X ) ) = ( 0g ` G ) ) )
121	114, 5, 78, 120	syl3anc 1184	. 2 |- ( ph -> ( ( I ` X ) = ( * o. X ) <-> ( X ( +g ` G ) ( * o. X ) ) = ( 0g ` G ) ) )
122	118, 121	mpbird 224	1 |- ( ph -> ( I ` X ) = ( * o. X ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2575   A.wral 2674   _Vcvv 2924   o. ccom 4849   Fn wfn 5416   -->wf 5417   ` cfv 5421  (class class class)co 6048   o Fcof 6270   CCcc 8952   RRcr 8953   0cc0 8954   1c1 8955   x. cmul 8959   NNcn 9964   2c2 10013   NN0cn0 10185   ^cexp 11345   *ccj 11864   abscabs 12002   Basecbs 13432   +g cplusg 13492   .rcmulr 13493   0gc0g 13686   Grpcgrp 14648   inv gcminusg 14649   Abelcabel 15376   Ringcrg 15623   CRingccrg 15624   1rcur 15625  Unitcui 15707  ℤ/nℤczn 16744  DChrcdchr 20977

This theorem is referenced by:  dchr2sum  21018  dchrisum0re  21168

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-inf2 7560  ax-cnex 9010  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-mulcom 9018  ax-addass 9019  ax-mulass 9020  ax-distr 9021  ax-i2m1 9022  ax-1ne0 9023  ax-1rid 9024  ax-rnegex 9025  ax-rrecex 9026  ax-cnre 9027  ax-pre-lttri 9028  ax-pre-lttrn 9029  ax-pre-ltadd 9030  ax-pre-mulgt0 9031  ax-pre-sup 9032  ax-addf 9033  ax-mulf 9034

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-int 4019  df-iun 4063  df-iin 4064  df-disj 4151  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-se 4510  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-of 6272  df-1st 6316  df-2nd 6317  df-tpos 6446  df-riota 6516  df-recs 6600  df-rdg 6635  df-1o 6691  df-2o 6692  df-oadd 6695  df-omul 6696  df-er 6872  df-ec 6874  df-qs 6878  df-map 6987  df-pm 6988  df-ixp 7031  df-en 7077  df-dom 7078  df-sdom 7079  df-fin 7080  df-fi 7382  df-sup 7412  df-oi 7443  df-card 7790  df-acn 7793  df-cda 8012  df-pnf 9086  df-mnf 9087  df-xr 9088  df-ltxr 9089  df-le 9090  df-sub 9257  df-neg 9258  df-div 9642  df-nn 9965  df-2 10022  df-3 10023  df-4 10024  df-5 10025  df-6 10026  df-7 10027  df-8 10028  df-9 10029  df-10 10030  df-n0 10186  df-z 10247  df-dec 10347  df-uz 10453  df-q 10539  df-rp 10577  df-xneg 10674  df-xadd 10675  df-xmul 10676  df-ioo 10884  df-ioc 10885  df-ico 10886  df-icc 10887  df-fz 11008  df-fzo 11099  df-fl 11165  df-mod 11214  df-seq 11287  df-exp 11346  df-fac 11530  df-bc 11557  df-hash 11582  df-shft 11845  df-cj 11867  df-re 11868  df-im 11869  df-sqr 12003  df-abs 12004  df-limsup 12228  df-clim 12245  df-rlim 12246  df-sum 12443  df-ef 12633  df-sin 12635  df-cos 12636  df-pi 12638  df-dvds 12816  df-struct 13434  df-ndx 13435  df-slot 13436  df-base 13437  df-sets 13438  df-ress 13439  df-plusg 13505  df-mulr 13506  df-starv 13507  df-sca 13508  df-vsca 13509  df-tset 13511  df-ple 13512  df-ds 13514  df-unif 13515  df-hom 13516  df-cco 13517  df-rest 13613  df-topn 13614  df-topgen 13630  df-pt 13631  df-prds 13634  df-xrs 13689  df-0g 13690  df-gsum 13691  df-qtop 13696  df-imas 13697  df-divs 13698  df-xps 13699  df-mre 13774  df-mrc 13775  df-acs 13777  df-mnd 14653  df-mhm 14701  df-submnd 14702  df-grp 14775  df-minusg 14776  df-sbg 14777  df-mulg 14778  df-subg 14904  df-nsg 14905  df-eqg 14906  df-ghm 14967  df-cntz 15079  df-od 15130  df-cmn 15377  df-abl 15378  df-mgp 15612  df-rng 15626  df-cring 15627  df-ur 15628  df-oppr 15691  df-dvdsr 15709  df-unit 15710  df-invr 15740  df-dvr 15751  df-rnghom 15782  df-drng 15800  df-subrg 15829  df-lmod 15915  df-lss 15972  df-lsp 16011  df-sra 16207  df-rgmod 16208  df-lidl 16209  df-rsp 16210  df-2idl 16266  df-psmet 16657  df-xmet 16658  df-met 16659  df-bl 16660  df-mopn 16661  df-fbas 16662  df-fg 16663  df-cnfld 16667  df-zrh 16745  df-zn 16748  df-top 16926  df-bases 16928  df-topon 16929  df-topsp 16930  df-cld 17046  df-ntr 17047  df-cls 17048  df-nei 17125  df-lp 17163  df-perf 17164  df-cn 17253  df-cnp 17254  df-haus 17341  df-tx 17555  df-hmeo 17748  df-fil 17839  df-fm 17931  df-flim 17932  df-flf 17933  df-xms 18311  df-ms 18312  df-tms 18313  df-cncf 18869  df-limc 19714  df-dv 19715  df-log 20415  df-cxp 20416  df-dchr 20978