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 ) |