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 
|- F/ x ph
iblsplitf.vol 
|- ( ph -> ( vol* ` ( A i^i B ) ) = 0 )
iblsplitf.u 
|- ( ph -> U = ( A u. B ) )
iblsplitf.c 
|- ( ( ph /\ x e. U ) -> C e. CC )
iblsplitf.a 
|- ( ph -> ( x e. A |-> C ) e. L^1 )
iblsplitf.b 
|- ( ph -> ( x e. B |-> C ) e. L^1 )
Assertion iblsplitf 
|- ( ph -> ( x e. U |-> C ) e. L^1 )

Proof

Step Hyp Ref Expression
1 iblsplitf.X 
 |-  F/ x ph
2 iblsplitf.vol 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) = 0 )
3 iblsplitf.u 
 |-  ( ph -> U = ( A u. B ) )
4 iblsplitf.c 
 |-  ( ( ph /\ x e. U ) -> C e. CC )
5 iblsplitf.a 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )
6 iblsplitf.b 
 |-  ( ph -> ( x e. B |-> C ) e. L^1 )
7 nfcv 
 |-  F/_ y C
8 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
9 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
10 7 8 9 cbvmpt 
 |-  ( x e. U |-> C ) = ( y e. U |-> [_ y / x ]_ C )
11 simpr 
 |-  ( ( ph /\ y e. U ) -> y e. U )
12 nfv 
 |-  F/ x y e. U
13 1 12 nfan 
 |-  F/ x ( ph /\ y e. U )
14 4 adantlr 
 |-  ( ( ( ph /\ y e. U ) /\ x e. U ) -> C e. CC )
15 14 ex 
 |-  ( ( ph /\ y e. U ) -> ( x e. U -> C e. CC ) )
16 13 15 ralrimi 
 |-  ( ( ph /\ y e. U ) -> A. x e. U C e. CC )
17 rspcsbela 
 |-  ( ( y e. U /\ A. x e. U C e. CC ) -> [_ y / x ]_ C e. CC )
18 11 16 17 syl2anc 
 |-  ( ( ph /\ y e. U ) -> [_ y / x ]_ C e. CC )
19 9 equcoms 
 |-  ( y = x -> C = [_ y / x ]_ C )
20 19 eqcomd 
 |-  ( y = x -> [_ y / x ]_ C = C )
21 8 7 20 cbvmpt 
 |-  ( y e. A |-> [_ y / x ]_ C ) = ( x e. A |-> C )
22 21 5 eqeltrid 
 |-  ( ph -> ( y e. A |-> [_ y / x ]_ C ) e. L^1 )
23 8 7 20 cbvmpt 
 |-  ( y e. B |-> [_ y / x ]_ C ) = ( x e. B |-> C )
24 23 6 eqeltrid 
 |-  ( ph -> ( y e. B |-> [_ y / x ]_ C ) e. L^1 )
25 2 3 18 22 24 iblsplit 
 |-  ( ph -> ( y e. U |-> [_ y / x ]_ C ) e. L^1 )
26 10 25 eqeltrid 
 |-  ( ph -> ( x e. U |-> C ) e. L^1 )