Theorem iblsplitf

Description: A version of iblsplit using bound-variable hypotheses instead of distinct variable conditions". (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	iblsplitf.X	⊢ Ⅎ 𝑥 𝜑
	iblsplitf.vol	⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = 0 )
	iblsplitf.u	⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
	iblsplitf.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
	iblsplitf.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
	iblsplitf.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 )
Assertion	iblsplitf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 ↦ 𝐶 ) ∈ 𝐿1 )

Proof

Step	Hyp	Ref	Expression
1		iblsplitf.X	⊢ Ⅎ 𝑥 𝜑
2		iblsplitf.vol	⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = 0 )
3		iblsplitf.u	⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
4		iblsplitf.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
5		iblsplitf.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
6		iblsplitf.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 )
7		nfcv	⊢ Ⅎ 𝑦 𝐶
8		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
9		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
10	7 8 9	cbvmpt	⊢ ( 𝑥 ∈ 𝑈 ↦ 𝐶 ) = ( 𝑦 ∈ 𝑈 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) → 𝑦 ∈ 𝑈 )
12		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝑈
13	1 12	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝑈 )
14	4	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
15	14	ex	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) → ( 𝑥 ∈ 𝑈 → 𝐶 ∈ ℂ ) )
16	13 15	ralrimi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝑈 𝐶 ∈ ℂ )
17		rspcsbela	⊢ ( ( 𝑦 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 𝐶 ∈ ℂ ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ℂ )
18	11 16 17	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ℂ )
19	9	equcoms	⊢ ( 𝑦 = 𝑥 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
20	19	eqcomd	⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = 𝐶 )
21	8 7 20	cbvmpt	⊢ ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
22	21 5	eqeltrid	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ∈ 𝐿1 )
23	8 7 20	cbvmpt	⊢ ( 𝑦 ∈ 𝐵 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
24	23 6	eqeltrid	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ∈ 𝐿1 )
25	2 3 18 22 24	iblsplit	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑈 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ∈ 𝐿1 )
26	10 25	eqeltrid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 ↦ 𝐶 ) ∈ 𝐿1 )