This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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