MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrinv Structured version   Visualization version   GIF version

Theorem dchrinv 26988
Description: The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of 𝑋 are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016.)
Hypotheses
Ref Expression
dchrabs.g 𝐺 = (DChrβ€˜π‘)
dchrabs.d 𝐷 = (Baseβ€˜πΊ)
dchrabs.x (πœ‘ β†’ 𝑋 ∈ 𝐷)
dchrinv.i 𝐼 = (invgβ€˜πΊ)
Assertion
Ref Expression
dchrinv (πœ‘ β†’ (πΌβ€˜π‘‹) = (βˆ— ∘ 𝑋))

Proof of Theorem dchrinv
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dchrabs.g . . . . . . . 8 𝐺 = (DChrβ€˜π‘)
2 eqid 2732 . . . . . . . 8 (β„€/nβ„€β€˜π‘) = (β„€/nβ„€β€˜π‘)
3 dchrabs.d . . . . . . . 8 𝐷 = (Baseβ€˜πΊ)
4 eqid 2732 . . . . . . . 8 (+gβ€˜πΊ) = (+gβ€˜πΊ)
5 dchrabs.x . . . . . . . 8 (πœ‘ β†’ 𝑋 ∈ 𝐷)
6 cjf 15055 . . . . . . . . . 10 βˆ—:β„‚βŸΆβ„‚
7 eqid 2732 . . . . . . . . . . 11 (Baseβ€˜(β„€/nβ„€β€˜π‘)) = (Baseβ€˜(β„€/nβ„€β€˜π‘))
81, 2, 3, 7, 5dchrf 26969 . . . . . . . . . 10 (πœ‘ β†’ 𝑋:(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚)
9 fco 6741 . . . . . . . . . 10 ((βˆ—:β„‚βŸΆβ„‚ ∧ 𝑋:(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚) β†’ (βˆ— ∘ 𝑋):(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚)
106, 8, 9sylancr 587 . . . . . . . . 9 (πœ‘ β†’ (βˆ— ∘ 𝑋):(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚)
11 eqid 2732 . . . . . . . . . . . . . . . . . . . . 21 (Unitβ€˜(β„€/nβ„€β€˜π‘)) = (Unitβ€˜(β„€/nβ„€β€˜π‘))
121, 3dchrrcl 26967 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 ∈ 𝐷 β†’ 𝑁 ∈ β„•)
135, 12syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑁 ∈ β„•)
141, 2, 7, 11, 13, 3dchrelbas3 26965 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝑋 ∈ 𝐷 ↔ (𝑋:(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚ ∧ (βˆ€π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))βˆ€π‘¦ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))(π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = ((π‘‹β€˜π‘₯) Β· (π‘‹β€˜π‘¦)) ∧ (π‘‹β€˜(1rβ€˜(β„€/nβ„€β€˜π‘))) = 1 ∧ βˆ€π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))((π‘‹β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))))))
155, 14mpbid 231 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑋:(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚ ∧ (βˆ€π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))βˆ€π‘¦ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))(π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = ((π‘‹β€˜π‘₯) Β· (π‘‹β€˜π‘¦)) ∧ (π‘‹β€˜(1rβ€˜(β„€/nβ„€β€˜π‘))) = 1 ∧ βˆ€π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))((π‘‹β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))))))
1615simprd 496 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (βˆ€π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))βˆ€π‘¦ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))(π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = ((π‘‹β€˜π‘₯) Β· (π‘‹β€˜π‘¦)) ∧ (π‘‹β€˜(1rβ€˜(β„€/nβ„€β€˜π‘))) = 1 ∧ βˆ€π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))((π‘‹β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))))
1716simp1d 1142 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ€π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))βˆ€π‘¦ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))(π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = ((π‘‹β€˜π‘₯) Β· (π‘‹β€˜π‘¦)))
1817r19.21bi 3248 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ βˆ€π‘¦ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))(π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = ((π‘‹β€˜π‘₯) Β· (π‘‹β€˜π‘¦)))
1918r19.21bi 3248 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ (π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = ((π‘‹β€˜π‘₯) Β· (π‘‹β€˜π‘¦)))
2019anasss 467 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ (π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = ((π‘‹β€˜π‘₯) Β· (π‘‹β€˜π‘¦)))
2120fveq2d 6895 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ (βˆ—β€˜(π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦))) = (βˆ—β€˜((π‘‹β€˜π‘₯) Β· (π‘‹β€˜π‘¦))))
228adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ 𝑋:(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚)
237, 11unitss 20267 . . . . . . . . . . . . . . . 16 (Unitβ€˜(β„€/nβ„€β€˜π‘)) βŠ† (Baseβ€˜(β„€/nβ„€β€˜π‘))
24 simprl 769 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))
2523, 24sselid 3980 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘)))
2622, 25ffvelcdmd 7087 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ (π‘‹β€˜π‘₯) ∈ β„‚)
27 simprr 771 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))
2823, 27sselid 3980 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ 𝑦 ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘)))
2922, 28ffvelcdmd 7087 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ (π‘‹β€˜π‘¦) ∈ β„‚)
3026, 29cjmuld 15172 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ (βˆ—β€˜((π‘‹β€˜π‘₯) Β· (π‘‹β€˜π‘¦))) = ((βˆ—β€˜(π‘‹β€˜π‘₯)) Β· (βˆ—β€˜(π‘‹β€˜π‘¦))))
3121, 30eqtrd 2772 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ (βˆ—β€˜(π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦))) = ((βˆ—β€˜(π‘‹β€˜π‘₯)) Β· (βˆ—β€˜(π‘‹β€˜π‘¦))))
3213nnnn0d 12536 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑁 ∈ β„•0)
332zncrng 21319 . . . . . . . . . . . . . . . 16 (𝑁 ∈ β„•0 β†’ (β„€/nβ„€β€˜π‘) ∈ CRing)
34 crngring 20139 . . . . . . . . . . . . . . . 16 ((β„€/nβ„€β€˜π‘) ∈ CRing β†’ (β„€/nβ„€β€˜π‘) ∈ Ring)
3532, 33, 343syl 18 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β„€/nβ„€β€˜π‘) ∈ Ring)
3635adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ (β„€/nβ„€β€˜π‘) ∈ Ring)
37 eqid 2732 . . . . . . . . . . . . . . 15 (.rβ€˜(β„€/nβ„€β€˜π‘)) = (.rβ€˜(β„€/nβ„€β€˜π‘))
387, 37ringcl 20144 . . . . . . . . . . . . . 14 (((β„€/nβ„€β€˜π‘) ∈ Ring ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ (π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦) ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘)))
3936, 25, 28, 38syl3anc 1371 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ (π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦) ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘)))
40 fvco3 6990 . . . . . . . . . . . . 13 ((𝑋:(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚ ∧ (π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦) ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((βˆ— ∘ 𝑋)β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = (βˆ—β€˜(π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦))))
4122, 39, 40syl2anc 584 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ ((βˆ— ∘ 𝑋)β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = (βˆ—β€˜(π‘‹β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦))))
42 fvco3 6990 . . . . . . . . . . . . . 14 ((𝑋:(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚ ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((βˆ— ∘ 𝑋)β€˜π‘₯) = (βˆ—β€˜(π‘‹β€˜π‘₯)))
4322, 25, 42syl2anc 584 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ ((βˆ— ∘ 𝑋)β€˜π‘₯) = (βˆ—β€˜(π‘‹β€˜π‘₯)))
44 fvco3 6990 . . . . . . . . . . . . . 14 ((𝑋:(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚ ∧ 𝑦 ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((βˆ— ∘ 𝑋)β€˜π‘¦) = (βˆ—β€˜(π‘‹β€˜π‘¦)))
4522, 28, 44syl2anc 584 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ ((βˆ— ∘ 𝑋)β€˜π‘¦) = (βˆ—β€˜(π‘‹β€˜π‘¦)))
4643, 45oveq12d 7429 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ (((βˆ— ∘ 𝑋)β€˜π‘₯) Β· ((βˆ— ∘ 𝑋)β€˜π‘¦)) = ((βˆ—β€˜(π‘‹β€˜π‘₯)) Β· (βˆ—β€˜(π‘‹β€˜π‘¦))))
4731, 41, 463eqtr4d 2782 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) ∧ 𝑦 ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))) β†’ ((βˆ— ∘ 𝑋)β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = (((βˆ— ∘ 𝑋)β€˜π‘₯) Β· ((βˆ— ∘ 𝑋)β€˜π‘¦)))
4847ralrimivva 3200 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))βˆ€π‘¦ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))((βˆ— ∘ 𝑋)β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = (((βˆ— ∘ 𝑋)β€˜π‘₯) Β· ((βˆ— ∘ 𝑋)β€˜π‘¦)))
49 eqid 2732 . . . . . . . . . . . . . 14 (1rβ€˜(β„€/nβ„€β€˜π‘)) = (1rβ€˜(β„€/nβ„€β€˜π‘))
507, 49ringidcl 20154 . . . . . . . . . . . . 13 ((β„€/nβ„€β€˜π‘) ∈ Ring β†’ (1rβ€˜(β„€/nβ„€β€˜π‘)) ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘)))
5135, 50syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (1rβ€˜(β„€/nβ„€β€˜π‘)) ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘)))
52 fvco3 6990 . . . . . . . . . . . 12 ((𝑋:(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚ ∧ (1rβ€˜(β„€/nβ„€β€˜π‘)) ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((βˆ— ∘ 𝑋)β€˜(1rβ€˜(β„€/nβ„€β€˜π‘))) = (βˆ—β€˜(π‘‹β€˜(1rβ€˜(β„€/nβ„€β€˜π‘)))))
538, 51, 52syl2anc 584 . . . . . . . . . . 11 (πœ‘ β†’ ((βˆ— ∘ 𝑋)β€˜(1rβ€˜(β„€/nβ„€β€˜π‘))) = (βˆ—β€˜(π‘‹β€˜(1rβ€˜(β„€/nβ„€β€˜π‘)))))
5416simp2d 1143 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘‹β€˜(1rβ€˜(β„€/nβ„€β€˜π‘))) = 1)
5554fveq2d 6895 . . . . . . . . . . . 12 (πœ‘ β†’ (βˆ—β€˜(π‘‹β€˜(1rβ€˜(β„€/nβ„€β€˜π‘)))) = (βˆ—β€˜1))
56 1re 11218 . . . . . . . . . . . . 13 1 ∈ ℝ
57 cjre 15090 . . . . . . . . . . . . 13 (1 ∈ ℝ β†’ (βˆ—β€˜1) = 1)
5856, 57ax-mp 5 . . . . . . . . . . . 12 (βˆ—β€˜1) = 1
5955, 58eqtrdi 2788 . . . . . . . . . . 11 (πœ‘ β†’ (βˆ—β€˜(π‘‹β€˜(1rβ€˜(β„€/nβ„€β€˜π‘)))) = 1)
6053, 59eqtrd 2772 . . . . . . . . . 10 (πœ‘ β†’ ((βˆ— ∘ 𝑋)β€˜(1rβ€˜(β„€/nβ„€β€˜π‘))) = 1)
6116simp3d 1144 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))((π‘‹β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))))
628, 42sylan 580 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((βˆ— ∘ 𝑋)β€˜π‘₯) = (βˆ—β€˜(π‘‹β€˜π‘₯)))
63 cj0 15109 . . . . . . . . . . . . . . . . . 18 (βˆ—β€˜0) = 0
6463eqcomi 2741 . . . . . . . . . . . . . . . . 17 0 = (βˆ—β€˜0)
6564a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ 0 = (βˆ—β€˜0))
6662, 65eqeq12d 2748 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ (((βˆ— ∘ 𝑋)β€˜π‘₯) = 0 ↔ (βˆ—β€˜(π‘‹β€˜π‘₯)) = (βˆ—β€˜0)))
678ffvelcdmda 7086 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ (π‘‹β€˜π‘₯) ∈ β„‚)
68 0cn 11210 . . . . . . . . . . . . . . . 16 0 ∈ β„‚
69 cj11 15113 . . . . . . . . . . . . . . . 16 (((π‘‹β€˜π‘₯) ∈ β„‚ ∧ 0 ∈ β„‚) β†’ ((βˆ—β€˜(π‘‹β€˜π‘₯)) = (βˆ—β€˜0) ↔ (π‘‹β€˜π‘₯) = 0))
7067, 68, 69sylancl 586 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((βˆ—β€˜(π‘‹β€˜π‘₯)) = (βˆ—β€˜0) ↔ (π‘‹β€˜π‘₯) = 0))
7166, 70bitrd 278 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ (((βˆ— ∘ 𝑋)β€˜π‘₯) = 0 ↔ (π‘‹β€˜π‘₯) = 0))
7271necon3bid 2985 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ (((βˆ— ∘ 𝑋)β€˜π‘₯) β‰  0 ↔ (π‘‹β€˜π‘₯) β‰  0))
7372imbi1d 341 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((((βˆ— ∘ 𝑋)β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) ↔ ((π‘‹β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))))
7473ralbidva 3175 . . . . . . . . . . 11 (πœ‘ β†’ (βˆ€π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))(((βˆ— ∘ 𝑋)β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) ↔ βˆ€π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))((π‘‹β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))))
7561, 74mpbird 256 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))(((βˆ— ∘ 𝑋)β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))))
7648, 60, 753jca 1128 . . . . . . . . 9 (πœ‘ β†’ (βˆ€π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))βˆ€π‘¦ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))((βˆ— ∘ 𝑋)β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = (((βˆ— ∘ 𝑋)β€˜π‘₯) Β· ((βˆ— ∘ 𝑋)β€˜π‘¦)) ∧ ((βˆ— ∘ 𝑋)β€˜(1rβ€˜(β„€/nβ„€β€˜π‘))) = 1 ∧ βˆ€π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))(((βˆ— ∘ 𝑋)β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))))
771, 2, 7, 11, 13, 3dchrelbas3 26965 . . . . . . . . 9 (πœ‘ β†’ ((βˆ— ∘ 𝑋) ∈ 𝐷 ↔ ((βˆ— ∘ 𝑋):(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚ ∧ (βˆ€π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))βˆ€π‘¦ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))((βˆ— ∘ 𝑋)β€˜(π‘₯(.rβ€˜(β„€/nβ„€β€˜π‘))𝑦)) = (((βˆ— ∘ 𝑋)β€˜π‘₯) Β· ((βˆ— ∘ 𝑋)β€˜π‘¦)) ∧ ((βˆ— ∘ 𝑋)β€˜(1rβ€˜(β„€/nβ„€β€˜π‘))) = 1 ∧ βˆ€π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘))(((βˆ— ∘ 𝑋)β€˜π‘₯) β‰  0 β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))))))
7810, 76, 77mpbir2and 711 . . . . . . . 8 (πœ‘ β†’ (βˆ— ∘ 𝑋) ∈ 𝐷)
791, 2, 3, 4, 5, 78dchrmul 26975 . . . . . . 7 (πœ‘ β†’ (𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋)) = (𝑋 ∘f Β· (βˆ— ∘ 𝑋)))
8079adantr 481 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ (𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋)) = (𝑋 ∘f Β· (βˆ— ∘ 𝑋)))
8180fveq1d 6893 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋))β€˜π‘₯) = ((𝑋 ∘f Β· (βˆ— ∘ 𝑋))β€˜π‘₯))
8223sseli 3978 . . . . . . . . 9 (π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)) β†’ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘)))
8382, 62sylan2 593 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((βˆ— ∘ 𝑋)β€˜π‘₯) = (βˆ—β€˜(π‘‹β€˜π‘₯)))
8483oveq2d 7427 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((π‘‹β€˜π‘₯) Β· ((βˆ— ∘ 𝑋)β€˜π‘₯)) = ((π‘‹β€˜π‘₯) Β· (βˆ—β€˜(π‘‹β€˜π‘₯))))
8582, 67sylan2 593 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ (π‘‹β€˜π‘₯) ∈ β„‚)
8685absvalsqd 15393 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((absβ€˜(π‘‹β€˜π‘₯))↑2) = ((π‘‹β€˜π‘₯) Β· (βˆ—β€˜(π‘‹β€˜π‘₯))))
875adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ 𝑋 ∈ 𝐷)
88 simpr 485 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘)))
891, 3, 87, 2, 11, 88dchrabs 26987 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ (absβ€˜(π‘‹β€˜π‘₯)) = 1)
9089oveq1d 7426 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((absβ€˜(π‘‹β€˜π‘₯))↑2) = (1↑2))
91 sq1 14163 . . . . . . . 8 (1↑2) = 1
9290, 91eqtrdi 2788 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((absβ€˜(π‘‹β€˜π‘₯))↑2) = 1)
9384, 86, 923eqtr2d 2778 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((π‘‹β€˜π‘₯) Β· ((βˆ— ∘ 𝑋)β€˜π‘₯)) = 1)
948adantr 481 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ 𝑋:(Baseβ€˜(β„€/nβ„€β€˜π‘))βŸΆβ„‚)
9594ffnd 6718 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ 𝑋 Fn (Baseβ€˜(β„€/nβ„€β€˜π‘)))
9610ffnd 6718 . . . . . . . 8 (πœ‘ β†’ (βˆ— ∘ 𝑋) Fn (Baseβ€˜(β„€/nβ„€β€˜π‘)))
9796adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ (βˆ— ∘ 𝑋) Fn (Baseβ€˜(β„€/nβ„€β€˜π‘)))
98 fvexd 6906 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ (Baseβ€˜(β„€/nβ„€β€˜π‘)) ∈ V)
9982adantl 482 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘)))
100 fnfvof 7689 . . . . . . 7 (((𝑋 Fn (Baseβ€˜(β„€/nβ„€β€˜π‘)) ∧ (βˆ— ∘ 𝑋) Fn (Baseβ€˜(β„€/nβ„€β€˜π‘))) ∧ ((Baseβ€˜(β„€/nβ„€β€˜π‘)) ∈ V ∧ π‘₯ ∈ (Baseβ€˜(β„€/nβ„€β€˜π‘)))) β†’ ((𝑋 ∘f Β· (βˆ— ∘ 𝑋))β€˜π‘₯) = ((π‘‹β€˜π‘₯) Β· ((βˆ— ∘ 𝑋)β€˜π‘₯)))
10195, 97, 98, 99, 100syl22anc 837 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((𝑋 ∘f Β· (βˆ— ∘ 𝑋))β€˜π‘₯) = ((π‘‹β€˜π‘₯) Β· ((βˆ— ∘ 𝑋)β€˜π‘₯)))
102 eqid 2732 . . . . . . 7 (0gβ€˜πΊ) = (0gβ€˜πΊ)
10313adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ 𝑁 ∈ β„•)
1041, 2, 102, 11, 103, 88dchr1 26984 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((0gβ€˜πΊ)β€˜π‘₯) = 1)
10593, 101, 1043eqtr4d 2782 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((𝑋 ∘f Β· (βˆ— ∘ 𝑋))β€˜π‘₯) = ((0gβ€˜πΊ)β€˜π‘₯))
10681, 105eqtrd 2772 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))) β†’ ((𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋))β€˜π‘₯) = ((0gβ€˜πΊ)β€˜π‘₯))
107106ralrimiva 3146 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))((𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋))β€˜π‘₯) = ((0gβ€˜πΊ)β€˜π‘₯))
1081, 2, 3, 4, 5, 78dchrmulcl 26976 . . . 4 (πœ‘ β†’ (𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋)) ∈ 𝐷)
1091dchrabl 26981 . . . . . 6 (𝑁 ∈ β„• β†’ 𝐺 ∈ Abel)
110 ablgrp 19694 . . . . . 6 (𝐺 ∈ Abel β†’ 𝐺 ∈ Grp)
11113, 109, 1103syl 18 . . . . 5 (πœ‘ β†’ 𝐺 ∈ Grp)
1123, 102grpidcl 18886 . . . . 5 (𝐺 ∈ Grp β†’ (0gβ€˜πΊ) ∈ 𝐷)
113111, 112syl 17 . . . 4 (πœ‘ β†’ (0gβ€˜πΊ) ∈ 𝐷)
1141, 2, 3, 11, 108, 113dchreq 26985 . . 3 (πœ‘ β†’ ((𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋)) = (0gβ€˜πΊ) ↔ βˆ€π‘₯ ∈ (Unitβ€˜(β„€/nβ„€β€˜π‘))((𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋))β€˜π‘₯) = ((0gβ€˜πΊ)β€˜π‘₯)))
115107, 114mpbird 256 . 2 (πœ‘ β†’ (𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋)) = (0gβ€˜πΊ))
116 dchrinv.i . . . 4 𝐼 = (invgβ€˜πΊ)
1173, 4, 102, 116grpinvid1 18912 . . 3 ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐷 ∧ (βˆ— ∘ 𝑋) ∈ 𝐷) β†’ ((πΌβ€˜π‘‹) = (βˆ— ∘ 𝑋) ↔ (𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋)) = (0gβ€˜πΊ)))
118111, 5, 78, 117syl3anc 1371 . 2 (πœ‘ β†’ ((πΌβ€˜π‘‹) = (βˆ— ∘ 𝑋) ↔ (𝑋(+gβ€˜πΊ)(βˆ— ∘ 𝑋)) = (0gβ€˜πΊ)))
119115, 118mpbird 256 1 (πœ‘ β†’ (πΌβ€˜π‘‹) = (βˆ— ∘ 𝑋))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  Vcvv 3474   ∘ ccom 5680   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411   ∘f cof 7670  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   Β· cmul 11117  β„•cn 12216  2c2 12271  β„•0cn0 12476  β†‘cexp 14031  βˆ—ccj 15047  abscabs 15185  Basecbs 17148  +gcplusg 17201  .rcmulr 17202  0gc0g 17389  Grpcgrp 18855  invgcminusg 18856  Abelcabl 19690  1rcur 20075  Ringcrg 20127  CRingccrg 20128  Unitcui 20246  β„€/nβ„€czn 21271  DChrcdchr 26959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-omul 8473  df-er 8705  df-ec 8707  df-qs 8711  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-acn 9939  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ioo 13332  df-ioc 13333  df-ico 13334  df-icc 13335  df-fz 13489  df-fzo 13632  df-fl 13761  df-mod 13839  df-seq 13971  df-exp 14032  df-fac 14238  df-bc 14267  df-hash 14295  df-shft 15018  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-limsup 15419  df-clim 15436  df-rlim 15437  df-sum 15637  df-ef 16015  df-sin 16017  df-cos 16018  df-pi 16020  df-dvds 16202  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-starv 17216  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-hom 17225  df-cco 17226  df-rest 17372  df-topn 17373  df-0g 17391  df-gsum 17392  df-topgen 17393  df-pt 17394  df-prds 17397  df-xrs 17452  df-qtop 17457  df-imas 17458  df-qus 17459  df-xps 17460  df-mre 17534  df-mrc 17535  df-acs 17537  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-mhm 18705  df-submnd 18706  df-grp 18858  df-minusg 18859  df-sbg 18860  df-mulg 18987  df-subg 19039  df-nsg 19040  df-eqg 19041  df-ghm 19128  df-cntz 19222  df-od 19437  df-cmn 19691  df-abl 19692  df-mgp 20029  df-rng 20047  df-ur 20076  df-ring 20129  df-cring 20130  df-oppr 20225  df-dvdsr 20248  df-unit 20249  df-invr 20279  df-dvr 20292  df-rhm 20363  df-subrng 20434  df-subrg 20459  df-drng 20502  df-lmod 20616  df-lss 20687  df-lsp 20727  df-sra 20930  df-rgmod 20931  df-lidl 20932  df-rsp 20933  df-2idl 21006  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-fbas 21141  df-fg 21142  df-cnfld 21145  df-zring 21218  df-zrh 21272  df-zn 21275  df-top 22616  df-topon 22633  df-topsp 22655  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745  df-nei 22822  df-lp 22860  df-perf 22861  df-cn 22951  df-cnp 22952  df-haus 23039  df-tx 23286  df-hmeo 23479  df-fil 23570  df-fm 23662  df-flim 23663  df-flf 23664  df-xms 24046  df-ms 24047  df-tms 24048  df-cncf 24618  df-limc 25607  df-dv 25608  df-log 26289  df-cxp 26290  df-dchr 26960
This theorem is referenced by:  dchr2sum  27000  dchrisum0re  27240
  Copyright terms: Public domain W3C validator