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

Metamath Proof Explorer

Theorem fprodeq0g

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

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

Proof

Step Hyp Ref Expression
1 fprodeq0g.kph 
 |-  F/ k ph
2 fprodeq0g.a 
 |-  ( ph -> A e. Fin )
3 fprodeq0g.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 fprodeq0g.c 
 |-  ( ph -> C e. A )
5 fprodeq0g.b0 
 |-  ( ( ph /\ k = C ) -> B = 0 )
6 nfcvd 
 |-  ( ph -> F/_ k 0 )
7 1 6 2 3 4 5 fprodsplit1f 
 |-  ( ph -> prod_ k e. A B = ( 0 x. prod_ k e. ( A \ { C } ) B ) )
8 diffi 
 |-  ( A e. Fin -> ( A \ { C } ) e. Fin )
9 2 8 syl 
 |-  ( ph -> ( A \ { C } ) e. Fin )
10 eldifi 
 |-  ( k e. ( A \ { C } ) -> k e. A )
11 10 3 sylan2 
 |-  ( ( ph /\ k e. ( A \ { C } ) ) -> B e. CC )
12 1 9 11 fprodclf 
 |-  ( ph -> prod_ k e. ( A \ { C } ) B e. CC )
13 12 mul02d 
 |-  ( ph -> ( 0 x. prod_ k e. ( A \ { C } ) B ) = 0 )
14 7 13 eqtrd 
 |-  ( ph -> prod_ k e. A B = 0 )