Metamath Proof Explorer

Theorem dchrelbas3

Description: A Dirichlet character is a monoid homomorphism from the multiplicative monoid on Z/nZ to the multiplicative monoid of CC , which is zero off the group of units of Z/nZ . (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses dchrval.g 
|- G = ( DChr ` N )
dchrval.z 
|- Z = ( Z/nZ ` N )
dchrval.b 
|- B = ( Base ` Z )
dchrval.u 
|- U = ( Unit ` Z )
dchrval.n 
|- ( ph -> N e. NN )
dchrbas.b 
|- D = ( Base ` G )
Assertion dchrelbas3 
|- ( ph -> ( X e. D <-> ( X : B --> CC /\ ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dchrval.g 
 |-  G = ( DChr ` N )
2 dchrval.z 
 |-  Z = ( Z/nZ ` N )
3 dchrval.b 
 |-  B = ( Base ` Z )
4 dchrval.u 
 |-  U = ( Unit ` Z )
5 dchrval.n 
 |-  ( ph -> N e. NN )
6 dchrbas.b 
 |-  D = ( Base ` G )
7 1 2 3 4 5 6 dchrelbas2 
 |-  ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) )
8 fveq2 
 |-  ( z = x -> ( X ` z ) = ( X ` x ) )
9 8 neeq1d 
 |-  ( z = x -> ( ( X ` z ) =/= 0 <-> ( X ` x ) =/= 0 ) )
10 eleq1 
 |-  ( z = x -> ( z e. U <-> x e. U ) )
11 9 10 imbi12d 
 |-  ( z = x -> ( ( ( X ` z ) =/= 0 -> z e. U ) <-> ( ( X ` x ) =/= 0 -> x e. U ) ) )
12 11 cbvralvw 
 |-  ( A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) <-> A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) )
13 5 nnnn0d 
 |-  ( ph -> N e. NN0 )
14 2 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
15 13 14 syl 
 |-  ( ph -> Z e. CRing )
16 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
17 15 16 syl 
 |-  ( ph -> Z e. Ring )
18 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
19 18 ringmgp 
 |-  ( Z e. Ring -> ( mulGrp ` Z ) e. Mnd )
20 17 19 syl 
 |-  ( ph -> ( mulGrp ` Z ) e. Mnd )
21 cnring 
 |-  CCfld e. Ring
22 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
23 22 ringmgp 
 |-  ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
24 21 23 ax-mp 
 |-  ( mulGrp ` CCfld ) e. Mnd
25 18 3 mgpbas 
 |-  B = ( Base ` ( mulGrp ` Z ) )
26 cnfldbas 
 |-  CC = ( Base ` CCfld )
27 22 26 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
28 eqid 
 |-  ( .r ` Z ) = ( .r ` Z )
29 18 28 mgpplusg 
 |-  ( .r ` Z ) = ( +g ` ( mulGrp ` Z ) )
30 cnfldmul 
 |-  x. = ( .r ` CCfld )
31 22 30 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
32 eqid 
 |-  ( 1r ` Z ) = ( 1r ` Z )
33 18 32 ringidval 
 |-  ( 1r ` Z ) = ( 0g ` ( mulGrp ` Z ) )
34 cnfld1 
 |-  1 = ( 1r ` CCfld )
35 22 34 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
36 25 27 29 31 33 35 ismhm 
 |-  ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) <-> ( ( ( mulGrp ` Z ) e. Mnd /\ ( mulGrp ` CCfld ) e. Mnd ) /\ ( X : B --> CC /\ A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) ) )
37 36 baib 
 |-  ( ( ( mulGrp ` Z ) e. Mnd /\ ( mulGrp ` CCfld ) e. Mnd ) -> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) <-> ( X : B --> CC /\ A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) ) )
38 20 24 37 sylancl 
 |-  ( ph -> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) <-> ( X : B --> CC /\ A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) ) )
39 38 adantr 
 |-  ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) -> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) <-> ( X : B --> CC /\ A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) ) )
40 biimt 
 |-  ( ( x e. U /\ y e. U ) -> ( ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) <-> ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) )
41 40 adantl 
 |-  ( ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) /\ ( x e. U /\ y e. U ) ) -> ( ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) <-> ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) )
42 fveq2 
 |-  ( z = ( x ( .r ` Z ) y ) -> ( X ` z ) = ( X ` ( x ( .r ` Z ) y ) ) )
