Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
โข ( ( ๐ โ ( mzPolyCld โ ๐ ) โง ๐น โ ๐ ) โ ๐น โ ๐ ) |
2 |
|
simpl |
โข ( ( ๐ โ ( mzPolyCld โ ๐ ) โง ๐น โ ๐ ) โ ๐ โ ( mzPolyCld โ ๐ ) ) |
3 |
|
elfvex |
โข ( ๐ โ ( mzPolyCld โ ๐ ) โ ๐ โ V ) |
4 |
3
|
adantr |
โข ( ( ๐ โ ( mzPolyCld โ ๐ ) โง ๐น โ ๐ ) โ ๐ โ V ) |
5 |
|
elmzpcl |
โข ( ๐ โ V โ ( ๐ โ ( mzPolyCld โ ๐ ) โ ( ๐ โ ( โค โm ( โค โm ๐ ) ) โง ( ( โ ๐ โ โค ( ( โค โm ๐ ) ร { ๐ } ) โ ๐ โง โ ๐ โ ๐ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐ ) ) โ ๐ ) โง โ ๐ โ ๐ โ ๐ โ ๐ ( ( ๐ โf + ๐ ) โ ๐ โง ( ๐ โf ยท ๐ ) โ ๐ ) ) ) ) ) |
6 |
4 5
|
syl |
โข ( ( ๐ โ ( mzPolyCld โ ๐ ) โง ๐น โ ๐ ) โ ( ๐ โ ( mzPolyCld โ ๐ ) โ ( ๐ โ ( โค โm ( โค โm ๐ ) ) โง ( ( โ ๐ โ โค ( ( โค โm ๐ ) ร { ๐ } ) โ ๐ โง โ ๐ โ ๐ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐ ) ) โ ๐ ) โง โ ๐ โ ๐ โ ๐ โ ๐ ( ( ๐ โf + ๐ ) โ ๐ โง ( ๐ โf ยท ๐ ) โ ๐ ) ) ) ) ) |
7 |
2 6
|
mpbid |
โข ( ( ๐ โ ( mzPolyCld โ ๐ ) โง ๐น โ ๐ ) โ ( ๐ โ ( โค โm ( โค โm ๐ ) ) โง ( ( โ ๐ โ โค ( ( โค โm ๐ ) ร { ๐ } ) โ ๐ โง โ ๐ โ ๐ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐ ) ) โ ๐ ) โง โ ๐ โ ๐ โ ๐ โ ๐ ( ( ๐ โf + ๐ ) โ ๐ โง ( ๐ โf ยท ๐ ) โ ๐ ) ) ) ) |
8 |
|
simprlr |
โข ( ( ๐ โ ( โค โm ( โค โm ๐ ) ) โง ( ( โ ๐ โ โค ( ( โค โm ๐ ) ร { ๐ } ) โ ๐ โง โ ๐ โ ๐ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐ ) ) โ ๐ ) โง โ ๐ โ ๐ โ ๐ โ ๐ ( ( ๐ โf + ๐ ) โ ๐ โง ( ๐ โf ยท ๐ ) โ ๐ ) ) ) โ โ ๐ โ ๐ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐ ) ) โ ๐ ) |
9 |
7 8
|
syl |
โข ( ( ๐ โ ( mzPolyCld โ ๐ ) โง ๐น โ ๐ ) โ โ ๐ โ ๐ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐ ) ) โ ๐ ) |
10 |
|
fveq2 |
โข ( ๐ = ๐น โ ( ๐ โ ๐ ) = ( ๐ โ ๐น ) ) |
11 |
10
|
mpteq2dv |
โข ( ๐ = ๐น โ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐ ) ) = ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐น ) ) ) |
12 |
11
|
eleq1d |
โข ( ๐ = ๐น โ ( ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐ ) ) โ ๐ โ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐น ) ) โ ๐ ) ) |
13 |
12
|
rspcva |
โข ( ( ๐น โ ๐ โง โ ๐ โ ๐ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐ ) ) โ ๐ ) โ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐น ) ) โ ๐ ) |
14 |
1 9 13
|
syl2anc |
โข ( ( ๐ โ ( mzPolyCld โ ๐ ) โง ๐น โ ๐ ) โ ( ๐ โ ( โค โm ๐ ) โฆ ( ๐ โ ๐น ) ) โ ๐ ) |