Theorem esplymhp

Description: The K -th elementary symmetric polynomial is homogeneous of degree K . (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	esplympl.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	esplympl.i	$$⊢\phi \to I\in \mathrm{Fin}$$
	esplympl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	esplympl.k	$$⊢\phi \to K\in {\mathbb{N}}_0$$
	esplymhp.1	$$⊢H=I\mathrm{mHomP}R$$
Assertion	esplymhp	Could not format assertion : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) e. ( H ` K ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		esplympl.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
2		esplympl.i	$$⊢\phi \to I\in \mathrm{Fin}$$
3		esplympl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		esplympl.k	$$⊢\phi \to K\in {\mathbb{N}}_0$$
5		esplymhp.1	$$⊢H=I\mathrm{mHomP}R$$
6	2	ad2antrr	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> I e. Fin ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> I e. Fin ) with typecode |-
7		simpr	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( _Ind ` I ) ` b ) = d ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( _Ind ` I ) ` b ) = d ) with typecode |-
8	6	ad2antrr	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> I e. Fin ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> I e. Fin ) with typecode |-
9		ssrab2	$$⊢\left\{c\in 𝒫I|\left|c\right|=K\right\}\subseteq 𝒫I$$
10	9	a1i	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> { c e. ~P I | ( # ` c ) = K } C_ ~P I ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> { c e. ~P I | ( # ` c ) = K } C_ ~P I ) with typecode |-
11	10	sselda	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) -> b e. ~P I ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) -> b e. ~P I ) with typecode |-
12	11	elpwid	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) -> b C_ I ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) -> b C_ I ) with typecode |-
13	12	adantr	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> b C_ I ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> b C_ I ) with typecode |-
14		indf	$$⊢\left(I\in \mathrm{Fin}\wedge b\subseteq I\right)\to {𝟙}_I\left(b\right):I⟶\left\{0,1\right\}$$
15	8 13 14	syl2anc	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( _Ind ` I ) ` b ) : I --> { 0 , 1 } ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( _Ind ` I ) ` b ) : I --> { 0 , 1 } ) with typecode |-
16	7 15	feq1dd	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> d : I --> { 0 , 1 } ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> d : I --> { 0 , 1 } ) with typecode |-
17		indf1o	$$⊢I\in \mathrm{Fin}\to {𝟙}_I:𝒫I\underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^I$$
18		f1of	$$⊢{𝟙}_I:𝒫I\underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^I\to {𝟙}_I:𝒫I⟶{\left\{0,1\right\}}^I$$
19	2 17 18	3syl	$$⊢\phi \to {𝟙}_I:𝒫I⟶{\left\{0,1\right\}}^I$$
20	19	ffund	$$⊢\phi \to \mathrm{Fun}{𝟙}_I$$
21	20	ad2antrr	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> Fun ( _Ind ` I ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> Fun ( _Ind ` I ) ) with typecode |-
22		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
23	1	ssrab3	$$⊢D\subseteq {{\mathbb{N}}_0}^I$$
24	22 23	ssexi	$$⊢D\in \mathrm{V}$$
25	24	a1i	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> D e. _V ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> D e. _V ) with typecode |-
26	3	ad2antrr	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> R e. Ring ) with typecode |-
27	4	ad2antrr	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> K e. NN0 ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> K e. NN0 ) with typecode |-
28	1 6 26 27	esplylem	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D ) with typecode |-
29		simplr	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d e. D ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d e. D ) with typecode |-
30		simpr	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) with typecode |-
31	30	neneqd	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> -. ( ( ( I eSymPoly R ) ` K ) ` d ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> -. ( ( ( I eSymPoly R ) ` K ) ` d ) = ( 0g ` R ) ) with typecode |-
32		indf	$$⊢\left(D\in \mathrm{V}\wedge {𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\subseteq D\right)\to {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right):D⟶\left\{0,1\right\}$$
33	25 28 32	syl2anc	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } ) with typecode |-
34	33	adantr	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } ) with typecode |-
35	29	adantr	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> d e. D ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> d e. D ) with typecode |-
36	34 35	ffvelcdmd	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) e. { 0 , 1 } ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) e. { 0 , 1 } ) with typecode |-
37		simpr	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) with typecode |-
38		elprn2	$$⊢\left({𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)\left(d\right)\in \left\{0,1\right\}\wedge {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)\left(d\right)\ne 1\right)\to {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)\left(d\right)=0$$
39	36 37 38	syl2anc	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) = 0 ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) = 0 ) with typecode |-
40	39	fveq2d	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) = ( ( ZRHom ` R ) ` 0 ) ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) = ( ( ZRHom ` R ) ` 0 ) ) with typecode |-
41		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(R\right)=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
42		eqid	$$⊢0_R=0_R$$
43	41 42	zrh0	$$⊢R\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(R\right)\left(0\right)=0_R$$
44	3 43	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(R\right)\left(0\right)=0_R$$
45	44	ad3antrrr	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) ) with typecode |-
46	40 45	eqtrd	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) = ( 0g ` R ) ) with typecode |-
47	1 2 3 4	esplyfval	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) with typecode |-
48	47	ad2antrr	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) with typecode |-
49	48	fveq1d	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) = ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` d ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) = ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` d ) ) with typecode |-
50	33 29	fvco3d	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` d ) = ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` d ) = ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) ) with typecode |-
51	49 50	eqtrd	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) = ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) = ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) ) with typecode |-
52	51 30	eqnetrrd	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) =/= ( 0g ` R ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) =/= ( 0g ` R ) ) with typecode |-
53	52	adantr	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) =/= ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) =/= ( 0g ` R ) ) with typecode |-
54	46 53	pm2.21ddne	Could not format ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) = ( 0g ` R ) ) with typecode |-
55	31 54	mtand	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> -. ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> -. ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) with typecode |-
56		nne	$$⊢\neg {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)\left(d\right)\ne 1\leftrightarrow {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)\left(d\right)=1$$
57	55 56	sylib	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) = 1 ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) = 1 ) with typecode |-
58		ind1a	$$⊢\left(D\in \mathrm{V}\wedge {𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\subseteq D\wedge d\in D\right)\to \left({𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)\left(d\right)=1\leftrightarrow d\in {𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)$$
59	58	biimpa	$$⊢\left(\left(D\in \mathrm{V}\wedge {𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\subseteq D\wedge d\in D\right)\wedge {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)\left(d\right)=1\right)\to d\in {𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]$$
60	25 28 29 57 59	syl31anc	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) with typecode |-
61		fvelima	$$⊢\left(\mathrm{Fun}{𝟙}_I\wedge d\in {𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)\to \exists b\in \left\{c\in 𝒫I|\left|c\right|=K\right\}{𝟙}_I\left(b\right)=d$$
62	21 60 61	syl2anc	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> E. b e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` b ) = d ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> E. b e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` b ) = d ) with typecode |-
63	16 62	r19.29a	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d : I --> { 0 , 1 } ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d : I --> { 0 , 1 } ) with typecode |-
64	6 63	indfsid	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d = ( ( _Ind ` I ) ` ( d supp 0 ) ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d = ( ( _Ind ` I ) ` ( d supp 0 ) ) ) with typecode |-
65	64	oveq2d	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum d ) = ( CCfld gsum ( ( _Ind ` I ) ` ( d supp 0 ) ) ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum d ) = ( CCfld gsum ( ( _Ind ` I ) ` ( d supp 0 ) ) ) ) with typecode |-
66		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
67	66	a1i	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> NN0 e. ( SubMnd ` CCfld ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> NN0 e. ( SubMnd ` CCfld ) ) with typecode |-
68	23	a1i	$$⊢\phi \to D\subseteq {{\mathbb{N}}_0}^I$$
69	68	sselda	$$⊢\left(\phi \wedge d\in D\right)\to d\in \left({{\mathbb{N}}_0}^I\right)$$
70	69	adantr	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d e. ( NN0 ^m I ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d e. ( NN0 ^m I ) ) with typecode |-
71	6 67 70	elmaprd	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d : I --> NN0 ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d : I --> NN0 ) with typecode |-
72		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
73	6 67 71 72	gsumsubm	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum d ) = ( ( CCfld |`s NN0 ) gsum d ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum d ) = ( ( CCfld |`s NN0 ) gsum d ) ) with typecode |-
74		suppssdm	$$⊢d\mathrm{supp}0\subseteq \mathrm{dom}d$$
75	2	adantr	$$⊢\left(\phi \wedge d\in D\right)\to I\in \mathrm{Fin}$$
76		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
77	76	a1i	$$⊢\left(\phi \wedge d\in D\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
78	75 77 69	elmaprd	$$⊢\left(\phi \wedge d\in D\right)\to d:I⟶{\mathbb{N}}_0$$
79	78	fdmd	$$⊢\left(\phi \wedge d\in D\right)\to \mathrm{dom}d=I$$
80	79	adantr	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> dom d = I ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> dom d = I ) with typecode |-
81	74 80	sseqtrid	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( d supp 0 ) C_ I ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( d supp 0 ) C_ I ) with typecode |-
82	6 81	ssfid	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( d supp 0 ) e. Fin ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( d supp 0 ) e. Fin ) with typecode |-
83	6 81 82	gsumind	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum ( ( _Ind ` I ) ` ( d supp 0 ) ) ) = ( # ` ( d supp 0 ) ) ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum ( ( _Ind ` I ) ` ( d supp 0 ) ) ) = ( # ` ( d supp 0 ) ) ) with typecode |-
84	7	oveq1d	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( ( _Ind ` I ) ` b ) supp 0 ) = ( d supp 0 ) ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( ( _Ind ` I ) ` b ) supp 0 ) = ( d supp 0 ) ) with typecode |-
85		indsupp	$$⊢\left(I\in \mathrm{Fin}\wedge b\subseteq I\right)\to {𝟙}_I\left(b\right)\mathrm{supp}0=b$$
86	8 13 85	syl2anc	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( ( _Ind ` I ) ` b ) supp 0 ) = b ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( ( _Ind ` I ) ` b ) supp 0 ) = b ) with typecode |-
87	84 86	eqtr3d	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( d supp 0 ) = b ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( d supp 0 ) = b ) with typecode |-
88	87	fveq2d	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( # ` ( d supp 0 ) ) = ( # ` b ) ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( # ` ( d supp 0 ) ) = ( # ` b ) ) with typecode |-
89		fveqeq2	$$⊢c=b\to \left(\left|c\right|=K\leftrightarrow \left|b\right|=K\right)$$
90		simplr	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> b e. { c e. ~P I | ( # ` c ) = K } ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> b e. { c e. ~P I | ( # ` c ) = K } ) with typecode |-
91	89 90	elrabrd	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( # ` b ) = K ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( # ` b ) = K ) with typecode |-
92	88 91	eqtrd	Could not format ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( # ` ( d supp 0 ) ) = K ) : No typesetting found for |- ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( # ` ( d supp 0 ) ) = K ) with typecode |-
93	92 62	r19.29a	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( # ` ( d supp 0 ) ) = K ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( # ` ( d supp 0 ) ) = K ) with typecode |-
94	83 93	eqtrd	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum ( ( _Ind ` I ) ` ( d supp 0 ) ) ) = K ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum ( ( _Ind ` I ) ` ( d supp 0 ) ) ) = K ) with typecode |-
95	65 73 94	3eqtr3d	Could not format ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) : No typesetting found for |- ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) with typecode |-
96	95	ex	Could not format ( ( ph /\ d e. D ) -> ( ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) ) : No typesetting found for |- ( ( ph /\ d e. D ) -> ( ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) ) with typecode |-
97	96	ralrimiva	Could not format ( ph -> A. d e. D ( ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) ) : No typesetting found for |- ( ph -> A. d e. D ( ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) ) with typecode |-
98		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
99		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
100	1	psrbasfsupp	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
101	1 2 3 4 99	esplympl	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPoly R ) ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPoly R ) ) ) with typecode |-
102	5 98 99 42 100 4 101	ismhp3	Could not format ( ph -> ( ( ( I eSymPoly R ) ` K ) e. ( H ` K ) <-> A. d e. D ( ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) ) ) : No typesetting found for |- ( ph -> ( ( ( I eSymPoly R ) ` K ) e. ( H ` K ) <-> A. d e. D ( ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) ) ) with typecode |-
103	97 102	mpbird	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) e. ( H ` K ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) e. ( H ` K ) ) with typecode |-