43 42 neeq1d 
 |-  ( z = ( x ( .r ` Z ) y ) -> ( ( X ` z ) =/= 0 <-> ( X ` ( x ( .r ` Z ) y ) ) =/= 0 ) )
44 eleq1 
 |-  ( z = ( x ( .r ` Z ) y ) -> ( z e. U <-> ( x ( .r ` Z ) y ) e. U ) )
45 43 44 imbi12d 
 |-  ( z = ( x ( .r ` Z ) y ) -> ( ( ( X ` z ) =/= 0 -> z e. U ) <-> ( ( X ` ( x ( .r ` Z ) y ) ) =/= 0 -> ( x ( .r ` Z ) y ) e. U ) ) )
46 simpllr 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) )
47 17 ad3antrrr 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> Z e. Ring )
48 simprl 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> x e. B )
49 simprr 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> y e. B )
50 3 28 ringcl 
 |-  ( ( Z e. Ring /\ x e. B /\ y e. B ) -> ( x ( .r ` Z ) y ) e. B )
51 47 48 49 50 syl3anc 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` Z ) y ) e. B )
52 45 46 51 rspcdva 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( ( X ` ( x ( .r ` Z ) y ) ) =/= 0 -> ( x ( .r ` Z ) y ) e. U ) )
53 15 ad3antrrr 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> Z e. CRing )
54 4 28 3 unitmulclb 
 |-  ( ( Z e. CRing /\ x e. B /\ y e. B ) -> ( ( x ( .r ` Z ) y ) e. U <-> ( x e. U /\ y e. U ) ) )
55 53 48 49 54 syl3anc 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( ( x ( .r ` Z ) y ) e. U <-> ( x e. U /\ y e. U ) ) )
56 52 55 sylibd 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( ( X ` ( x ( .r ` Z ) y ) ) =/= 0 -> ( x e. U /\ y e. U ) ) )
57 56 necon1bd 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( -. ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = 0 ) )
58 57 imp 
 |-  ( ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x e. U /\ y e. U ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = 0 )
59 11 46 48 rspcdva 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( ( X ` x ) =/= 0 -> x e. U ) )
60 fveq2 
 |-  ( z = y -> ( X ` z ) = ( X ` y ) )
61 60 neeq1d 
 |-  ( z = y -> ( ( X ` z ) =/= 0 <-> ( X ` y ) =/= 0 ) )
62 eleq1 
 |-  ( z = y -> ( z e. U <-> y e. U ) )
63 61 62 imbi12d 
 |-  ( z = y -> ( ( ( X ` z ) =/= 0 -> z e. U ) <-> ( ( X ` y ) =/= 0 -> y e. U ) ) )
64 63 46 49 rspcdva 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( ( X ` y ) =/= 0 -> y e. U ) )
65 59 64 anim12d 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( ( ( X ` x ) =/= 0 /\ ( X ` y ) =/= 0 ) -> ( x e. U /\ y e. U ) ) )
66 65 con3dimp 
 |-  ( ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x e. U /\ y e. U ) ) -> -. ( ( X ` x ) =/= 0 /\ ( X ` y ) =/= 0 ) )
67 neanior 
 |-  ( ( ( X ` x ) =/= 0 /\ ( X ` y ) =/= 0 ) <-> -. ( ( X ` x ) = 0 \/ ( X ` y ) = 0 ) )
68 67 con2bii 
 |-  ( ( ( X ` x ) = 0 \/ ( X ` y ) = 0 ) <-> -. ( ( X ` x ) =/= 0 /\ ( X ` y ) =/= 0 ) )
69 66 68 sylibr 
 |-  ( ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x e. U /\ y e. U ) ) -> ( ( X ` x ) = 0 \/ ( X ` y ) = 0 ) )
70 simplr 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> X : B --> CC )
71 70 48 ffvelrnd 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( X ` x ) e. CC )
72 70 49 ffvelrnd 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( X ` y ) e. CC )
73 71 72 mul0ord 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( ( ( X ` x ) x. ( X ` y ) ) = 0 <-> ( ( X ` x ) = 0 \/ ( X ` y ) = 0 ) ) )
74 73 adantr 
 |-  ( ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x e. U /\ y e. U ) ) -> ( ( ( X ` x ) x. ( X ` y ) ) = 0 <-> ( ( X ` x ) = 0 \/ ( X ` y ) = 0 ) ) )
