Theorem dchrplusg

Description: Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrmul.t	⊢ · = ( +g ‘ 𝐺 )
	dchrplusg.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	dchrplusg	⊢ ( 𝜑 → · = ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		dchrmul.t	⊢ · = ( +g ‘ 𝐺 )
5		dchrplusg.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
7		eqid	⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
8	1 2 6 7 5 3	dchrbas	⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑍 ) ∖ ( Unit ‘ 𝑍 ) ) × { 0 } ) ⊆ 𝑥 } )
9	1 2 6 7 5 8	dchrval	⊢ ( 𝜑 → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )
10	9	fveq2d	⊢ ( 𝜑 → ( +g ‘ 𝐺 ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } ) )
11	3	fvexi	⊢ 𝐷 ∈ V
12	11 11	xpex	⊢ ( 𝐷 × 𝐷 ) ∈ V
13		ofexg	⊢ ( ( 𝐷 × 𝐷 ) ∈ V → ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ∈ V )
14		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ }
15	14	grpplusg	⊢ ( ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ∈ V → ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } ) )
16	12 13 15	mp2b	⊢ ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐷 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) ⟩ } )
17	10 4 16	3eqtr4g	⊢ ( 𝜑 → · = ( ∘f · ↾ ( 𝐷 × 𝐷 ) ) )