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	sselid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( .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	sselid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝐵 )
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	sselid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝐵 )
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	sselid	⊢ ( 𝜑 → ( 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 ) ) ∈ 𝐷 )