Metamath Proof Explorer

Theorem mplcoe1

Description: Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mplcoe1.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplcoe1.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
mplcoe1.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplcoe1.o ⊢ 1 = ( 1r ‘ 𝑅 )
mplcoe1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mplcoe1.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
mplcoe1.n ⊢ · = ( ·𝑠 ‘ 𝑃 )
mplcoe1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mplcoe1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion mplcoe1 ( 𝜑 → 𝑋 = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mplcoe1.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplcoe1.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3 mplcoe1.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 mplcoe1.o ⊢ 1 = ( 1r ‘ 𝑅 )
5 mplcoe1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 mplcoe1.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
7 mplcoe1.n ⊢ · = ( ·𝑠 ‘ 𝑃 )
8 mplcoe1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
9 mplcoe1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 1 10 6 2 9 mplelf ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
12 11 feqmptd ⊢ ( 𝜑 → 𝑋 = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑦 ) ) )
13 iftrue ⊢ ( 𝑦 ∈ ( 𝑋 supp 0 ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝑋 supp 0 ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
15 eldif ⊢ ( 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ↔ ( 𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ ( 𝑋 supp 0 ) ) )
16 ssidd ⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ ( 𝑋 supp 0 ) )
17 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
18 2 17 rabex2 ⊢ 𝐷 ∈ V
19 18 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
20 3 fvexi ⊢ 0 ∈ V
21 20 a1i ⊢ ( 𝜑 → 0 ∈ V )
22 11 16 19 21 suppssr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 𝑋 ‘ 𝑦 ) = 0 )
23 22 ifeq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , ( 𝑋 ‘ 𝑦 ) ) = if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
24 ifid ⊢ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , ( 𝑋 ‘ 𝑦 ) ) = ( 𝑋 ‘ 𝑦 )
25 23 24 eqtr3di ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
26 15 25 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ ( 𝑋 supp 0 ) ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
27 26 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ ( 𝑋 supp 0 ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
28 14 27 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
29 28 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑦 ) ) )
30 12 29 eqtr4d ⊢ ( 𝜑 → 𝑋 = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
31 suppssdm ⊢ ( 𝑋 supp 0 ) ⊆ dom 𝑋
32 31 11 fssdm ⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ 𝐷 )
33 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
34 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
35 1 33 34 3 6 mplelbas ⊢ ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑋 finSupp 0 ) )
36 35 simprbi ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 finSupp 0 )
37 9 36 syl ⊢ ( 𝜑 → 𝑋 finSupp 0 )
38 37 fsuppimpd ⊢ ( 𝜑 → ( 𝑋 supp 0 ) ∈ Fin )
39 sseq1 ⊢ ( 𝑤 = ∅ → ( 𝑤 ⊆ 𝐷 ↔ ∅ ⊆ 𝐷 ) )
40 mpteq1 ⊢ ( 𝑤 = ∅ → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ ∅ ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
41 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ∅
42 40 41 eqtrdi ⊢ ( 𝑤 = ∅ → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ∅ )
43 42 oveq2d ⊢ ( 𝑤 = ∅ → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ∅ ) )
44 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
45 44 gsum0 ⊢ ( 𝑃 Σg ∅ ) = ( 0g ‘ 𝑃 )
46 43 45 eqtrdi ⊢ ( 𝑤 = ∅ → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 0g ‘ 𝑃 ) )
47 noel ⊢ ¬ 𝑦 ∈ ∅
48 eleq2 ⊢ ( 𝑤 = ∅ → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ∅ ) )
49 47 48 mtbiri ⊢ ( 𝑤 = ∅ → ¬ 𝑦 ∈ 𝑤 )
50 49 iffalsed ⊢ ( 𝑤 = ∅ → if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) = 0 )
51 50 mpteq2dv ⊢ ( 𝑤 = ∅ → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) )
52 46 51 eqeq12d ⊢ ( 𝑤 = ∅ → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) ) )
53 39 52 imbi12d ⊢ ( 𝑤 = ∅ → ( ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ↔ ( ∅ ⊆ 𝐷 → ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) ) ) )
54 53 imbi2d ⊢ ( 𝑤 = ∅ → ( ( 𝜑 → ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐷 → ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) ) ) ) )
55 sseq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ⊆ 𝐷 ↔ 𝑥 ⊆ 𝐷 ) )
56 mpteq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
57 56 oveq2d ⊢ ( 𝑤 = 𝑥 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
58 eleq2 ⊢ ( 𝑤 = 𝑥 → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥 ) )
59 58 ifbid ⊢ ( 𝑤 = 𝑥 → if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
60 59 mpteq2dv ⊢ ( 𝑤 = 𝑥 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
61 57 60 eqeq12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
62 55 61 imbi12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ↔ ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
63 62 imbi2d ⊢ ( 𝑤 = 𝑥 → ( ( 𝜑 → ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ↔ ( 𝜑 → ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
64 sseq1 ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑤 ⊆ 𝐷 ↔ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) )
65 mpteq1 ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
66 65 oveq2d ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
67 eleq2 ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ) )
68 67 ifbid ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
69 68 mpteq2dv ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
70 66 69 eqeq12d ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
71 64 70 imbi12d ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ↔ ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
72 71 imbi2d ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝜑 → ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ↔ ( 𝜑 → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
73 sseq1 ⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( 𝑤 ⊆ 𝐷 ↔ ( 𝑋 supp 0 ) ⊆ 𝐷 ) )
74 mpteq1 ⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
75 74 oveq2d ⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
76 eleq2 ⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ( 𝑋 supp 0 ) ) )
77 76 ifbid ⊢ ( 𝑤 = ( 𝑋 supp 0 ) → if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) = if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
78 77 mpteq2dv ⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
79 75 78 eqeq12d ⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
80 73 79 imbi12d ⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ↔ ( ( 𝑋 supp 0 ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
81 80 imbi2d ⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( ( 𝜑 → ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ↔ ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
82 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
83 8 82 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
84 1 2 3 44 5 83 mpl0 ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 𝐷 × { 0 } ) )
85 fconstmpt ⊢ ( 𝐷 × { 0 } ) = ( 𝑦 ∈ 𝐷 ↦ 0 )
86 84 85 eqtrdi ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) )
87 86 a1d ⊢ ( 𝜑 → ( ∅ ⊆ 𝐷 → ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) ) )
88 ssun1 ⊢ 𝑥 ⊆ ( 𝑥 ∪ { 𝑧 } )
89 sstr2 ⊢ ( 𝑥 ⊆ ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → 𝑥 ⊆ 𝐷 ) )
90 88 89 ax-mp ⊢ ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → 𝑥 ⊆ 𝐷 )
91 90 imim1i ⊢ ( ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
92 oveq1 ⊢ ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
93 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
94 1 5 8 mplringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
95 ringcmn ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
96 94 95 syl ⊢ ( 𝜑 → 𝑃 ∈ CMnd )
97 96 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑃 ∈ CMnd )
98 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑥 ∈ Fin )
99 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 )
100 99 unssad ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑥 ⊆ 𝐷 )
101 100 sselda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝐷 )
102 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝐼 ∈ 𝑊 )
103 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ Ring )
104 1 102 103 mpllmodd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑃 ∈ LMod )
105 11 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
106 1 5 8 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
107 106 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
108 107 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
109 105 108 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
110 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑘 ∈ 𝐷 )
111 1 6 3 4 2 102 103 110 mplmon ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ∈ 𝐵 )
112 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
113 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
114 6 112 7 113 lmodvscl ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
115 104 109 111 114 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
116 115 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
117 101 116 syldan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑘 ∈ 𝑥 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
118 vex ⊢ 𝑧 ∈ V
119 118 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑧 ∈ V )
120 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ¬ 𝑧 ∈ 𝑥 )
121 1 5 8 mpllmodd ⊢ ( 𝜑 → 𝑃 ∈ LMod )
122 121 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑃 ∈ LMod )
123 11 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
124 99 unssbd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → { 𝑧 } ⊆ 𝐷 )
125 118 snss ⊢ ( 𝑧 ∈ 𝐷 ↔ { 𝑧 } ⊆ 𝐷 )
126 124 125 sylibr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑧 ∈ 𝐷 )
127 123 126 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
128 106 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
129 128 fveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
130 127 129 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
131 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝐼 ∈ 𝑊 )
132 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑅 ∈ Ring )
133 1 6 3 4 2 131 132 126 mplmon ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ∈ 𝐵 )
134 6 112 7 113 lmodvscl ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ∈ 𝐵 )
135 122 130 133 134 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ∈ 𝐵 )
136 fveq2 ⊢ ( 𝑘 = 𝑧 → ( 𝑋 ‘ 𝑘 ) = ( 𝑋 ‘ 𝑧 ) )
137 equequ2 ⊢ ( 𝑘 = 𝑧 → ( 𝑦 = 𝑘 ↔ 𝑦 = 𝑧 ) )
138 137 ifbid ⊢ ( 𝑘 = 𝑧 → if ( 𝑦 = 𝑘 , 1 , 0 ) = if ( 𝑦 = 𝑧 , 1 , 0 ) )
139 138 mpteq2dv ⊢ ( 𝑘 = 𝑧 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) )
140 136 139 oveq12d ⊢ ( 𝑘 = 𝑧 → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
141 6 93 97 98 117 119 120 135 140 gsumunsn ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
142 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
143 123 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
144 10 3 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
145 8 144 syl ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
146 145 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → 0 ∈ ( Base ‘ 𝑅 ) )
147 143 146 ifcld ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ∈ ( Base ‘ 𝑅 ) )
148 147 fmpttd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
149 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
150 149 18 elmap ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
151 148 150 sylibr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
152 33 10 2 34 131 psrbas ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
153 151 152 eleqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
154 18 mptex ⊢ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V
155 funmpt ⊢ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
156 154 155 20 3pm3.2i ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∧ 0 ∈ V )
157 156 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∧ 0 ∈ V ) )
158 eldifn ⊢ ( 𝑦 ∈ ( 𝐷 ∖ 𝑥 ) → ¬ 𝑦 ∈ 𝑥 )
159 158 adantl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ 𝑥 ) ) → ¬ 𝑦 ∈ 𝑥 )
160 159 iffalsed ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ 𝑥 ) ) → if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) = 0 )
161 18 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝐷 ∈ V )
162 160 161 suppss2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) supp 0 ) ⊆ 𝑥 )
163 suppssfifsupp ⊢ ( ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∧ 0 ∈ V ) ∧ ( 𝑥 ∈ Fin ∧ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) supp 0 ) ⊆ 𝑥 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) finSupp 0 )
164 157 98 162 163 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) finSupp 0 )
165 1 33 34 3 6 mplelbas ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ 𝐵 ↔ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) finSupp 0 ) )
166 153 164 165 sylanbrc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ 𝐵 )
167 1 6 142 93 166 135 mpladd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
168 ovexd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ∈ V )
169 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
170 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
171 1 7 10 6 170 2 127 133 mplvsca ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
172 127 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
173 10 4 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
174 173 144 ifcld ⊢ ( 𝑅 ∈ Ring → if ( 𝑦 = 𝑧 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
175 8 174 syl ⊢ ( 𝜑 → if ( 𝑦 = 𝑧 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
176 175 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 = 𝑧 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
177 fconstmpt ⊢ ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑧 ) )
178 177 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑧 ) ) )
179 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) )
180 161 172 176 178 179 offval2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
181 171 180 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
182 161 147 168 169 181 offval2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
183 132 82 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑅 ∈ Grp )
184 10 142 3 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑧 ) )
185 183 127 184 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑧 ) )
186 185 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑧 ) )
187 velsn ⊢ ( 𝑦 ∈ { 𝑧 } ↔ 𝑦 = 𝑧 )
188 187 bilani ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → 𝑦 = 𝑧 )
189 188 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( 𝑋 ‘ 𝑦 ) = ( 𝑋 ‘ 𝑧 ) )
190 186 189 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑦 ) )
191 120 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑧 ∈ 𝑥 )
192 188 191 eqneltrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑦 ∈ 𝑥 )
193 192 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) = 0 )
194 188 iftrued ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 = 𝑧 , 1 , 0 ) = 1 )
195 194 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) )
196 10 170 4 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑧 ) )
197 132 127 196 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑧 ) )
198 197 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑧 ) )
199 195 198 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( 𝑋 ‘ 𝑧 ) )
200 193 199 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) )
201 elun2 ⊢ ( 𝑦 ∈ { 𝑧 } → 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) )
202 201 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) )
203 202 iftrued ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
204 190 200 203 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
205 83 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝑅 ∈ Grp )
206 10 142 3 grprid ⊢ ( ( 𝑅 ∈ Grp ∧ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ∈ ( Base ‘ 𝑅 ) ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
207 205 147 206 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
208 207 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
209 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑦 ∈ { 𝑧 } )
210 209 187 sylnib ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑦 = 𝑧 )
211 210 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 = 𝑧 , 1 , 0 ) = 0 )
212 211 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) )
213 10 170 3 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
214 132 127 213 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
215 214 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
216 212 215 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = 0 )
217 216 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) )
218 elun ⊢ ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ ( 𝑦 ∈ 𝑥 ∨ 𝑦 ∈ { 𝑧 } ) )
219 orcom ⊢ ( ( 𝑦 ∈ 𝑥 ∨ 𝑦 ∈ { 𝑧 } ) ↔ ( 𝑦 ∈ { 𝑧 } ∨ 𝑦 ∈ 𝑥 ) )
220 218 219 bitri ⊢ ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ ( 𝑦 ∈ { 𝑧 } ∨ 𝑦 ∈ 𝑥 ) )
221 biorf ⊢ ( ¬ 𝑦 ∈ { 𝑧 } → ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ { 𝑧 } ∨ 𝑦 ∈ 𝑥 ) ) )
222 220 221 bitr4id ⊢ ( ¬ 𝑦 ∈ { 𝑧 } → ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ 𝑦 ∈ 𝑥 ) )
223 222 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ 𝑦 ∈ 𝑥 ) )
224 223 ifbid ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
225 208 217 224 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
226 204 225 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
227 226 mpteq2dva ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
228 167 182 227 3eqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
229 141 228 eqeq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) ) )
230 92 229 imbitrrid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
231 230 expr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
232 231 a2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
233 91 232 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
234 233 expcom ⊢ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) → ( 𝜑 → ( ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
235 234 a2d ⊢ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) → ( ( 𝜑 → ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) → ( 𝜑 → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
236 54 63 72 81 87 235 findcard2s ⊢ ( ( 𝑋 supp 0 ) ∈ Fin → ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
237 38 236 mpcom ⊢ ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
238 32 237 mpd ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
239 30 238 eqtr4d ⊢ ( 𝜑 → 𝑋 = ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
240 32 resmptd ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ↾ ( 𝑋 supp 0 ) ) = ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
241 240 oveq2d ⊢ ( 𝜑 → ( 𝑃 Σg ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ↾ ( 𝑋 supp 0 ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
242 115 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) : 𝐷 ⟶ 𝐵 )
243 11 16 19 21 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 𝑋 ‘ 𝑘 ) = 0 )
244 243 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) )
245 eldifi ⊢ ( 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) → 𝑘 ∈ 𝐷 )
246 107 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
247 3 246 eqtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
248 247 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) )
249 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
250 6 112 7 249 44 lmod0vs ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
251 104 111 250 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
252 248 251 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
253 245 252 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
254 244 253 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
255 254 19 suppss2 ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) supp ( 0g ‘ 𝑃 ) ) ⊆ ( 𝑋 supp 0 ) )
256 18 mptex ⊢ ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V
257 funmpt ⊢ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) )
258 fvex ⊢ ( 0g ‘ 𝑃 ) ∈ V
259 256 257 258 3pm3.2i ⊢ ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V )
260 259 a1i ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V ) )
261 suppssfifsupp ⊢ ( ( ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V ) ∧ ( ( 𝑋 supp 0 ) ∈ Fin ∧ ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) supp ( 0g ‘ 𝑃 ) ) ⊆ ( 𝑋 supp 0 ) ) ) → ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) finSupp ( 0g ‘ 𝑃 ) )
262 260 38 255 261 syl12anc ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) finSupp ( 0g ‘ 𝑃 ) )
263 6 44 96 19 242 255 262 gsumres ⊢ ( 𝜑 → ( 𝑃 Σg ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ↾ ( 𝑋 supp 0 ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
264 241 263 eqtr3d ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
265 239 264 eqtrd ⊢ ( 𝜑 → 𝑋 = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )