Metamath Proof Explorer

Theorem fproddivf

Description: The quotient of two finite products. A version of fproddiv using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fproddivf.kph 
|- F/ k ph
fproddivf.a 
|- ( ph -> A e. Fin )
fproddivf.b 
|- ( ( ph /\ k e. A ) -> B e. CC )
fproddivf.c 
|- ( ( ph /\ k e. A ) -> C e. CC )
fproddivf.ne0 
|- ( ( ph /\ k e. A ) -> C =/= 0 )
Assertion fproddivf 
|- ( ph -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) )

Proof

Step Hyp Ref Expression
1 fproddivf.kph 
 |-  F/ k ph
2 fproddivf.a 
 |-  ( ph -> A e. Fin )
3 fproddivf.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 fproddivf.c 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
5 fproddivf.ne0 
 |-  ( ( ph /\ k e. A ) -> C =/= 0 )
6 nfcv 
 |-  F/_ j ( B / C )
7 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
8 nfcv 
 |-  F/_ k /
9 nfcsb1v 
 |-  F/_ k [_ j / k ]_ C
10 7 8 9 nfov 
 |-  F/_ k ( [_ j / k ]_ B / [_ j / k ]_ C )
11 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
12 csbeq1a 
 |-  ( k = j -> C = [_ j / k ]_ C )
13 11 12 oveq12d 
 |-  ( k = j -> ( B / C ) = ( [_ j / k ]_ B / [_ j / k ]_ C ) )
14 6 10 13 cbvprodi 
 |-  prod_ k e. A ( B / C ) = prod_ j e. A ( [_ j / k ]_ B / [_ j / k ]_ C )
15 14 a1i 
 |-  ( ph -> prod_ k e. A ( B / C ) = prod_ j e. A ( [_ j / k ]_ B / [_ j / k ]_ C ) )
16 nfvd 
 |-  ( ph -> F/ k j e. A )
17 1 16 nfan1 
 |-  F/ k ( ph /\ j e. A )
18 7 nfel1 
 |-  F/ k [_ j / k ]_ B e. CC
19 17 18 nfim 
 |-  F/ k ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
20 eleq1w 
 |-  ( k = j -> ( k e. A <-> j e. A ) )
21 20 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. A ) <-> ( ph /\ j e. A ) ) )
22 11 eleq1d 
 |-  ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
23 21 22 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. A ) -> B e. CC ) <-> ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC ) ) )
24 19 23 3 chvarfv 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
25 9 nfel1 
 |-  F/ k [_ j / k ]_ C e. CC
26 17 25 nfim 
 |-  F/ k ( ( ph /\ j e. A ) -> [_ j / k ]_ C e. CC )
27 12 eleq1d 
 |-  ( k = j -> ( C e. CC <-> [_ j / k ]_ C e. CC ) )
28 21 27 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. A ) -> C e. CC ) <-> ( ( ph /\ j e. A ) -> [_ j / k ]_ C e. CC ) ) )
29 26 28 4 chvarfv 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ C e. CC )
30 nfcv 
 |-  F/_ k 0
31 9 30 nfne 
 |-  F/ k [_ j / k ]_ C =/= 0
32 17 31 nfim 
 |-  F/ k ( ( ph /\ j e. A ) -> [_ j / k ]_ C =/= 0 )
33 12 neeq1d 
 |-  ( k = j -> ( C =/= 0 <-> [_ j / k ]_ C =/= 0 ) )
34 21 33 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. A ) -> C =/= 0 ) <-> ( ( ph /\ j e. A ) -> [_ j / k ]_ C =/= 0 ) ) )
35 32 34 5 chvarfv 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ C =/= 0 )
36 2 24 29 35 fproddiv 
 |-  ( ph -> prod_ j e. A ( [_ j / k ]_ B / [_ j / k ]_ C ) = ( prod_ j e. A [_ j / k ]_ B / prod_ j e. A [_ j / k ]_ C ) )
37 nfcv 
 |-  F/_ j B
38 37 7 11 cbvprodi 
 |-  prod_ k e. A B = prod_ j e. A [_ j / k ]_ B
39 38 eqcomi 
 |-  prod_ j e. A [_ j / k ]_ B = prod_ k e. A B
40 39 a1i 
 |-  ( ph -> prod_ j e. A [_ j / k ]_ B = prod_ k e. A B )
41 nfcv 
 |-  F/_ j C
42 12 equcoms 
 |-  ( j = k -> C = [_ j / k ]_ C )
43 42 eqcomd 
 |-  ( j = k -> [_ j / k ]_ C = C )
44 9 41 43 cbvprodi 
 |-  prod_ j e. A [_ j / k ]_ C = prod_ k e. A C
45 44 a1i 
 |-  ( ph -> prod_ j e. A [_ j / k ]_ C = prod_ k e. A C )
46 40 45 oveq12d 
 |-  ( ph -> ( prod_ j e. A [_ j / k ]_ B / prod_ j e. A [_ j / k ]_ C ) = ( prod_ k e. A B / prod_ k e. A C ) )
47 15 36 46 3eqtrd 
 |-  ( ph -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) )