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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σ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 19 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑥 } ) ∈ V )
78 77 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ V )
79 78 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ V )
80 funmpt ⊢ Fun ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) )
81 80 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → Fun ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) )
82 25 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑓 finSupp 0 )
83 ssdif ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼 → ( ( 𝐼 ∖ { 𝑥 } ) ∖ ( 𝑓 supp 0 ) ) ⊆ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) )
84 57 83 ax-mp ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ∖ ( 𝑓 supp 0 ) ) ⊆ ( 𝐼 ∖ ( 𝑓 supp 0 ) )
85 84 sseli ⊢ ( 𝑘 ∈ ( ( 𝐼 ∖ { 𝑥 } ) ∖ ( 𝑓 supp 0 ) ) → 𝑘 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) )
86 ssidd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 supp 0 ) ⊆ ( 𝑓 supp 0 ) )
87 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ V )
88 5 fvexi ⊢ 0 ∈ V
89 88 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 0 ∈ V )
90 65 86 87 89 suppssr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( 𝑓 ‘ 𝑘 ) = 0 )
91 85 90 sylan2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑘 ∈ ( ( 𝐼 ∖ { 𝑥 } ) ∖ ( 𝑓 supp 0 ) ) ) → ( 𝑓 ‘ 𝑘 ) = 0 )
92 77 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐼 ∖ { 𝑥 } ) ∈ V )
93 91 92 suppss2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) supp 0 ) ⊆ ( 𝑓 supp 0 ) )
94 fsuppsssupp ⊢ ( ( ( ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ V ∧ Fun ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) supp 0 ) ⊆ ( 𝑓 supp 0 ) ) ) → ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) finSupp 0 )
95 79 81 82 93 94 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) finSupp 0 )
96 56 60 64 76 95 dprdwd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ { ℎ ∈ X 𝑖 ∈ ( 𝐼 ∖ { 𝑥 } ) ( ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ‘ 𝑖 ) ∣ ℎ finSupp 0 } )
97 70 96 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ∈ { ℎ ∈ X 𝑖 ∈ ( 𝐼 ∖ { 𝑥 } ) ( ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ‘ 𝑖 ) ∣ ℎ finSupp 0 } )
98 5 56 60 64 97 eldprdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) )
99 26 98 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) )
100 55 99 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → 𝐴 ∈ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) )
101 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
102 eqid ⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
103 61 15 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
104 dprdsubg ⊢ ( 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
105 60 104 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
106 13 14 15 5 dpjdisj ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } )
107 13 14 15 33 dpjcntz ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
108 101 102 5 33 103 105 106 107 27 pj1rid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝐴 ∈ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) → ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = 0 )
109 26 108 sylanl2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) ∧ 𝐴 ∈ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) → ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = 0 )
110 100 109 mpdan ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = 0 )
111 30 110 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝑓 supp 0 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = 0 )
112 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝐼 ∈ V )
113 111 112 suppss2 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) supp 0 ) ⊆ ( 𝑓 supp 0 ) )
114 fsuppsssupp ⊢ ( ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ V ∧ Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑓 finSupp 0 ∧ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) supp 0 ) ⊆ ( 𝑓 supp 0 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) finSupp 0 )
115 21 23 25 113 114 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) finSupp 0 )
116 6 11 12 18 115 dprdwd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ 𝑊 )
117 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝐴 = ( 𝐺 Σg 𝑓 ) )
118 39 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ‘ 𝑥 ) ) )
119 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐴 = ( 𝐺 Σg 𝑓 ) )
120 13 34 35 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐺 ∈ Mnd )
121 6 13 14 41 dprdffsupp ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑓 finSupp 0 )
122 disjdif ⊢ ( { 𝑥 } ∩ ( 𝐼 ∖ { 𝑥 } ) ) = ∅
123 122 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( { 𝑥 } ∩ ( 𝐼 ∖ { 𝑥 } ) ) = ∅ )
124 undif2 ⊢ ( { 𝑥 } ∪ ( 𝐼 ∖ { 𝑥 } ) ) = ( { 𝑥 } ∪ 𝐼 )
125 15 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → { 𝑥 } ⊆ 𝐼 )
126 ssequn1 ⊢ ( { 𝑥 } ⊆ 𝐼 ↔ ( { 𝑥 } ∪ 𝐼 ) = 𝐼 )
127 125 126 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( { 𝑥 } ∪ 𝐼 ) = 𝐼 )
128 124 127 eqtr2id ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 = ( { 𝑥 } ∪ ( 𝐼 ∖ { 𝑥 } ) ) )
129 32 5 101 33 120 87 65 42 121 123 128 gsumzsplit ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 Σg 𝑓 ) = ( ( 𝐺 Σg ( 𝑓 ↾ { 𝑥 } ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
130 65 125 feqresmpt ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ↾ { 𝑥 } ) = ( 𝑘 ∈ { 𝑥 } ↦ ( 𝑓 ‘ 𝑘 ) ) )
131 130 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 Σg ( 𝑓 ↾ { 𝑥 } ) ) = ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 } ↦ ( 𝑓 ‘ 𝑘 ) ) ) )
132 65 15 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
133 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑥 ) )
134 32 133 gsumsn ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐼 ∧ ( 𝑓 ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 } ↦ ( 𝑓 ‘ 𝑘 ) ) ) = ( 𝑓 ‘ 𝑥 ) )
135 120 15 132 134 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 } ↦ ( 𝑓 ‘ 𝑘 ) ) ) = ( 𝑓 ‘ 𝑥 ) )
136 131 135 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 Σg ( 𝑓 ↾ { 𝑥 } ) ) = ( 𝑓 ‘ 𝑥 ) )
137 136 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐺 Σg ( 𝑓 ↾ { 𝑥 } ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
138 119 129 137 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐴 = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
139 13 14 15 102 dpjlsm ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 DProd 𝑆 ) = ( ( 𝑆 ‘ 𝑥 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
140 17 139 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐴 ∈ ( ( 𝑆 ‘ 𝑥 ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
141 6 11 12 24 dprdfcl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) )
142 101 102 5 33 103 105 106 107 27 140 141 98 pj1eq ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐴 = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ↔ ( ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = ( 𝑓 ‘ 𝑥 ) ∧ ( ( ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ( proj1 ‘ 𝐺 ) ( 𝑆 ‘ 𝑥 ) ) ‘ 𝐴 ) = ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ) )
143 138 142 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = ( 𝑓 ‘ 𝑥 ) ∧ ( ( ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ( proj1 ‘ 𝐺 ) ( 𝑆 ‘ 𝑥 ) ) ‘ 𝐴 ) = ( 𝐺 Σg ( 𝑓 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
144 143 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑆 ‘ 𝑥 ) ( proj1 ‘ 𝐺 ) ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ‘ 𝐴 ) = ( 𝑓 ‘ 𝑥 ) )
145 29 144 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = ( 𝑓 ‘ 𝑥 ) )
146 145 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ‘ 𝑥 ) ) )
147 118 146 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝑓 = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) )
148 147 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( 𝐺 Σg 𝑓 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )
149 117 148 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )
150 116 149 jca ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg 𝑓 ) ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ) )
151 10 150 rexlimddv ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ∈ 𝑊 ∧ 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ) )