75 69 74 mpbird 
 |-  ( ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x e. U /\ y e. U ) ) -> ( ( X ` x ) x. ( X ` y ) ) = 0 )
76 58 75 eqtr4d 
 |-  ( ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x e. U /\ y e. U ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
77 76 a1d 
 |-  ( ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x e. U /\ y e. U ) ) -> ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
78 76 77 2thd 
 |-  ( ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) /\ -. ( x e. U /\ y e. U ) ) -> ( ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) <-> ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) )
79 41 78 pm2.61dan 
 |-  ( ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) /\ ( x e. B /\ y e. B ) ) -> ( ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) <-> ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) )
80 79 pm5.74da 
 |-  ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) -> ( ( ( x e. B /\ y e. B ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) <-> ( ( x e. B /\ y e. B ) -> ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) ) )
81 3 4 unitcl 
 |-  ( x e. U -> x e. B )
82 3 4 unitcl 
 |-  ( y e. U -> y e. B )
83 81 82 anim12i 
 |-  ( ( x e. U /\ y e. U ) -> ( x e. B /\ y e. B ) )
84 83 pm4.71ri 
 |-  ( ( x e. U /\ y e. U ) <-> ( ( x e. B /\ y e. B ) /\ ( x e. U /\ y e. U ) ) )
85 84 imbi1i 
 |-  ( ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) <-> ( ( ( x e. B /\ y e. B ) /\ ( x e. U /\ y e. U ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
86 impexp 
 |-  ( ( ( ( x e. B /\ y e. B ) /\ ( x e. U /\ y e. U ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) <-> ( ( x e. B /\ y e. B ) -> ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) )
87 85 86 bitri 
 |-  ( ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) <-> ( ( x e. B /\ y e. B ) -> ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) )
88 80 87 bitr4di 
 |-  ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) -> ( ( ( x e. B /\ y e. B ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) <-> ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) )
89 88 2albidv 
 |-  ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) -> ( A. x A. y ( ( x e. B /\ y e. B ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) <-> A. x A. y ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) )
90 r2al 
 |-  ( A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) <-> A. x A. y ( ( x e. B /\ y e. B ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
91 r2al 
 |-  ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) <-> A. x A. y ( ( x e. U /\ y e. U ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
92 89 90 91 3bitr4g 
 |-  ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ X : B --> CC ) -> ( A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) <-> A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
93 92 adantrr 
 |-  ( ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) /\ ( X : B --> CC /\ ( X ` ( 1r ` Z ) ) = 1 ) ) -> ( A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) <-> A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
94 93 pm5.32da 
 |-  ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) -> ( ( ( X : B --> CC /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) <-> ( ( X : B --> CC /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) ) )
95 3anan32 
 |-  ( ( X : B --> CC /\ A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) <-> ( ( X : B --> CC /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
96 an31 
 |-  ( ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ X : B --> CC ) <-> ( ( X : B --> CC /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
97 94 95 96 3bitr4g 
 |-  ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) -> ( ( X : B --> CC /\ A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) <-> ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ X : B --> CC ) ) )
98 39 97 bitrd 
 |-  ( ( ph /\ A. z e. B ( ( X ` z ) =/= 0 -> z e. U ) ) -> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) <-> ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ X : B --> CC ) ) )
99 12 98 sylan2br 
 |-  ( ( ph /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) -> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) <-> ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ X : B --> CC ) ) )
100 99 pm5.32da 
 |-  ( ph -> ( ( A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) <-> ( A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) /\ ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ X : B --> CC ) ) ) )
101 ancom 
 |-  ( ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) <-> ( A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) )
102 df-3an 
 |-  ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) <-> ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) )
103 102 anbi2i 
 |-  ( ( X : B --> CC /\ ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) <-> ( X : B --> CC /\ ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) )
104 an13 
 |-  ( ( X : B --> CC /\ ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) <-> ( A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) /\ ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ X : B --> CC ) ) )
105 103 104 bitri 
 |-  ( ( X : B --> CC /\ ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) <-> ( A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) /\ ( ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 ) /\ X : B --> CC ) ) )
106 100 101 105 3bitr4g 
 |-  ( ph -> ( ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) <-> ( X : B --> CC /\ ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) ) )
107 7 106 bitrd 
 |-  ( ph -> ( X e. D <-> ( X : B --> CC /\ ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) ) )