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

Metamath Proof Explorer

Theorem fprod0

Description: A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 fprod0.kph 
 |-  F/ k ph
2 fprod0.kc 
 |-  F/_ k C
3 fprod0.a 
 |-  ( ph -> A e. Fin )
4 fprod0.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
5 fprod0.bc 
 |-  ( k = K -> B = C )
6 fprod0.k 
 |-  ( ph -> K e. A )
7 fprod0.c 
 |-  ( ph -> C = 0 )
8 2 a1i 
 |-  ( ph -> F/_ k C )
9 5 adantl 
 |-  ( ( ph /\ k = K ) -> B = C )
10 1 8 3 4 6 9 fprodsplit1f 
 |-  ( ph -> prod_ k e. A B = ( C x. prod_ k e. ( A \ { K } ) B ) )
11 7 oveq1d 
 |-  ( ph -> ( C x. prod_ k e. ( A \ { K } ) B ) = ( 0 x. prod_ k e. ( A \ { K } ) B ) )
12 diffi 
 |-  ( A e. Fin -> ( A \ { K } ) e. Fin )
13 3 12 syl 
 |-  ( ph -> ( A \ { K } ) e. Fin )
14 simpl 
 |-  ( ( ph /\ k e. ( A \ { K } ) ) -> ph )
15 eldifi 
 |-  ( k e. ( A \ { K } ) -> k e. A )
16 15 adantl 
 |-  ( ( ph /\ k e. ( A \ { K } ) ) -> k e. A )
17 14 16 4 syl2anc 
 |-  ( ( ph /\ k e. ( A \ { K } ) ) -> B e. CC )
18 1 13 17 fprodclf 
 |-  ( ph -> prod_ k e. ( A \ { K } ) B e. CC )
19 18 mul02d 
 |-  ( ph -> ( 0 x. prod_ k e. ( A \ { K } ) B ) = 0 )
20 10 11 19 3eqtrd 
 |-  ( ph -> prod_ k e. A B = 0 )