Metamath Proof Explorer

Theorem esplyfval1

Description: The first elementary symmetric polynomial is the sum of all variables. (Contributed by Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses esplyfval1.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
esplyfval1.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
esplyfval1.e ⊢ 𝐸 = ( 𝐼 eSymPoly 𝑅 )
esplyfval1.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplyfval1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion esplyfval1 ( 𝜑 → ( 𝐸 ‘ 1 ) = ( 𝑊 Σg 𝑉 ) )

Proof

Step Hyp Ref Expression
1 esplyfval1.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
2 esplyfval1.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
3 esplyfval1.e ⊢ 𝐸 = ( 𝐼 eSymPoly 𝑅 )
4 esplyfval1.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
5 esplyfval1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
7 6 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ Fin )
11 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑅 ∈ Ring )
12 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑖 ∈ 𝐼 )
13 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
14 2 7 8 9 10 11 12 13 mvrval2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) = if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
15 14 ad4ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) = if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
16 15 an52ds ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) = if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
17 16 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
18 17 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
19 nfv ⊢ Ⅎ 𝑗 ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 )
20 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) )
21 20 nfeq2 ⊢ Ⅎ 𝑗 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) )
22 nfv ⊢ Ⅎ 𝑗 𝑖 = ∪ ( 𝑓 supp 0 )
23 21 22 nfbi ⊢ Ⅎ 𝑗 ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ↔ 𝑖 = ∪ ( 𝑓 supp 0 ) )
24 unisnv ⊢ ∪ { 𝑗 } = 𝑗
25 24 eqeq2i ⊢ ( 𝑖 = ∪ { 𝑗 } ↔ 𝑖 = 𝑗 )
26 25 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ( 𝑖 = ∪ { 𝑗 } ↔ 𝑖 = 𝑗 ) )
27 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ( 𝑓 supp 0 ) = { 𝑗 } )
28 27 unieqd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ∪ ( 𝑓 supp 0 ) = ∪ { 𝑗 } )
29 28 adantllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ∪ ( 𝑓 supp 0 ) = ∪ { 𝑗 } )
30 29 eqeq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ( 𝑖 = ∪ ( 𝑓 supp 0 ) ↔ 𝑖 = ∪ { 𝑗 } ) )
31 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑖 = 𝑗 ) → ( 𝑓 supp 0 ) = { 𝑗 } )
32 31 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑖 = 𝑗 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝑓 supp 0 ) ) = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑗 } ) )
33 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝐼 ∈ Fin )
34 ssrab2 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 )
35 34 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 ) )
36 35 sselda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) )
37 36 elmaprd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑓 : 𝐼 ⟶ ℕ0 )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑓 : 𝐼 ⟶ ℕ0 )
39 ffrn ⊢ ( 𝑓 : 𝐼 ⟶ ℕ0 → 𝑓 : 𝐼 ⟶ ran 𝑓 )
40 38 39 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑓 : 𝐼 ⟶ ran 𝑓 )
41 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ran 𝑓 ⊆ { 0 , 1 } )
42 40 41 fssd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑓 : 𝐼 ⟶ { 0 , 1 } )
43 33 42 indfsid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝑓 supp 0 ) ) )
44 43 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑖 = 𝑗 ) → 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝑓 supp 0 ) ) )
45 sneq ⊢ ( 𝑖 = 𝑗 → { 𝑖 } = { 𝑗 } )
46 45 adantl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑖 = 𝑗 ) → { 𝑖 } = { 𝑗 } )
47 46 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑖 = 𝑗 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑗 } ) )
48 32 44 47 3eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑖 = 𝑗 ) → 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) )
49 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) → 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) )
50 49 oveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) → ( 𝑓 supp 0 ) = ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) supp 0 ) )
51 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) → ( 𝑓 supp 0 ) = { 𝑗 } )
52 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → 𝐼 ∈ Fin )
53 52 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) → 𝐼 ∈ Fin )
54 snssi ⊢ ( 𝑖 ∈ 𝐼 → { 𝑖 } ⊆ 𝐼 )
55 54 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) → { 𝑖 } ⊆ 𝐼 )
56 55 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) → { 𝑖 } ⊆ 𝐼 )
57 indsupp ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑖 } ⊆ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) supp 0 ) = { 𝑖 } )
58 53 56 57 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) supp 0 ) = { 𝑖 } )
59 50 51 58 3eqtr3rd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) → { 𝑖 } = { 𝑗 } )
60 vex ⊢ 𝑖 ∈ V
61 60 sneqr ⊢ ( { 𝑖 } = { 𝑗 } → 𝑖 = 𝑗 )
62 59 61 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) ∧ 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) → 𝑖 = 𝑗 )
63 48 62 impbida ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ( 𝑖 = 𝑗 ↔ 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) )
64 indsn ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
65 52 64 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
66 65 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
67 66 eqeq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ( 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ↔ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) )
68 63 67 bitr2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ↔ 𝑖 = 𝑗 ) )
69 26 30 68 3bitr4rd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ↔ 𝑖 = ∪ ( 𝑓 supp 0 ) ) )
70 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 𝑓 supp 0 ) ∈ V )
71 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 )
72 hash1snb ⊢ ( ( 𝑓 supp 0 ) ∈ V → ( ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ↔ ∃ 𝑗 ( 𝑓 supp 0 ) = { 𝑗 } ) )
73 72 biimpa ⊢ ( ( ( 𝑓 supp 0 ) ∈ V ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ∃ 𝑗 ( 𝑓 supp 0 ) = { 𝑗 } )
74 70 71 73 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ∃ 𝑗 ( 𝑓 supp 0 ) = { 𝑗 } )
75 exsnrex ⊢ ( ∃ 𝑗 ( 𝑓 supp 0 ) = { 𝑗 } ↔ ∃ 𝑗 ∈ ( 𝑓 supp 0 ) ( 𝑓 supp 0 ) = { 𝑗 } )
76 74 75 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ∃ 𝑗 ∈ ( 𝑓 supp 0 ) ( 𝑓 supp 0 ) = { 𝑗 } )
77 76 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) → ∃ 𝑗 ∈ ( 𝑓 supp 0 ) ( 𝑓 supp 0 ) = { 𝑗 } )
78 19 23 69 77 r19.29af2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ↔ 𝑖 = ∪ ( 𝑓 supp 0 ) ) )
79 78 ifbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑖 = ∪ ( 𝑓 supp 0 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
80 79 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = ∪ ( 𝑓 supp 0 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
81 80 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = ∪ ( 𝑓 supp 0 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
82 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
83 5 82 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
84 83 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → 𝑅 ∈ Mnd )
85 suppssdm ⊢ ( 𝑓 supp 0 ) ⊆ dom 𝑓
86 37 fdmd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → dom 𝑓 = 𝐼 )
87 86 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → dom 𝑓 = 𝐼 )
88 85 87 sseqtrid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ( 𝑓 supp 0 ) ⊆ 𝐼 )
89 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → 𝑗 ∈ ( 𝑓 supp 0 ) )
90 88 89 sseldd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → 𝑗 ∈ 𝐼 )
91 24 90 eqeltrid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ∪ { 𝑗 } ∈ 𝐼 )
92 28 91 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑗 ∈ ( 𝑓 supp 0 ) ) ∧ ( 𝑓 supp 0 ) = { 𝑗 } ) → ∪ ( 𝑓 supp 0 ) ∈ 𝐼 )
93 92 76 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ∪ ( 𝑓 supp 0 ) ∈ 𝐼 )
94 eqid ⊢ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = ∪ ( 𝑓 supp 0 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = ∪ ( 𝑓 supp 0 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
95 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
96 95 9 5 ringidcld ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
97 96 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
98 8 84 52 93 94 97 gsummptif1n0 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = ∪ ( 𝑓 supp 0 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 1r ‘ 𝑅 ) )
99 18 81 98 3eqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 1r ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) )
100 99 anasss ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ) → ( 1r ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) )
101 83 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑅 ∈ Mnd )
102 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → 𝐼 ∈ Fin )
103 8 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ Fin ) → ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
104 101 102 103 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
105 14 an32s ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) = if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
106 105 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) = if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
107 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
108 107 rneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ran 𝑓 = ran ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
109 nfv ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 )
110 109 21 nfan ⊢ Ⅎ 𝑗 ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
111 eqid ⊢ ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) )
112 1nn0 ⊢ 1 ∈ ℕ0
113 prid2g ⊢ ( 1 ∈ ℕ0 → 1 ∈ { 0 , 1 } )
114 112 113 mp1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) ∧ 𝑗 ∈ 𝐼 ) → 1 ∈ { 0 , 1 } )
115 0nn0 ⊢ 0 ∈ ℕ0
116 prid1g ⊢ ( 0 ∈ ℕ0 → 0 ∈ { 0 , 1 } )
117 115 116 mp1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) ∧ 𝑗 ∈ 𝐼 ) → 0 ∈ { 0 , 1 } )
118 114 117 ifcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) ∧ 𝑗 ∈ 𝐼 ) → if ( 𝑗 = 𝑖 , 1 , 0 ) ∈ { 0 , 1 } )
119 110 111 118 rnmptssd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ran ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ⊆ { 0 , 1 } )
120 108 119 eqsstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ran 𝑓 ⊆ { 0 , 1 } )
121 120 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ran 𝑓 ⊆ { 0 , 1 } )
122 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ¬ ran 𝑓 ⊆ { 0 , 1 } )
123 121 122 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) ∧ 𝑖 ∈ 𝐼 ) → ¬ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
124 123 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
125 106 124 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) ∧ 𝑖 ∈ 𝐼 ) → ( 0g ‘ 𝑅 ) = ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) )
126 125 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( 𝑖 ∈ 𝐼 ↦ ( 0g ‘ 𝑅 ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) )
127 126 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( 0g ‘ 𝑅 ) ) ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) )
128 104 127 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( 0g ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) )
129 128 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( 0g ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) )
130 83 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → 𝑅 ∈ Mnd )
131 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → 𝐼 ∈ Fin )
132 130 131 103 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
133 105 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) = if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
134 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
135 4 64 sylan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
136 135 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
137 134 136 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → 𝑓 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) )
138 137 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ( 𝑓 supp 0 ) = ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) supp 0 ) )
139 131 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → 𝐼 ∈ Fin )
140 54 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → { 𝑖 } ⊆ 𝐼 )
141 139 140 57 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) supp 0 ) = { 𝑖 } )
142 138 141 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ( 𝑓 supp 0 ) = { 𝑖 } )
143 142 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) = ( ♯ ‘ { 𝑖 } ) )
144 hashsng ⊢ ( 𝑖 ∈ 𝐼 → ( ♯ ‘ { 𝑖 } ) = 1 )
145 144 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ( ♯ ‘ { 𝑖 } ) = 1 )
146 143 145 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 )
147 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) → ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 )
148 146 147 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) → ¬ 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
149 148 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑓 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
150 133 149 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ∧ 𝑖 ∈ 𝐼 ) → ( 0g ‘ 𝑅 ) = ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) )
151 150 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 𝑖 ∈ 𝐼 ↦ ( 0g ‘ 𝑅 ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) )
152 151 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( 0g ‘ 𝑅 ) ) ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) )
153 132 152 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 0g ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) )
154 153 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ) ∧ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( 0g ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) )
155 pm3.13 ⊢ ( ¬ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) → ( ¬ ran 𝑓 ⊆ { 0 , 1 } ∨ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) )
156 155 adantl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ) → ( ¬ ran 𝑓 ⊆ { 0 , 1 } ∨ ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) )
157 129 154 156 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ¬ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) ) → ( 0g ‘ 𝑅 ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) )
158 100 157 ifeqda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) )
159 158 mpteq2dva ⊢ ( 𝜑 → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) ) )
160 3 fveq1i ⊢ ( 𝐸 ‘ 1 ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ 1 )
161 112 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
162 6 4 5 161 8 9 esplyfval3 ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 1 ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
163 160 162 eqtrid ⊢ ( 𝜑 → ( 𝐸 ‘ 1 ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 1 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
164 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
165 1 2 164 4 5 mvrf2 ⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ ( Base ‘ 𝑊 ) )
166 1 164 5 4 6 4 165 mplgsum ⊢ ( 𝜑 → ( 𝑊 Σg 𝑉 ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑅 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑉 ‘ 𝑖 ) ‘ 𝑓 ) ) ) ) )
167 159 163 166 3eqtr4d ⊢ ( 𝜑 → ( 𝐸 ‘ 1 ) = ( 𝑊 Σg 𝑉 ) )