This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )