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 1elpr01 ⊢ 1 ∈ { 0 , 1 }
91 89 90 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ∈ { 0 , 1 } )
92 91 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ∈ { 0 , 1 } )
93 50 51 92 rnmptssd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ran ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ⊆ { 0 , 1 } )
94 93 adantr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ran ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ⊆ { 0 , 1 } )
95 49 94 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ran 𝑢 ⊆ { 0 , 1 } )
96 48 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( 𝑢 supp 0 ) = ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) )
97 suppssdm ⊢ ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) ⊆ dom ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) )
98 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
99 98 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ℕ0 ∈ ( SubMnd ‘ ℂfld ) )
100 25 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 0 ∈ ℕ0 )
101 27 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 1 ∈ ℕ0 )
102 100 101 prssd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → { 0 , 1 } ⊆ ℕ0 )
103 indf ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑘 } ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) : 𝐼 ⟶ { 0 , 1 } )
104 59 60 103 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) : 𝐼 ⟶ { 0 , 1 } )
105 104 61 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ∈ { 0 , 1 } )
106 102 105 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ∈ ℕ0 )
107 58 106 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ∈ ℕ0 )
108 107 fmpttd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) : 𝐼 ⟶ ℕ0 )
109 25 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → 0 ∈ ℕ0 )
110 108 81 109 fdmfifsupp ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) finSupp 0 )
111 72 79 81 99 108 110 gsumsubmcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ∈ ℕ0 )
112 51 111 dmmptd ⊢ ( 𝜑 → dom ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) = 𝐼 )
113 97 112 sseqtrid ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) ⊆ 𝐼 )
114 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑖 ∈ 𝐼 )
115 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ∈ V )
116 eqid ⊢ ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) )
117 114 115 116 fnmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) Fn 𝐼 )
118 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
119 fveq2 ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) = ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) )
120 119 mpteq2dv ⊢ ( 𝑗 = 𝑖 → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) )
121 120 oveq2d ⊢ ( 𝑗 = 𝑖 → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) ) )
122 ovexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) ) ∈ V )
123 116 121 118 122 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) = ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) ) )
124 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐼 ∈ Fin )
125 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
126 125 snssd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → { 𝑘 } ⊆ 𝐼 )
127 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
128 indfval ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑘 } ⊆ 𝐼 ∧ 𝑖 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) = if ( 𝑖 ∈ { 𝑘 } , 1 , 0 ) )
129 124 126 127 128 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) = if ( 𝑖 ∈ { 𝑘 } , 1 , 0 ) )
130 velsn ⊢ ( 𝑖 ∈ { 𝑘 } ↔ 𝑖 = 𝑘 )
131 equcom ⊢ ( 𝑖 = 𝑘 ↔ 𝑘 = 𝑖 )
132 130 131 bitri ⊢ ( 𝑖 ∈ { 𝑘 } ↔ 𝑘 = 𝑖 )
133 132 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑖 ∈ { 𝑘 } ↔ 𝑘 = 𝑖 ) )
134 133 ifbid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → if ( 𝑖 ∈ { 𝑘 } , 1 , 0 ) = if ( 𝑘 = 𝑖 , 1 , 0 ) )
135 129 134 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) = if ( 𝑘 = 𝑖 , 1 , 0 ) )
136 135 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑖 , 1 , 0 ) ) )
137 136 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑖 ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑖 , 1 , 0 ) ) ) )
138 73 78 mp1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ℂfld ∈ CMnd )
139 138 cmnmndd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ℂfld ∈ Mnd )
140 eqid ⊢ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑖 , 1 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑖 , 1 , 0 ) )
141 86 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 1 ∈ ( Base ‘ ℂfld ) )
142 72 139 21 118 140 141 gsummptif1n0 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑖 , 1 , 0 ) ) ) = 1 )
143 123 137 142 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) = 1 )
144 ax-1ne0 ⊢ 1 ≠ 0
145 144 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 1 ≠ 0 )
146 143 145 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) ‘ 𝑖 ) ≠ 0 )
147 117 21 26 118 146 elsuppfnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) supp 0 ) )
148 147 ex ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 → 𝑖 ∈ ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) supp 0 ) ) )
149 148 ssrdv ⊢ ( 𝜑 → 𝐼 ⊆ ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) supp 0 ) )
150 58 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) )
151 150 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) = ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) )
152 151 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) )
153 152 oveq1d ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) = ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑘 } ) ‘ 𝑗 ) ) ) ) supp 0 ) )
154 149 153 sseqtrrd ⊢ ( 𝜑 → 𝐼 ⊆ ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) )
155 113 154 eqssd ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) = 𝐼 )
156 155 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) supp 0 ) = 𝐼 )
157 96 156 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( 𝑢 supp 0 ) = 𝐼 )
158 157 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( ♯ ‘ ( 𝑢 supp 0 ) ) = ( ♯ ‘ 𝐼 ) )
159 158 6 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 )
160 95 159 jca ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) )
161 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ran 𝑢 ⊆ { 0 , 1 } )
162 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → 𝐼 ∈ Fin )
163 19 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → ℕ0 ∈ V )
164 ssrab2 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 )
165 164 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 ) )
166 165 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑢 ∈ ( ℕ0 ↑m 𝐼 ) )
167 166 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → 𝑢 ∈ ( ℕ0 ↑m 𝐼 ) )
168 162 163 167 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → 𝑢 : 𝐼 ⟶ ℕ0 )
169 168 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑢 : 𝐼 ⟶ ℕ0 )
170 169 ffnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑢 Fn 𝐼 )
171 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑗 ∈ 𝐼 )
172 170 171 fnfvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑢 ‘ 𝑗 ) ∈ ran 𝑢 )
173 161 172 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑢 ‘ 𝑗 ) ∈ { 0 , 1 } )
174 162 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐼 ∈ Fin )
175 25 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 0 ∈ ℕ0 )
176 suppssdm ⊢ ( 𝑢 supp 0 ) ⊆ dom 𝑢
177 176 169 fssdm ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑢 supp 0 ) ⊆ 𝐼 )
178 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 )
179 178 6 eqtr2di ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( ♯ ‘ 𝐼 ) = ( ♯ ‘ ( 𝑢 supp 0 ) ) )
180 174 177 179 phphashd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐼 = ( 𝑢 supp 0 ) )
181 171 180 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑗 ∈ ( 𝑢 supp 0 ) )
182 elsuppfn ⊢ ( ( 𝑢 Fn 𝐼 ∧ 𝐼 ∈ Fin ∧ 0 ∈ ℕ0 ) → ( 𝑗 ∈ ( 𝑢 supp 0 ) ↔ ( 𝑗 ∈ 𝐼 ∧ ( 𝑢 ‘ 𝑗 ) ≠ 0 ) ) )
183 182 simplbda ⊢ ( ( ( 𝑢 Fn 𝐼 ∧ 𝐼 ∈ Fin ∧ 0 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 𝑢 supp 0 ) ) → ( 𝑢 ‘ 𝑗 ) ≠ 0 )
184 170 174 175 181 183 syl31anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑢 ‘ 𝑗 ) ≠ 0 )
185 elprn1 ⊢ ( ( ( 𝑢 ‘ 𝑗 ) ∈ { 0 , 1 } ∧ ( 𝑢 ‘ 𝑗 ) ≠ 0 ) → ( 𝑢 ‘ 𝑗 ) = 1 )
186 173 184 185 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑢 ‘ 𝑗 ) = 1 )
187 186 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → ( 𝑗 ∈ 𝐼 ↦ ( 𝑢 ‘ 𝑗 ) ) = ( 𝑗 ∈ 𝐼 ↦ 1 ) )
188 168 feqmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( 𝑢 ‘ 𝑗 ) ) )
189 89 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ 1 ) )
190 189 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ 𝐼 ↦ 1 ) )
191 187 188 190 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ran 𝑢 ⊆ { 0 , 1 } ) ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) → 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) )
192 191 anasss ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ) → 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) )
193 160 192 impbida ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ↔ ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ) )
194 193 ifbid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
195 194 mpteq2dva ⊢ ( 𝜑 → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
196 rneq ⊢ ( 𝑢 = 𝑓 → ran 𝑢 = ran 𝑓 )
197 196 sseq1d ⊢ ( 𝑢 = 𝑓 → ( ran 𝑢 ⊆ { 0 , 1 } ↔ ran 𝑓 ⊆ { 0 , 1 } ) )
198 oveq1 ⊢ ( 𝑢 = 𝑓 → ( 𝑢 supp 0 ) = ( 𝑓 supp 0 ) )
199 198 fveqeq2d ⊢ ( 𝑢 = 𝑓 → ( ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ↔ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) )
200 197 199 anbi12d ⊢ ( 𝑢 = 𝑓 → ( ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) ↔ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) ) )
201 200 ifbid ⊢ ( 𝑢 = 𝑓 → if ( ( ran 𝑢 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑢 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
202 201 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 ‘ 𝑅 ) ) )
203 195 202 eqtrdi ⊢ ( 𝜑 → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
204 47 203 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑡 = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ) → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
205 breq1 ⊢ ( ℎ = ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) → ( ℎ finSupp 0 ↔ ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) finSupp 0 ) )
206 19 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
207 111 fmpttd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) : 𝐼 ⟶ ℕ0 )
208 206 4 207 elmapdd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ∈ ( ℕ0 ↑m 𝐼 ) )
209 25 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
210 207 4 209 fidmfisupp ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) finSupp 0 )
211 205 208 210 elrabd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑘 ∈ 𝐼 ↦ ( ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ‘ 𝑘 ) ‘ 𝑗 ) ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
212 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
213 212 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V
214 213 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V )
215 214 mptexd ⊢ ( 𝜑 → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝑁 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ V )
216 44 204 211 215 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 ‘ 𝑅 ) ) ) )
217 43 216 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 ‘ 𝑅 ) ) ) )
218 indval ⊢ ( ( 𝐼 ∈ Fin ∧ { 𝑖 } ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 ∈ { 𝑖 } , 1 , 0 ) ) )
219 4 22 218 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 ∈ { 𝑖 } , 1 , 0 ) ) )
220 velsn ⊢ ( 𝑗 ∈ { 𝑖 } ↔ 𝑗 = 𝑖 )
221 220 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝑗 ∈ { 𝑖 } ↔ 𝑗 = 𝑖 ) )
222 221 ifbid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐼 ) → if ( 𝑗 ∈ { 𝑖 } , 1 , 0 ) = if ( 𝑗 = 𝑖 , 1 , 0 ) )
223 222 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 ∈ { 𝑖 } , 1 , 0 ) ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
224 219 223 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) )
225 224 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ↔ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) )
226 225 ifbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
227 226 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
228 eqeq1 ⊢ ( 𝑡 = 𝑢 → ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ↔ 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) ) )
229 228 ifbid ⊢ ( 𝑡 = 𝑢 → if ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
230 229 cbvmptv ⊢ ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
231 227 230 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
232 231 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
233 eqidd ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) )
234 eqidd ⊢ ( 𝜑 → ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
235 eqeq2 ⊢ ( 𝑡 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) → ( 𝑢 = 𝑡 ↔ 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) )
236 235 ifbid ⊢ ( 𝑡 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) → if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
237 236 mpteq2dv ⊢ ( 𝑡 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) → ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
238 33 233 234 237 fmptco ⊢ ( 𝜑 → ( ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ∘ ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
239 9 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
240 2 239 14 15 4 5 mvrfval ⊢ ( 𝜑 → 𝑉 = ( 𝑖 ∈ 𝐼 ↦ ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑡 = ( 𝑗 ∈ 𝐼 ↦ if ( 𝑗 = 𝑖 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
241 232 238 240 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ∘ ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ) = 𝑉 )
242 241 oveq2d ⊢ ( 𝜑 → ( 𝑀 Σg ( ( 𝑡 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑢 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ if ( 𝑢 = 𝑡 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ∘ ( 𝑖 ∈ 𝐼 ↦ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑖 } ) ) ) ) = ( 𝑀 Σg 𝑉 ) )
243 16 217 242 3eqtr2d ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝑁 ) = ( 𝑀 Σg 𝑉 ) )
244 8 243 eqtrid ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑁 ) = ( 𝑀 Σg 𝑉 ) )