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 ifid ⊢ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , ( 𝑋 ‘ 𝑦 ) ) = ( 𝑋 ‘ 𝑦 )
17 ssidd ⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ ( 𝑋 supp 0 ) )
18 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
19 2 18 rabex2 ⊢ 𝐷 ∈ V
20 19 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
21 3 fvexi ⊢ 0 ∈ V
22 21 a1i ⊢ ( 𝜑 → 0 ∈ V )
23 11 17 20 22 suppssr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 𝑋 ‘ 𝑦 ) = 0 )
24 23 ifeq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , ( 𝑋 ‘ 𝑦 ) ) = if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
25 16 24 syl5reqr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 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 mplring ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
95 5 8 94 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ Ring )
96 ringcmn ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
97 95 96 syl ⊢ ( 𝜑 → 𝑃 ∈ CMnd )
98 97 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑃 ∈ CMnd )
99 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑥 ∈ Fin )
100 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 )
101 100 unssad ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑥 ⊆ 𝐷 )
102 101 sselda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝐷 )
103 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝐼 ∈ 𝑊 )
104 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ Ring )
105 1 mpllmod ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
106 103 104 105 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑃 ∈ LMod )
107 11 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
108 1 5 8 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
109 108 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
110 109 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
111 107 110 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
112 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑘 ∈ 𝐷 )
113 1 6 3 4 2 103 104 112 mplmon ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ∈ 𝐵 )
114 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
115 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
116 6 114 7 115 lmodvscl ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
117 106 111 113 116 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
118 117 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
119 102 118 syldan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑘 ∈ 𝑥 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
120 vex ⊢ 𝑧 ∈ V
121 120 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑧 ∈ V )
122 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ¬ 𝑧 ∈ 𝑥 )
123 5 8 105 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ LMod )
124 123 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑃 ∈ LMod )
125 11 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
126 100 unssbd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → { 𝑧 } ⊆ 𝐷 )
127 120 snss ⊢ ( 𝑧 ∈ 𝐷 ↔ { 𝑧 } ⊆ 𝐷 )
128 126 127 sylibr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑧 ∈ 𝐷 )
129 125 128 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
130 108 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
131 130 fveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
132 129 131 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
133 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝐼 ∈ 𝑊 )
134 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑅 ∈ Ring )
135 1 6 3 4 2 133 134 128 mplmon ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ∈ 𝐵 )
136 6 114 7 115 lmodvscl ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ∈ 𝐵 )
137 124 132 135 136 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ∈ 𝐵 )
138 fveq2 ⊢ ( 𝑘 = 𝑧 → ( 𝑋 ‘ 𝑘 ) = ( 𝑋 ‘ 𝑧 ) )
139 equequ2 ⊢ ( 𝑘 = 𝑧 → ( 𝑦 = 𝑘 ↔ 𝑦 = 𝑧 ) )
140 139 ifbid ⊢ ( 𝑘 = 𝑧 → if ( 𝑦 = 𝑘 , 1 , 0 ) = if ( 𝑦 = 𝑧 , 1 , 0 ) )
141 140 mpteq2dv ⊢ ( 𝑘 = 𝑧 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) )
142 138 141 oveq12d ⊢ ( 𝑘 = 𝑧 → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
143 6 93 98 99 119 121 122 137 142 gsumunsn ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
144 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
145 125 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
146 10 3 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
147 8 146 syl ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
148 147 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → 0 ∈ ( Base ‘ 𝑅 ) )
149 145 148 ifcld ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ∈ ( Base ‘ 𝑅 ) )
150 149 fmpttd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
151 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
152 151 19 elmap ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
153 150 152 sylibr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
154 33 10 2 34 133 psrbas ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
155 153 154 eleqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
156 19 mptex ⊢ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V
157 funmpt ⊢ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
158 156 157 21 3pm3.2i ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∧ 0 ∈ V )
159 158 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∧ 0 ∈ V ) )
160 eldifn ⊢ ( 𝑦 ∈ ( 𝐷 ∖ 𝑥 ) → ¬ 𝑦 ∈ 𝑥 )
161 160 adantl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ 𝑥 ) ) → ¬ 𝑦 ∈ 𝑥 )
162 161 iffalsed ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ 𝑥 ) ) → if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) = 0 )
163 19 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝐷 ∈ V )
164 162 163 suppss2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) supp 0 ) ⊆ 𝑥 )
165 suppssfifsupp ⊢ ( ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∧ 0 ∈ V ) ∧ ( 𝑥 ∈ Fin ∧ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) supp 0 ) ⊆ 𝑥 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) finSupp 0 )
166 159 99 164 165 syl12anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) finSupp 0 )
167 1 33 34 3 6 mplelbas ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ 𝐵 ↔ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) finSupp 0 ) )
168 155 166 167 sylanbrc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ 𝐵 )
169 1 6 144 93 168 137 mpladd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
170 ovexd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ∈ V )
171 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
172 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
173 1 7 10 6 172 2 129 135 mplvsca ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
174 129 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
175 10 4 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
176 175 146 ifcld ⊢ ( 𝑅 ∈ Ring → if ( 𝑦 = 𝑧 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
177 8 176 syl ⊢ ( 𝜑 → if ( 𝑦 = 𝑧 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
178 177 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 = 𝑧 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
179 fconstmpt ⊢ ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑧 ) )
180 179 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑧 ) ) )
181 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) )
182 163 174 178 180 181 offval2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
183 173 182 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
184 163 149 170 171 183 offval2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
185 134 82 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑅 ∈ Grp )
186 10 144 3 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑧 ) )
187 185 129 186 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑧 ) )
188 187 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑧 ) )
189 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → 𝑦 ∈ { 𝑧 } )
190 velsn ⊢ ( 𝑦 ∈ { 𝑧 } ↔ 𝑦 = 𝑧 )
191 189 190 sylib ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → 𝑦 = 𝑧 )
192 191 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( 𝑋 ‘ 𝑦 ) = ( 𝑋 ‘ 𝑧 ) )
193 188 192 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑦 ) )
194 122 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑧 ∈ 𝑥 )
195 191 194 eqneltrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑦 ∈ 𝑥 )
196 195 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) = 0 )
197 191 iftrued ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 = 𝑧 , 1 , 0 ) = 1 )
198 197 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) )
199 10 172 4 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑧 ) )
200 134 129 199 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑧 ) )
201 200 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑧 ) )
202 198 201 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( 𝑋 ‘ 𝑧 ) )
203 196 202 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) )
204 elun2 ⊢ ( 𝑦 ∈ { 𝑧 } → 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) )
205 204 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) )
206 205 iftrued ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
207 193 203 206 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
208 83 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝑅 ∈ Grp )
209 10 144 3 grprid ⊢ ( ( 𝑅 ∈ Grp ∧ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ∈ ( Base ‘ 𝑅 ) ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
210 208 149 209 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
211 210 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
212 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑦 ∈ { 𝑧 } )
213 212 190 sylnib ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑦 = 𝑧 )
214 213 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 = 𝑧 , 1 , 0 ) = 0 )
215 214 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) )
216 10 172 3 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
217 134 129 216 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
218 217 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
219 215 218 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = 0 )
220 219 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) )
221 biorf ⊢ ( ¬ 𝑦 ∈ { 𝑧 } → ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ { 𝑧 } ∨ 𝑦 ∈ 𝑥 ) ) )
222 elun ⊢ ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ ( 𝑦 ∈ 𝑥 ∨ 𝑦 ∈ { 𝑧 } ) )
223 orcom ⊢ ( ( 𝑦 ∈ 𝑥 ∨ 𝑦 ∈ { 𝑧 } ) ↔ ( 𝑦 ∈ { 𝑧 } ∨ 𝑦 ∈ 𝑥 ) )
224 222 223 bitri ⊢ ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ ( 𝑦 ∈ { 𝑧 } ∨ 𝑦 ∈ 𝑥 ) )
225 221 224 syl6rbbr ⊢ ( ¬ 𝑦 ∈ { 𝑧 } → ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ 𝑦 ∈ 𝑥 ) )
226 225 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ 𝑦 ∈ 𝑥 ) )
227 226 ifbid ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
228 211 220 227 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
229 207 228 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
230 229 mpteq2dva ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
231 169 184 230 3eqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
232 143 231 eqeq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) ) )
233 92 232 syl5ibr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
234 233 expr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 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 91 235 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
237 236 expcom ⊢ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) → ( 𝜑 → ( ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
238 237 a2d ⊢ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) → ( ( 𝜑 → ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) → ( 𝜑 → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
239 54 63 72 81 87 238 findcard2s ⊢ ( ( 𝑋 supp 0 ) ∈ Fin → ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
240 38 239 mpcom ⊢ ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
241 32 240 mpd ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
242 30 241 eqtr4d ⊢ ( 𝜑 → 𝑋 = ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
243 32 resmptd ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ↾ ( 𝑋 supp 0 ) ) = ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
244 243 oveq2d ⊢ ( 𝜑 → ( 𝑃 Σg ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ↾ ( 𝑋 supp 0 ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
245 117 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) : 𝐷 ⟶ 𝐵 )
246 11 17 20 22 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 𝑋 ‘ 𝑘 ) = 0 )
247 246 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) )
248 eldifi ⊢ ( 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) → 𝑘 ∈ 𝐷 )
249 109 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
250 3 249 syl5eq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
251 250 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) )
252 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
253 6 114 7 252 44 lmod0vs ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
254 106 113 253 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
255 251 254 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
256 248 255 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
257 247 256 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
258 257 20 suppss2 ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) supp ( 0g ‘ 𝑃 ) ) ⊆ ( 𝑋 supp 0 ) )
259 19 mptex ⊢ ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V
260 funmpt ⊢ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) )
261 fvex ⊢ ( 0g ‘ 𝑃 ) ∈ V
262 259 260 261 3pm3.2i ⊢ ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V )
263 262 a1i ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V ) )
264 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 ‘ 𝑃 ) )
265 263 38 258 264 syl12anc ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) finSupp ( 0g ‘ 𝑃 ) )
266 6 44 97 20 245 258 265 gsumres ⊢ ( 𝜑 → ( 𝑃 Σg ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ↾ ( 𝑋 supp 0 ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
267 244 266 eqtr3d ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
268 242 267 eqtrd ⊢ ( 𝜑 → 𝑋 = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )