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 = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
	esplympl.i	$⊢ φ \to I \in Fin$
	esplympl.r	$⊢ φ \to R \in Ring$
	esplympl.k	$⊢ φ \to K \in ℕ_{0}$
	esplymhp.1	$⊢ H = I 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 = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
2		esplympl.i	$⊢ φ \to I \in Fin$
3		esplympl.r	$⊢ φ \to R \in Ring$
4		esplympl.k	$⊢ φ \to K \in ℕ_{0}$
5		esplymhp.1	$⊢ H = I 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	$⊢ \{c \in 𝒫 I \| \|c\| = K\} \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	$⊢ (I \in Fin \land b \subseteq I) \to 𝟙_{I} (b) : I ⟶ \{0, 1\}$
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 Fin \to 𝟙_{I} : 𝒫 I \underset{1-1 onto}{⟶} {\{0, 1\}}^{I}$
18		f1of	$⊢ 𝟙_{I} : 𝒫 I \underset{1-1 onto}{⟶} {\{0, 1\}}^{I} \to 𝟙_{I} : 𝒫 I ⟶ {\{0, 1\}}^{I}$
19	2 17 18	3syl	$⊢ φ \to 𝟙_{I} : 𝒫 I ⟶ {\{0, 1\}}^{I}$
20	19	ffund	$⊢ φ \to 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	$⊢ {ℕ_{0}}^{I} \in V$
23	1	ssrab3	$⊢ D \subseteq {ℕ_{0}}^{I}$
24	22 23	ssexi	$⊢ D \in 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	$⊢ (D \in V \land 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ \{0, 1\}$
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	$⊢ (𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (d) \in \{0, 1\} \land 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (d) \neq 1) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (d) = 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	$⊢ ℤRHom (R) = ℤRHom (R)$
42		eqid	$⊢ 0_{R} = 0_{R}$
43	41 42	zrh0	$⊢ R \in Ring \to ℤRHom (R) (0) = 0_{R}$
44	3 43	syl	$⊢ φ \to ℤRHom (R) (0) = 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} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (d) \neq 1 \leftrightarrow 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (d) = 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	$⊢ (D \in V \land 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D \land d \in D) \to (𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (d) = 1 \leftrightarrow d \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}])$
59	58	biimpa	$⊢ ((D \in V \land 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D \land d \in D) \land 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (d) = 1) \to d \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]$
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	$⊢ (Fun 𝟙_{I} \land d \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \to \exists b \in \{c \in 𝒫 I \| \|c\| = K\} 𝟙_{I} (b) = 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	$⊢ ℕ_{0} \in SubMnd (ℂ_{fld})$
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	$⊢ φ \to D \subseteq {ℕ_{0}}^{I}$
69	68	sselda	$⊢ (φ \land d \in D) \to d \in ({ℕ_{0}}^{I})$
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	$⊢ ℂ_{fld} ↾_{𝑠} ℕ_{0} = ℂ_{fld} ↾_{𝑠} ℕ_{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 supp 0 \subseteq dom d$
75	2	adantr	$⊢ (φ \land d \in D) \to I \in Fin$
76		nn0ex	$⊢ ℕ_{0} \in V$
77	76	a1i	$⊢ (φ \land d \in D) \to ℕ_{0} \in V$
78	75 77 69	elmaprd	$⊢ (φ \land d \in D) \to d : I ⟶ ℕ_{0}$
79	78	fdmd	$⊢ (φ \land d \in D) \to 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	$⊢ (I \in Fin \land b \subseteq I) \to 𝟙_{I} (b) 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 (\|c\| = K \leftrightarrow \|b\| = K)$
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 mPoly R = I mPoly R$
99		eqid	$⊢ {Base}_{(I mPoly R)} = {Base}_{(I mPoly R)}$
100	1	psrbasfsupp	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
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 \|-

Metamath Proof Explorer

Theorem esplymhp

Proof