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 โŠข โ„ฒ ๐‘˜ ๐œ‘
fprodeq0g.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ Fin )
fprodeq0g.b โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด ) โ†’ ๐ต โˆˆ โ„‚ )
fprodeq0g.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ ๐ด )
fprodeq0g.b0 โŠข ( ( ๐œ‘ โˆง ๐‘˜ = ๐ถ ) โ†’ ๐ต = 0 )
Assertion fprodeq0g ( ๐œ‘ โ†’ โˆ ๐‘˜ โˆˆ ๐ด ๐ต = 0 )

Proof

Step Hyp Ref Expression
1 fprodeq0g.kph โŠข โ„ฒ ๐‘˜ ๐œ‘
2 fprodeq0g.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ Fin )
3 fprodeq0g.b โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด ) โ†’ ๐ต โˆˆ โ„‚ )
4 fprodeq0g.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ ๐ด )
5 fprodeq0g.b0 โŠข ( ( ๐œ‘ โˆง ๐‘˜ = ๐ถ ) โ†’ ๐ต = 0 )
6 nfcvd โŠข ( ๐œ‘ โ†’ โ„ฒ ๐‘˜ 0 )
7 1 6 2 3 4 5 fprodsplit1f โŠข ( ๐œ‘ โ†’ โˆ ๐‘˜ โˆˆ ๐ด ๐ต = ( 0 ยท โˆ ๐‘˜ โˆˆ ( ๐ด โˆ– { ๐ถ } ) ๐ต ) )
8 diffi โŠข ( ๐ด โˆˆ Fin โ†’ ( ๐ด โˆ– { ๐ถ } ) โˆˆ Fin )
9 2 8 syl โŠข ( ๐œ‘ โ†’ ( ๐ด โˆ– { ๐ถ } ) โˆˆ Fin )
10 eldifi โŠข ( ๐‘˜ โˆˆ ( ๐ด โˆ– { ๐ถ } ) โ†’ ๐‘˜ โˆˆ ๐ด )
11 10 3 sylan2 โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ด โˆ– { ๐ถ } ) ) โ†’ ๐ต โˆˆ โ„‚ )
12 1 9 11 fprodclf โŠข ( ๐œ‘ โ†’ โˆ ๐‘˜ โˆˆ ( ๐ด โˆ– { ๐ถ } ) ๐ต โˆˆ โ„‚ )
13 12 mul02d โŠข ( ๐œ‘ โ†’ ( 0 ยท โˆ ๐‘˜ โˆˆ ( ๐ด โˆ– { ๐ถ } ) ๐ต ) = 0 )
14 7 13 eqtrd โŠข ( ๐œ‘ โ†’ โˆ ๐‘˜ โˆˆ ๐ด ๐ต = 0 )