Metamath Proof Explorer

Theorem dchrelbasd

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, 28-Apr-2016)

Ref Expression
Hypotheses dchrval.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrval.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrval.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
dchrval.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
dchrval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dchrbas.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrelbasd.1 ⊢ ( 𝑘 = 𝑥 → 𝑋 = 𝐴 )
dchrelbasd.2 ⊢ ( 𝑘 = 𝑦 → 𝑋 = 𝐶 )
dchrelbasd.3 ⊢ ( 𝑘 = ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) → 𝑋 = 𝐸 )
dchrelbasd.4 ⊢ ( 𝑘 = ( 1r ‘ 𝑍 ) → 𝑋 = 𝑌 )
dchrelbasd.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝑋 ∈ ℂ )
dchrelbasd.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐸 = ( 𝐴 · 𝐶 ) )
dchrelbasd.7 ⊢ ( 𝜑 → 𝑌 = 1 )
Assertion dchrelbasd ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 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 dchrelbasd.1 ⊢ ( 𝑘 = 𝑥 → 𝑋 = 𝐴 )
8 dchrelbasd.2 ⊢ ( 𝑘 = 𝑦 → 𝑋 = 𝐶 )
9 dchrelbasd.3 ⊢ ( 𝑘 = ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) → 𝑋 = 𝐸 )
10 dchrelbasd.4 ⊢ ( 𝑘 = ( 1r ‘ 𝑍 ) → 𝑋 = 𝑌 )
11 dchrelbasd.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝑋 ∈ ℂ )
12 dchrelbasd.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐸 = ( 𝐴 · 𝐶 ) )
13 dchrelbasd.7 ⊢ ( 𝜑 → 𝑌 = 1 )
14 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝑈 ) → 𝑋 ∈ ℂ )
15 0cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ ¬ 𝑘 ∈ 𝑈 ) → 0 ∈ ℂ )
16 14 15 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ∈ ℂ )
17 16 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) : 𝐵 ⟶ ℂ )
18 5 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
19 2 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
20 crngring ⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
21 18 19 20 3syl ⊢ ( 𝜑 → 𝑍 ∈ Ring )
22 eqid ⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 )
23 4 22 unitmulcl ⊢ ( ( 𝑍 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 )
24 23 3expb ⊢ ( ( 𝑍 ∈ Ring ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 )
25 21 24 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 )
26 25 iftrued ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → if ( ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 , 𝐸 , 0 ) = 𝐸 )
27 26 12 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → if ( ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 , 𝐸 , 0 ) = ( 𝐴 · 𝐶 ) )
28 eqid ⊢ ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) )
29 eleq1 ⊢ ( 𝑘 = ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) → ( 𝑘 ∈ 𝑈 ↔ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 ) )
30 29 9 ifbieq1d ⊢ ( 𝑘 = ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) → if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) = if ( ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 , 𝐸 , 0 ) )
31 3 4 unitss ⊢ 𝑈 ⊆ 𝐵
32 31 25 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝐵 )
33 9 eleq1d ⊢ ( 𝑘 = ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) → ( 𝑋 ∈ ℂ ↔ 𝐸 ∈ ℂ ) )
34 11 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑈 𝑋 ∈ ℂ )
35 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ∀ 𝑘 ∈ 𝑈 𝑋 ∈ ℂ )
36 33 35 25 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐸 ∈ ℂ )
37 26 36 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → if ( ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 , 𝐸 , 0 ) ∈ ℂ )
38 28 30 32 37 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = if ( ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 , 𝐸 , 0 ) )
39 eleq1 ⊢ ( 𝑘 = 𝑥 → ( 𝑘 ∈ 𝑈 ↔ 𝑥 ∈ 𝑈 ) )
40 39 7 ifbieq1d ⊢ ( 𝑘 = 𝑥 → if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) = if ( 𝑥 ∈ 𝑈 , 𝐴 , 0 ) )
41 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝑈 )
42 31 41 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝐵 )
43 iftrue ⊢ ( 𝑥 ∈ 𝑈 → if ( 𝑥 ∈ 𝑈 , 𝐴 , 0 ) = 𝐴 )
44 43 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → if ( 𝑥 ∈ 𝑈 , 𝐴 , 0 ) = 𝐴 )
45 7 eleq1d ⊢ ( 𝑘 = 𝑥 → ( 𝑋 ∈ ℂ ↔ 𝐴 ∈ ℂ ) )
46 45 35 41 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐴 ∈ ℂ )
47 44 46 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → if ( 𝑥 ∈ 𝑈 , 𝐴 , 0 ) ∈ ℂ )
48 28 40 42 47 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐴 , 0 ) )
49 48 44 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) = 𝐴 )
50 eleq1 ⊢ ( 𝑘 = 𝑦 → ( 𝑘 ∈ 𝑈 ↔ 𝑦 ∈ 𝑈 ) )
51 50 8 ifbieq1d ⊢ ( 𝑘 = 𝑦 → if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) = if ( 𝑦 ∈ 𝑈 , 𝐶 , 0 ) )
52 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
53 31 52 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝐵 )
54 iftrue ⊢ ( 𝑦 ∈ 𝑈 → if ( 𝑦 ∈ 𝑈 , 𝐶 , 0 ) = 𝐶 )
55 54 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → if ( 𝑦 ∈ 𝑈 , 𝐶 , 0 ) = 𝐶 )
56 8 eleq1d ⊢ ( 𝑘 = 𝑦 → ( 𝑋 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
57 56 35 52 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐶 ∈ ℂ )
58 55 57 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → if ( 𝑦 ∈ 𝑈 , 𝐶 , 0 ) ∈ ℂ )
59 28 51 53 58 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) = if ( 𝑦 ∈ 𝑈 , 𝐶 , 0 ) )
60 59 55 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) = 𝐶 )
61 49 60 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) · ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) ) = ( 𝐴 · 𝐶 ) )
62 27 38 61 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) · ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) ) )
63 62 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) · ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) ) )
64 eleq1 ⊢ ( 𝑘 = ( 1r ‘ 𝑍 ) → ( 𝑘 ∈ 𝑈 ↔ ( 1r ‘ 𝑍 ) ∈ 𝑈 ) )
65 64 10 ifbieq1d ⊢ ( 𝑘 = ( 1r ‘ 𝑍 ) → if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) = if ( ( 1r ‘ 𝑍 ) ∈ 𝑈 , 𝑌 , 0 ) )
66 eqid ⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
67 4 66 1unit ⊢ ( 𝑍 ∈ Ring → ( 1r ‘ 𝑍 ) ∈ 𝑈 )
68 21 67 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑍 ) ∈ 𝑈 )
69 31 68 sseldi ⊢ ( 𝜑 → ( 1r ‘ 𝑍 ) ∈ 𝐵 )
70 68 iftrued ⊢ ( 𝜑 → if ( ( 1r ‘ 𝑍 ) ∈ 𝑈 , 𝑌 , 0 ) = 𝑌 )
71 70 13 eqtrd ⊢ ( 𝜑 → if ( ( 1r ‘ 𝑍 ) ∈ 𝑈 , 𝑌 , 0 ) = 1 )
72 ax-1cn ⊢ 1 ∈ ℂ
73 71 72 eqeltrdi ⊢ ( 𝜑 → if ( ( 1r ‘ 𝑍 ) ∈ 𝑈 , 𝑌 , 0 ) ∈ ℂ )
74 28 65 69 73 fvmptd3 ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ ( 1r ‘ 𝑍 ) ) = if ( ( 1r ‘ 𝑍 ) ∈ 𝑈 , 𝑌 , 0 ) )
75 74 71 eqtrd ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ ( 1r ‘ 𝑍 ) ) = 1 )
76 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
77 45 rspcv ⊢ ( 𝑥 ∈ 𝑈 → ( ∀ 𝑘 ∈ 𝑈 𝑋 ∈ ℂ → 𝐴 ∈ ℂ ) )
78 34 77 mpan9 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝐴 ∈ ℂ )
79 78 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑈 ) → 𝐴 ∈ ℂ )
80 0cnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ∈ 𝑈 ) → 0 ∈ ℂ )
81 79 80 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ∈ 𝑈 , 𝐴 , 0 ) ∈ ℂ )
82 28 40 76 81 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐴 , 0 ) )
83 82 neeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) ≠ 0 ↔ if ( 𝑥 ∈ 𝑈 , 𝐴 , 0 ) ≠ 0 ) )
84 iffalse ⊢ ( ¬ 𝑥 ∈ 𝑈 → if ( 𝑥 ∈ 𝑈 , 𝐴 , 0 ) = 0 )
85 84 necon1ai ⊢ ( if ( 𝑥 ∈ 𝑈 , 𝐴 , 0 ) ≠ 0 → 𝑥 ∈ 𝑈 )
86 83 85 syl6bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) )
87 86 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) )
88 63 75 87 3jca ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) · ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) ) ∧ ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ ( 1r ‘ 𝑍 ) ) = 1 ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) )
89 1 2 3 4 5 6 dchrelbas3 ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ∈ 𝐷 ↔ ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) : 𝐵 ⟶ ℂ ∧ ( ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) · ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) ) ∧ ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ ( 1r ‘ 𝑍 ) ) = 1 ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) ) ) )
90 17 88 89 mpbir2and ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 𝑋 , 0 ) ) ∈ 𝐷 )