Metamath Proof Explorer

Theorem esplyfvaln

Description: The last elementary symmetric polynomial is the product 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 )
esplyfvaln.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
esplyfvaln.n ⊢ 𝑁 = ( ♯ ‘ 𝐼 )
esplyfvaln.m ⊢ 𝑀 = ( mulGrp ‘ 𝑊 )
Assertion esplyfvaln ( 𝜑 → ( 𝐸 ‘ 𝑁 ) = ( 𝑀 Σg 𝑉 ) )

Proof

Step Hyp Ref Expression
1 esplyfval1.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
2 esplyfval1.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
3 esplyfval1.e ⊢ 𝐸 = ( 𝐼 eSymPoly 𝑅 )
4 esplyfval1.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
5 esplyfvaln.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 esplyfvaln.n ⊢ 𝑁 = ( ♯ ‘ 𝐼 )
7 esplyfvaln.m ⊢ 𝑀 = ( mulGrp ‘ 𝑊 )
8 3 fveq1i ⊢ ( 𝐸 ‘ 𝑁 ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝑁 )
9 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
10 5 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
11 hashcl ⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
12 4 11 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
13 6 12 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
14 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
15 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
16 9 4 10 13 14 15 esplyfval3 ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝑁 ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
17 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
18 breq1 ⊢ ( ℎ = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) → ( ℎ finSupp 0 ↔ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) finSupp 0 ) )
19 nn0ex ⊢ ℕ0 ∈ V
20 19 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ℕ0 ∈ V )
21 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐼 ∈ Fin )
22 snssi ⊢ ( 𝑖 ∈ 𝐼 → { 𝑖 } ⊆ 𝐼 )
23 indf ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑖 } ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) : 𝐼 ⟶ { 0 , 1 } )
24 4 22 23 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) : 𝐼 ⟶ { 0 , 1 } )
25 0nn0 ⊢ 0 ∈ ℕ0
26 25 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 0 ∈ ℕ0 )
27 1nn0 ⊢ 1 ∈ ℕ0
28 27 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 1 ∈ ℕ0 )
29 26 28 prssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → { 0 , 1 } ⊆ ℕ0 )
30 24 29 fssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) : 𝐼 ⟶ ℕ0 )
31 20 21 30 elmapdd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ∈ ( ℕ0 ↑m 𝐼 ) )
32 24 21 26 fidmfisupp ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) finSupp 0 )
33 18 31 32 elrabd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
34 33 fmpttd ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) : 𝐼 ⟶ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
35 eqeq2 ⊢ ( 𝑡 = 𝑦 → ( 𝑢 = 𝑡 ↔ 𝑢 = 𝑦 ) )
36 35 ifbid ⊢ ( 𝑡 = 𝑦 → if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑢 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
37 36 mpteq2dv ⊢ ( 𝑡 = 𝑦 → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
38 eqeq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 = 𝑦 ↔ 𝑧 = 𝑦 ) )
39 38 ifbid ⊢ ( 𝑢 = 𝑧 → if ( 𝑢 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑧 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
40 39 cbvmptv ⊢ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑧 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
41 37 40 eqtrdi ⊢ ( 𝑡 = 𝑦 → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑧 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
42 41 cbvmptv ⊢ ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑧 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
43 1 17 5 4 9 4 34 15 14 7 42 mplmonprod ⊢ ( 𝜑 → ( 𝑀 Σg ( ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ∘ ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ) ) = ( ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ‘ ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) )
44 eqid ⊢ ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
45 eqeq2 ⊢ ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) → ( 𝑢 = 𝑡 ↔ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) )
46 45 ifbid ⊢ ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) → if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
47 46 mpteq2dv ⊢ ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
48 simpr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) )
49 48 rneqd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ran 𝑢 = ran ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) )
50 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
51 eqid ⊢ ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) )
52 eqid ⊢ ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) )
53 sneq ⊢ ( 𝑖 = 𝑘 → { 𝑖 } = { 𝑘 } )
54 53 fveq2d ⊢ ( 𝑖 = 𝑘 → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) )
55 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
56 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ∈ V )
57 52 54 55 56 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) )
58 57 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) = ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) )
59 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐼 ∈ Fin )
60 55 snssd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → { 𝑘 } ⊆ 𝐼 )
61 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑗 ∈ 𝐼 )
62 indfval ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑘 } ⊆ 𝐼 ∧ 𝑗 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) = if ( 𝑗 ∈ { 𝑘 } , 1 , 0 ) )
63 59 60 61 62 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) = if ( 𝑗 ∈ { 𝑘 } , 1 , 0 ) )
64 velsn ⊢ ( 𝑗 ∈ { 𝑘 } ↔ 𝑗 = 𝑘 )
65 equcom ⊢ ( 𝑗 = 𝑘 ↔ 𝑘 = 𝑗 )
66 64 65 bitri ⊢ ( 𝑗 ∈ { 𝑘 } ↔ 𝑘 = 𝑗 )
67 66 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑗 ∈ { 𝑘 } ↔ 𝑘 = 𝑗 ) )
68 67 ifbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → if ( 𝑗 ∈ { 𝑘 } , 1 , 0 ) = if ( 𝑘 = 𝑗 , 1 , 0 ) )
69 58 63 68 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) = if ( 𝑘 = 𝑗 , 1 , 0 ) )
70 69 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) )
71 70 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) )
72 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
73 cnfldfld ⊢ ℂfld ∈ Field
74 id ⊢ ( ℂfld ∈ Field → ℂfld ∈ Field )
75 74 fldcrngd ⊢ ( ℂfld ∈ Field → ℂfld ∈ CRing )
76 crngring ⊢ ( ℂfld ∈ CRing → ℂfld ∈ Ring )
77 ringcmn ⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
78 75 76 77 3syl ⊢ ( ℂfld ∈ Field → ℂfld ∈ CMnd )
79 73 78 mp1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ℂfld ∈ CMnd )
80 79 cmnmndd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ℂfld ∈ Mnd )
81 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → 𝐼 ∈ Fin )
82 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → 𝑗 ∈ 𝐼 )
83 eqid ⊢ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) )
84 ax-1cn ⊢ 1 ∈ ℂ
85 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
86 84 85 eleqtri ⊢ 1 ∈ ( Base ‘ ℂfld )
87 86 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → 1 ∈ ( Base ‘ ℂfld ) )
88 72 80 81 82 83 87 gsummptif1n0 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) = 1 )
89 71 88 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) = 1 )
90 1ex ⊢ 1 ∈ V
91 90 prid2 ⊢ 1 ∈ { 0 , 1 }
92 89 91 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ∈ { 0 , 1 } )
93 92 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ∈ { 0 , 1 } )
94 50 51 93 rnmptssd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ran ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ⊆ { 0 , 1 } )
95 94 adantr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ran ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ⊆ { 0 , 1 } )
96 49 95 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ran 𝑢 ⊆ { 0 , 1 } )
97 48 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( 𝑢 supp 0 ) = ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) )
98 suppssdm ⊢ ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) ⊆ dom ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) )
99 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
100 99 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ℕ0 ∈ ( SubMnd ‘ ℂfld ) )
101 25 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 0 ∈ ℕ0 )
102 27 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 1 ∈ ℕ0 )
103 101 102 prssd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → { 0 , 1 } ⊆ ℕ0 )
104 indf ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑘 } ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) : 𝐼 ⟶ { 0 , 1 } )
105 59 60 104 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) : 𝐼 ⟶ { 0 , 1 } )
106 105 61 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ∈ { 0 , 1 } )
107 103 106 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ∈ ℕ0 )
108 58 107 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ∈ ℕ0 )
109 108 fmpttd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) : 𝐼 ⟶ ℕ0 )
110 25 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → 0 ∈ ℕ0 )
111 109 81 110 fdmfifsupp ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) finSupp 0 )
112 72 79 81 100 109 111 gsumsubmcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ∈ ℕ0 )
113 51 112 dmmptd ⊢ ( 𝜑 → dom ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) = 𝐼 )
114 98 113 sseqtrid ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) ⊆ 𝐼 )
115 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑖 ∈ 𝐼 )
116 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ∈ V )
117 eqid ⊢ ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) )
118 115 116 117 fnmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) Fn 𝐼 )
119 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
120 fveq2 ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) = ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) )
121 120 mpteq2dv ⊢ ( 𝑗 = 𝑖 → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) )
122 121 oveq2d ⊢ ( 𝑗 = 𝑖 → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) ) )
123 ovexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) ) ∈ V )
124 117 122 119 123 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) = ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) ) )
125 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐼 ∈ Fin )
126 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
127 126 snssd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → { 𝑘 } ⊆ 𝐼 )
128 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
129 indfval ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑘 } ⊆ 𝐼 ∧ 𝑖 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) = if ( 𝑖 ∈ { 𝑘 } , 1 , 0 ) )
130 125 127 128 129 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) = if ( 𝑖 ∈ { 𝑘 } , 1 , 0 ) )
131 velsn ⊢ ( 𝑖 ∈ { 𝑘 } ↔ 𝑖 = 𝑘 )
132 equcom ⊢ ( 𝑖 = 𝑘 ↔ 𝑘 = 𝑖 )
133 131 132 bitri ⊢ ( 𝑖 ∈ { 𝑘 } ↔ 𝑘 = 𝑖 )
134 133 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑖 ∈ { 𝑘 } ↔ 𝑘 = 𝑖 ) )
135 134 ifbid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → if ( 𝑖 ∈ { 𝑘 } , 1 , 0 ) = if ( 𝑘 = 𝑖 , 1 , 0 ) )
136 130 135 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) = if ( 𝑘 = 𝑖 , 1 , 0 ) )
137 136 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑖 , 1 , 0 ) ) )
138 137 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑖 , 1 , 0 ) ) ) )
139 73 78 mp1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ℂfld ∈ CMnd )
140 139 cmnmndd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ℂfld ∈ Mnd )
141 eqid ⊢ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑖 , 1 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑖 , 1 , 0 ) )
142 86 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 1 ∈ ( Base ‘ ℂfld ) )
143 72 140 21 119 141 142 gsummptif1n0 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑖 , 1 , 0 ) ) ) = 1 )
144 124 138 143 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) = 1 )
145 ax-1ne0 ⊢ 1 ≠ 0
146 145 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 1 ≠ 0 )
147 144 146 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) ≠ 0 )
148 118 21 26 119 147 elsuppfnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) supp 0 ) )
149 148 ex ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 → 𝑖 ∈ ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) supp 0 ) ) )
150 149 ssrdv ⊢ ( 𝜑 → 𝐼 ⊆ ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) supp 0 ) )
151 58 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) )
152 151 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) )
153 152 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) )
154 153 oveq1d ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) = ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) supp 0 ) )
155 150 154 sseqtrrd ⊢ ( 𝜑 → 𝐼 ⊆ ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) )
156 114 155 eqssd ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) = 𝐼 )
157 156 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) = 𝐼 )
158 97 157 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( 𝑢 supp 0 ) = 𝐼 )
159 158 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( ♯ ‘ ( 𝑢 supp 0 ) ) = ( ♯ ‘ 𝐼 ) )
160 159 6 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 )
161 96 160 jca ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) )
162 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ran 𝑢 ⊆ { 0 , 1 } )
163 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → 𝐼 ∈ Fin )
164 19 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → ℕ0 ∈ V )
165 ssrab2 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 )
166 165 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 ) )
167 166 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑢 ∈ ( ℕ0 ↑m 𝐼 ) )
168 167 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → 𝑢 ∈ ( ℕ0 ↑m 𝐼 ) )
169 163 164 168 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → 𝑢 : 𝐼 ⟶ ℕ0 )
170 169 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑢 : 𝐼 ⟶ ℕ0 )
171 170 ffnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑢 Fn 𝐼 )
172 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑗 ∈ 𝐼 )
173 171 172 fnfvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑢 ‘ 𝑗 ) ∈ ran 𝑢 )
174 162 173 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑢 ‘ 𝑗 ) ∈ { 0 , 1 } )
175 163 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐼 ∈ Fin )
176 25 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 0 ∈ ℕ0 )
177 suppssdm ⊢ ( 𝑢 supp 0 ) ⊆ dom 𝑢
178 177 170 fssdm ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑢 supp 0 ) ⊆ 𝐼 )
179 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 )
180 179 6 eqtr2di ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( ♯ ‘ 𝐼 ) = ( ♯ ‘ ( 𝑢 supp 0 ) ) )
181 175 178 180 phphashd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐼 = ( 𝑢 supp 0 ) )
182 172 181 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑗 ∈ ( 𝑢 supp 0 ) )
183 elsuppfn ⊢ ( ( 𝑢 Fn 𝐼 ∧ 𝐼 ∈ Fin ∧ 0 ∈ ℕ0 ) → ( 𝑗 ∈ ( 𝑢 supp 0 ) ↔ ( 𝑗 ∈ 𝐼 ∧ ( 𝑢 ‘ 𝑗 ) ≠ 0 ) ) )
184 183 simplbda ⊢ ( ( ( 𝑢 Fn 𝐼 ∧ 𝐼 ∈ Fin ∧ 0 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 𝑢 supp 0 ) ) → ( 𝑢 ‘ 𝑗 ) ≠ 0 )
185 171 175 176 182 184 syl31anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑢 ‘ 𝑗 ) ≠ 0 )
186 elprn1 ⊢ ( ( ( 𝑢 ‘ 𝑗 ) ∈ { 0 , 1 } ∧ ( 𝑢 ‘ 𝑗 ) ≠ 0 ) → ( 𝑢 ‘ 𝑗 ) = 1 )
187 174 185 186 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑢 ‘ 𝑗 ) = 1 )
188 187 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → ( 𝑗 ∈ 𝐼 ↦ ( 𝑢 ‘ 𝑗 ) ) = ( 𝑗 ∈ 𝐼 ↦ 1 ) )
189 169 feqmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( 𝑢 ‘ 𝑗 ) ) )
190 89 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ 1 ) )
191 190 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ 1 ) )
192 188 189 191 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) )
193 192 anasss ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ) → 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) )
194 161 193 impbida ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ↔ ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ) )
195 194 ifbid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
196 195 mpteq2dva ⊢ ( 𝜑 → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
197 rneq ⊢ ( 𝑢 = 𝑓 → ran 𝑢 = ran 𝑓 )
198 197 sseq1d ⊢ ( 𝑢 = 𝑓 → ( ran 𝑢 ⊆ { 0 , 1 } ↔ ran 𝑓 ⊆ { 0 , 1 } ) )
199 oveq1 ⊢ ( 𝑢 = 𝑓 → ( 𝑢 supp 0 ) = ( 𝑓 supp 0 ) )
200 199 fveqeq2d ⊢ ( 𝑢 = 𝑓 → ( ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ↔ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) )
201 198 200 anbi12d ⊢ ( 𝑢 = 𝑓 → ( ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ↔ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) ) )
202 201 ifbid ⊢ ( 𝑢 = 𝑓 → if ( ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
203 202 cbvmptv ⊢ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
204 196 203 eqtrdi ⊢ ( 𝜑 → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
205 47 204 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑡 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
206 breq1 ⊢ ( ℎ = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) → ( ℎ finSupp 0 ↔ ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) finSupp 0 ) )
207 19 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
208 112 fmpttd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) : 𝐼 ⟶ ℕ0 )
209 207 4 208 elmapdd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ∈ ( ℕ0 ↑m 𝐼 ) )
210 25 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
211 208 4 210 fidmfisupp ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) finSupp 0 )
212 206 209 211 elrabd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
213 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
214 213 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V
215 214 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V )
216 215 mptexd ⊢ ( 𝜑 → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ V )
217 44 205 212 216 fvmptd2 ⊢ ( 𝜑 → ( ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ‘ ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
218 43 217 eqtrd ⊢ ( 𝜑 → ( 𝑀 Σg ( ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ∘ ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
219 indval ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑖 } ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 ∈ { 𝑖 } , 1 , 0 ) ) )
220 4 22 219 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 ∈ { 𝑖 } , 1 , 0 ) ) )
221 velsn ⊢ ( 𝑗 ∈ { 𝑖 } ↔ 𝑗 = 𝑖 )
222 221 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑗 ∈ { 𝑖 } ↔ 𝑗 = 𝑖 ) )
223 222 ifbid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐼 ) → if ( 𝑗 ∈ { 𝑖 } , 1 , 0 ) = if ( 𝑗 = 𝑖 , 1 , 0 ) )
224 223 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 ∈ { 𝑖 } , 1 , 0 ) ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
225 220 224 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
226 225 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ↔ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) )
227 226 ifbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
228 227 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
229 eqeq1 ⊢ ( 𝑡 = 𝑢 → ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ↔ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) )
230 229 ifbid ⊢ ( 𝑡 = 𝑢 → if ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
231 230 cbvmptv ⊢ ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
232 228 231 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
233 232 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
234 eqidd ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) )
235 eqidd ⊢ ( 𝜑 → ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
236 eqeq2 ⊢ ( 𝑡 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) → ( 𝑢 = 𝑡 ↔ 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) )
237 236 ifbid ⊢ ( 𝑡 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) → if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
238 237 mpteq2dv ⊢ ( 𝑡 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
239 33 234 235 238 fmptco ⊢ ( 𝜑 → ( ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ∘ ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
240 9 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
241 2 240 14 15 4 5 mvrfval ⊢ ( 𝜑 → 𝑉 = ( 𝑖 ∈ 𝐼 ↦ ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
242 233 239 241 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ∘ ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ) = 𝑉 )
243 242 oveq2d ⊢ ( 𝜑 → ( 𝑀 Σg ( ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ∘ ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ) ) = ( 𝑀 Σg 𝑉 ) )
244 16 218 243 3eqtr2d ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝑁 ) = ( 𝑀 Σg 𝑉 ) )
245 8 244 eqtrid ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑁 ) = ( 𝑀 Σg 𝑉 ) )