Metamath Proof Explorer


Theorem dchrbas

Description: Base set of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrval.g โŠข ๐บ = ( DChr โ€˜ ๐‘ )
dchrval.z โŠข ๐‘ = ( โ„ค/nโ„ค โ€˜ ๐‘ )
dchrval.b โŠข ๐ต = ( Base โ€˜ ๐‘ )
dchrval.u โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘ )
dchrval.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
dchrbas.b โŠข ๐ท = ( Base โ€˜ ๐บ )
Assertion dchrbas ( ๐œ‘ โ†’ ๐ท = { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } )

Proof

Step Hyp Ref Expression
1 dchrval.g โŠข ๐บ = ( DChr โ€˜ ๐‘ )
2 dchrval.z โŠข ๐‘ = ( โ„ค/nโ„ค โ€˜ ๐‘ )
3 dchrval.b โŠข ๐ต = ( Base โ€˜ ๐‘ )
4 dchrval.u โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘ )
5 dchrval.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
6 dchrbas.b โŠข ๐ท = ( Base โ€˜ ๐บ )
7 eqidd โŠข ( ๐œ‘ โ†’ { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } = { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } )
8 1 2 3 4 5 7 dchrval โŠข ( ๐œ‘ โ†’ ๐บ = { โŸจ ( Base โ€˜ ndx ) , { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ร— { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ) ) โŸฉ } )
9 8 fveq2d โŠข ( ๐œ‘ โ†’ ( Base โ€˜ ๐บ ) = ( Base โ€˜ { โŸจ ( Base โ€˜ ndx ) , { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ร— { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ) ) โŸฉ } ) )
10 ovex โŠข ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆˆ V
11 10 rabex โŠข { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } โˆˆ V
12 eqid โŠข { โŸจ ( Base โ€˜ ndx ) , { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ร— { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ) ) โŸฉ } = { โŸจ ( Base โ€˜ ndx ) , { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ร— { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ) ) โŸฉ }
13 12 grpbase โŠข ( { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } โˆˆ V โ†’ { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } = ( Base โ€˜ { โŸจ ( Base โ€˜ ndx ) , { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ร— { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ) ) โŸฉ } ) )
14 11 13 ax-mp โŠข { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } = ( Base โ€˜ { โŸจ ( Base โ€˜ ndx ) , { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ร— { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } ) ) โŸฉ } )
15 9 6 14 3eqtr4g โŠข ( ๐œ‘ โ†’ ๐ท = { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ๐ต โˆ– ๐‘ˆ ) ร— { 0 } ) โІ ๐‘ฅ } )