Metamath Proof Explorer


Theorem dchrmullid

Description: Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g โŠข ๐บ = ( DChr โ€˜ ๐‘ )
dchrmhm.z โŠข ๐‘ = ( โ„ค/nโ„ค โ€˜ ๐‘ )
dchrmhm.b โŠข ๐ท = ( Base โ€˜ ๐บ )
dchrn0.b โŠข ๐ต = ( Base โ€˜ ๐‘ )
dchrn0.u โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘ )
dchr1cl.o โŠข 1 = ( ๐‘˜ โˆˆ ๐ต โ†ฆ if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) )
dchrmullid.t โŠข ยท = ( +g โ€˜ ๐บ )
dchrmullid.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ท )
Assertion dchrmullid ( ๐œ‘ โ†’ ( 1 ยท ๐‘‹ ) = ๐‘‹ )

Proof

Step Hyp Ref Expression
1 dchrmhm.g โŠข ๐บ = ( DChr โ€˜ ๐‘ )
2 dchrmhm.z โŠข ๐‘ = ( โ„ค/nโ„ค โ€˜ ๐‘ )
3 dchrmhm.b โŠข ๐ท = ( Base โ€˜ ๐บ )
4 dchrn0.b โŠข ๐ต = ( Base โ€˜ ๐‘ )
5 dchrn0.u โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘ )
6 dchr1cl.o โŠข 1 = ( ๐‘˜ โˆˆ ๐ต โ†ฆ if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) )
7 dchrmullid.t โŠข ยท = ( +g โ€˜ ๐บ )
8 dchrmullid.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ท )
9 1 3 dchrrcl โŠข ( ๐‘‹ โˆˆ ๐ท โ†’ ๐‘ โˆˆ โ„• )
10 8 9 syl โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
11 1 2 3 4 5 6 10 dchr1cl โŠข ( ๐œ‘ โ†’ 1 โˆˆ ๐ท )
12 1 2 3 7 11 8 dchrmul โŠข ( ๐œ‘ โ†’ ( 1 ยท ๐‘‹ ) = ( 1 โˆ˜f ยท ๐‘‹ ) )
13 oveq1 โŠข ( 1 = if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) โ†’ ( 1 ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) = ( if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) )
14 13 eqeq1d โŠข ( 1 = if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) โ†’ ( ( 1 ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) = ( ๐‘‹ โ€˜ ๐‘˜ ) โ†” ( if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) = ( ๐‘‹ โ€˜ ๐‘˜ ) ) )
15 oveq1 โŠข ( 0 = if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) โ†’ ( 0 ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) = ( if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) )
16 15 eqeq1d โŠข ( 0 = if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) โ†’ ( ( 0 ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) = ( ๐‘‹ โ€˜ ๐‘˜ ) โ†” ( if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) = ( ๐‘‹ โ€˜ ๐‘˜ ) ) )
17 1 2 3 4 8 dchrf โŠข ( ๐œ‘ โ†’ ๐‘‹ : ๐ต โŸถ โ„‚ )
18 17 ffvelcdmda โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ต ) โ†’ ( ๐‘‹ โ€˜ ๐‘˜ ) โˆˆ โ„‚ )
19 18 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ต ) โˆง ๐‘˜ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘‹ โ€˜ ๐‘˜ ) โˆˆ โ„‚ )
20 19 mullidd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ต ) โˆง ๐‘˜ โˆˆ ๐‘ˆ ) โ†’ ( 1 ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) = ( ๐‘‹ โ€˜ ๐‘˜ ) )
21 0cn โŠข 0 โˆˆ โ„‚
22 21 mul02i โŠข ( 0 ยท 0 ) = 0
23 1 2 4 5 10 3 dchrelbas2 โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆˆ ๐ท โ†” ( ๐‘‹ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆง โˆ€ ๐‘˜ โˆˆ ๐ต ( ( ๐‘‹ โ€˜ ๐‘˜ ) โ‰  0 โ†’ ๐‘˜ โˆˆ ๐‘ˆ ) ) ) )
24 8 23 mpbid โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆง โˆ€ ๐‘˜ โˆˆ ๐ต ( ( ๐‘‹ โ€˜ ๐‘˜ ) โ‰  0 โ†’ ๐‘˜ โˆˆ ๐‘ˆ ) ) )
25 24 simprd โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘˜ โˆˆ ๐ต ( ( ๐‘‹ โ€˜ ๐‘˜ ) โ‰  0 โ†’ ๐‘˜ โˆˆ ๐‘ˆ ) )
26 25 r19.21bi โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ต ) โ†’ ( ( ๐‘‹ โ€˜ ๐‘˜ ) โ‰  0 โ†’ ๐‘˜ โˆˆ ๐‘ˆ ) )
27 26 necon1bd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ต ) โ†’ ( ยฌ ๐‘˜ โˆˆ ๐‘ˆ โ†’ ( ๐‘‹ โ€˜ ๐‘˜ ) = 0 ) )
28 27 imp โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ต ) โˆง ยฌ ๐‘˜ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘‹ โ€˜ ๐‘˜ ) = 0 )
29 28 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ต ) โˆง ยฌ ๐‘˜ โˆˆ ๐‘ˆ ) โ†’ ( 0 ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) = ( 0 ยท 0 ) )
30 22 29 28 3eqtr4a โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ต ) โˆง ยฌ ๐‘˜ โˆˆ ๐‘ˆ ) โ†’ ( 0 ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) = ( ๐‘‹ โ€˜ ๐‘˜ ) )
31 14 16 20 30 ifbothda โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ต ) โ†’ ( if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) = ( ๐‘‹ โ€˜ ๐‘˜ ) )
32 31 mpteq2dva โŠข ( ๐œ‘ โ†’ ( ๐‘˜ โˆˆ ๐ต โ†ฆ ( if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) ) = ( ๐‘˜ โˆˆ ๐ต โ†ฆ ( ๐‘‹ โ€˜ ๐‘˜ ) ) )
33 4 fvexi โŠข ๐ต โˆˆ V
34 33 a1i โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ V )
35 ax-1cn โŠข 1 โˆˆ โ„‚
36 35 21 ifcli โŠข if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) โˆˆ โ„‚
37 36 a1i โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ต ) โ†’ if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) โˆˆ โ„‚ )
38 6 a1i โŠข ( ๐œ‘ โ†’ 1 = ( ๐‘˜ โˆˆ ๐ต โ†ฆ if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) ) )
39 17 feqmptd โŠข ( ๐œ‘ โ†’ ๐‘‹ = ( ๐‘˜ โˆˆ ๐ต โ†ฆ ( ๐‘‹ โ€˜ ๐‘˜ ) ) )
40 34 37 18 38 39 offval2 โŠข ( ๐œ‘ โ†’ ( 1 โˆ˜f ยท ๐‘‹ ) = ( ๐‘˜ โˆˆ ๐ต โ†ฆ ( if ( ๐‘˜ โˆˆ ๐‘ˆ , 1 , 0 ) ยท ( ๐‘‹ โ€˜ ๐‘˜ ) ) ) )
41 32 40 39 3eqtr4d โŠข ( ๐œ‘ โ†’ ( 1 โˆ˜f ยท ๐‘‹ ) = ๐‘‹ )
42 12 41 eqtrd โŠข ( ๐œ‘ โ†’ ( 1 ยท ๐‘‹ ) = ๐‘‹ )