Metamath Proof Explorer

Theorem dpjidcl

Description: The key property of projections: the sum of all the projections of A is A . (Contributed by Mario Carneiro, 26-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dpjfval.p ⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
dpjidcl.3 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 DProd 𝑆 ) )
dpjidcl.0 ⊢ 0 = ( 0g ‘ 𝐺 )
dpjidcl.w ⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
Assertion dpjidcl ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dpjfval.p ⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4 dpjidcl.3 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 DProd 𝑆 ) )
5 dpjidcl.0 ⊢ 0 = ( 0g ‘ 𝐺 )
6 dpjidcl.w ⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
7 5 6 eldprd ⊢ ( dom 𝑆 = 𝐼 → ( 𝐴 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ 𝑊 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) )
8 2 7 syl ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ 𝑊 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) )
9 4 8 mpbid ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ 𝑊 𝐴 = ( 𝐺 Σg 𝑓 ) ) )
10 9 simprd ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑊 𝐴 = ( 𝐺 Σg 𝑓 ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝐺 dom DProd 𝑆 )
12 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → dom 𝑆 = 𝐼 )
13 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐺 dom DProd 𝑆 )
14 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → dom 𝑆 = 𝐼 )
15 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
16 13 14 3 15 dpjf ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑃 ‘ 𝑥 ) : ( 𝐺 DProd 𝑆 ) ⟶ ( 𝑆 ‘ 𝑥 ) )
17 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐴 ∈ ( 𝐺 DProd 𝑆 ) )
18 16 17 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ∈ ( 𝑆 ‘ 𝑥 ) )
19 1 2 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
20 19 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ V )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ V )
22 funmpt ⊢ Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) )
23 22 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) )
24 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 ∈ 𝑊 )
25 6 11 12 24 dprdffsupp ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 finSupp 0 )
26 eldifi ⊢ ( 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) → 𝑥 ∈ 𝐼 )
27 eqid ⊢ ( proj1 ‘ 𝐺 ) = ( proj1 ‘ 𝐺 )
28 13 14 3 27 15 dpjval ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑃 ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
29 28 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) )
30 26 29 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) )
31 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → 𝐴 = ( 𝐺 Σg 𝑓 ) )
32 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
33 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
34 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
35 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
36 11 34 35 3syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝐺 ∈ Mnd )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → 𝐺 ∈ Mnd )
38 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → 𝐼 ∈ V )
39 6 11 12 24 32 dprdff ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → 𝑓 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
41 24 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑓 ∈ 𝑊 )
42 6 13 14 41 33 dprdfcntz ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ran 𝑓 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝑓 ) )
43 26 42 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ran 𝑓 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝑓 ) )
44 snssi ⊢ ( 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) → { 𝑥 } ⊆ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) )
45 44 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → { 𝑥 } ⊆ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) )
46 45 difss2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → { 𝑥 } ⊆ 𝐼 )
47 suppssdm ⊢ ( 𝑓 supp 0 ) ⊆ dom 𝑓
48 47 39 fssdm ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑓 supp 0 ) ⊆ 𝐼 )
49 48 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( 𝑓 supp 0 ) ⊆ 𝐼 )
50 ssconb ⊢ ( ( { 𝑥 } ⊆ 𝐼 ∧ ( 𝑓 supp 0 ) ⊆ 𝐼 ) → ( { 𝑥 } ⊆ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ↔ ( 𝑓 supp 0 ) ⊆ ( 𝐼 ∖ { 𝑥 } ) ) )
51 46 49 50 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( { 𝑥 } ⊆ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ↔ ( 𝑓 supp 0 ) ⊆ ( 𝐼 ∖ { 𝑥 } ) ) )
52 45 51 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( 𝑓 supp 0 ) ⊆ ( 𝐼 ∖ { 𝑥 } ) )
53 25 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → 𝑓 finSupp 0 )
54 32 5 33 37 38 40 43 52 53 gsumzres ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) = ( 𝐺 Σg 𝑓 ) )
55 31 54 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → 𝐴 = ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) )
56 eqid ⊢ { ℎ ∈ X 𝑖 ∈ ( 𝐼 ∖ { 𝑥 } ) ( ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ‘ 𝑖 ) ∣ ℎ finSupp 0 } = { ℎ ∈ X 𝑖 ∈ ( 𝐼 ∖ { 𝑥 } ) ( ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ‘ 𝑖 ) ∣ ℎ finSupp 0 }
57 difss ⊢ ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼
58 57 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼 )
59 13 14 58 dprdres ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
60 59 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) )
61 13 14 dprdf2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
62 fssres ⊢ ( ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼 ) → ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) : ( 𝐼 ∖ { 𝑥 } ) ⟶ ( SubGrp ‘ 𝐺 ) )
63 61 57 62 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) : ( 𝐼 ∖ { 𝑥 } ) ⟶ ( SubGrp ‘ 𝐺 ) )
64 63 fdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → dom ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) = ( 𝐼 ∖ { 𝑥 } ) )
65 39 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑓 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
66 65 feqmptd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑓 = ( 𝑘 ∈ 𝐼 ↦ ( 𝑓 ‘ 𝑘 ) ) )
67 66 reseq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) = ( ( 𝑘 ∈ 𝐼 ↦ ( 𝑓 ‘ 𝑘 ) ) ↾ ( 𝐼 ∖ { 𝑥 } ) ) )
68 resmpt ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼 → ( ( 𝑘 ∈ 𝐼 ↦ ( 𝑓 ‘ 𝑘 ) ) ↾ ( 𝐼 ∖ { 𝑥 } ) ) = ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) )
69 57 68 ax-mp ⊢ ( ( 𝑘 ∈ 𝐼 ↦ ( 𝑓 ‘ 𝑘 ) ) ↾ ( 𝐼 ∖ { 𝑥 } ) ) = ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) )
70 67 69 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) = ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) )
71 eldifi ⊢ ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) → 𝑘 ∈ 𝐼 )
72 6 13 14 41 dprdfcl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
73 71 72 sylan2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
74 fvres ⊢ ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) → ( ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ‘ 𝑘 ) = ( 𝑆 ‘ 𝑘 ) )
75 74 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ) → ( ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ‘ 𝑘 ) = ( 𝑆 ‘ 𝑘 ) )
76 73 75 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ( ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ‘ 𝑘 ) )
77 difexg ⊢ ( 𝐼 ∈ V → ( 𝐼 ∖ { 𝑥 } ) ∈ V )
78 19 77 syl ⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑥 } ) ∈ V )
79 78 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ V )
80 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ V )
81 funmpt ⊢ Fun ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) )
82 81 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → Fun ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) )
83 25 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑓 finSupp 0 )
84 ssdif ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼 → ( ( 𝐼 ∖ { 𝑥 } ) ∖ ( 𝑓 supp 0 ) ) ⊆ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) )
85 57 84 ax-mp ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ∖ ( 𝑓 supp 0 ) ) ⊆ ( 𝐼 ∖ ( 𝑓 supp 0 ) )
86 85 sseli ⊢ ( 𝑘 ∈ ( ( 𝐼 ∖ { 𝑥 } ) ∖ ( 𝑓 supp 0 ) ) → 𝑘 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) )
87 ssidd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 supp 0 ) ⊆ ( 𝑓 supp 0 ) )
88 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ V )
89 5 fvexi ⊢ 0 ∈ V
90 89 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 0 ∈ V )
91 65 87 88 90 suppssr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( 𝑓 ‘ 𝑘 ) = 0 )
92 86 91 sylan2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 ∈ ( ( 𝐼 ∖ { 𝑥 } ) ∖ ( 𝑓 supp 0 ) ) ) → ( 𝑓 ‘ 𝑘 ) = 0 )
93 78 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐼 ∖ { 𝑥 } ) ∈ V )
94 92 93 suppss2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) supp 0 ) ⊆ ( 𝑓 supp 0 ) )
95 fsuppsssupp ⊢ ( ( ( ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ V ∧ Fun ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) supp 0 ) ⊆ ( 𝑓 supp 0 ) ) ) → ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) finSupp 0 )
96 80 82 83 94 95 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) finSupp 0 )
97 56 60 64 76 96 dprdwd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ { ℎ ∈ X 𝑖 ∈ ( 𝐼 ∖ { 𝑥 } ) ( ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ‘ 𝑖 ) ∣ ℎ finSupp 0 } )
98 70 97 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ∈ { ℎ ∈ X 𝑖 ∈ ( 𝐼 ∖ { 𝑥 } ) ( ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ‘ 𝑖 ) ∣ ℎ finSupp 0 } )
99 5 56 60 64 98 eldprdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) )
100 26 99 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) )
101 55 100 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → 𝐴 ∈ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) )
102 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
103 eqid ⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
104 61 15 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
105 dprdsubg ⊢ ( 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
106 60 105 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
107 13 14 15 5 dpjdisj ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } )
108 13 14 15 33 dpjcntz ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
109 102 103 5 33 104 106 107 108 27 pj1rid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝐴 ∈ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) → ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = 0 )
110 26 109 sylanl2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) ∧ 𝐴 ∈ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) → ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = 0 )
111 101 110 mpdan ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = 0 )
112 30 111 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = 0 )
113 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝐼 ∈ V )
114 112 113 suppss2 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) supp 0 ) ⊆ ( 𝑓 supp 0 ) )
115 fsuppsssupp ⊢ ( ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ V ∧ Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) supp 0 ) ⊆ ( 𝑓 supp 0 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) finSupp 0 )
116 21 23 25 114 115 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) finSupp 0 )
117 6 11 12 18 116 dprdwd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ 𝑊 )
118 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝐴 = ( 𝐺 Σg 𝑓 ) )
119 39 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ‘ 𝑥 ) ) )
120 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐴 = ( 𝐺 Σg 𝑓 ) )
121 13 34 35 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐺 ∈ Mnd )
122 6 13 14 41 dprdffsupp ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑓 finSupp 0 )
123 disjdif ⊢ ( { 𝑥 } ∩ ( 𝐼 ∖ { 𝑥 } ) ) = ∅
124 123 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( { 𝑥 } ∩ ( 𝐼 ∖ { 𝑥 } ) ) = ∅ )
125 undif2 ⊢ ( { 𝑥 } ∪ ( 𝐼 ∖ { 𝑥 } ) ) = ( { 𝑥 } ∪ 𝐼 )
126 15 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → { 𝑥 } ⊆ 𝐼 )
127 ssequn1 ⊢ ( { 𝑥 } ⊆ 𝐼 ↔ ( { 𝑥 } ∪ 𝐼 ) = 𝐼 )
128 126 127 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( { 𝑥 } ∪ 𝐼 ) = 𝐼 )
129 125 128 syl5req ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 = ( { 𝑥 } ∪ ( 𝐼 ∖ { 𝑥 } ) ) )
130 32 5 102 33 121 88 65 42 122 124 129 gsumzsplit ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 Σg 𝑓 ) = ( ( 𝐺 Σg ( 𝑓 ↾ { 𝑥 } ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
131 65 126 feqresmpt ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ↾ { 𝑥 } ) = ( 𝑘 ∈ { 𝑥 } ↦ ( 𝑓 ‘ 𝑘 ) ) )
132 131 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 Σg ( 𝑓 ↾ { 𝑥 } ) ) = ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 } ↦ ( 𝑓 ‘ 𝑘 ) ) ) )
133 65 15 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
134 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑥 ) )
135 32 134 gsumsn ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐼 ∧ ( 𝑓 ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 } ↦ ( 𝑓 ‘ 𝑘 ) ) ) = ( 𝑓 ‘ 𝑥 ) )
136 121 15 133 135 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 } ↦ ( 𝑓 ‘ 𝑘 ) ) ) = ( 𝑓 ‘ 𝑥 ) )
137 132 136 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 Σg ( 𝑓 ↾ { 𝑥 } ) ) = ( 𝑓 ‘ 𝑥 ) )
138 137 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐺 Σg ( 𝑓 ↾ { 𝑥 } ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
139 120 130 138 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐴 = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
140 13 14 15 103 dpjlsm ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 DProd 𝑆 ) = ( ( 𝑆 ‘ 𝑥 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
141 17 140 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐴 ∈ ( ( 𝑆 ‘ 𝑥 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
142 6 11 12 24 dprdfcl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) )
143 102 103 5 33 104 106 107 108 27 141 142 99 pj1eq ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐴 = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ↔ ( ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = ( 𝑓 ‘ 𝑥 ) ∧ ( ( ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ( proj1 ‘ 𝐺 ) ( 𝑆 ‘ 𝑥 ) ) ‘ 𝐴 ) = ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ) )
144 139 143 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = ( 𝑓 ‘ 𝑥 ) ∧ ( ( ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ( proj1 ‘ 𝐺 ) ( 𝑆 ‘ 𝑥 ) ) ‘ 𝐴 ) = ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
145 144 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = ( 𝑓 ‘ 𝑥 ) )
146 29 145 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = ( 𝑓 ‘ 𝑥 ) )
147 146 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ‘ 𝑥 ) ) )
148 119 147 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) )
149 148 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝐺 Σg 𝑓 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )
150 118 149 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )
151 117 150 jca ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ) )
152 10 151 rexlimddv ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ) )