Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dpjidcl Structured version   Visualization version   GIF version

Theorem dpjidcl 19102
 Description: The key property of projections: the sum of all the projections of 𝐴 is 𝐴. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.)
Hypotheses
Ref Expression
dpjfval.1 (𝜑𝐺dom DProd 𝑆)
dpjfval.2 (𝜑 → dom 𝑆 = 𝐼)
dpjfval.p 𝑃 = (𝐺dProj𝑆)
dpjidcl.3 (𝜑𝐴 ∈ (𝐺 DProd 𝑆))
dpjidcl.0 0 = (0g𝐺)
dpjidcl.w 𝑊 = {X𝑖𝐼 (𝑆𝑖) ∣ finSupp 0 }
Assertion
Ref Expression
dpjidcl (𝜑 → ((𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) ∈ 𝑊𝐴 = (𝐺 Σg (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)))))
Distinct variable groups:   𝑥,, 0   ,𝑖,𝐺,𝑥   𝑃,,𝑥   𝜑,𝑖,𝑥   ,𝐼,𝑖,𝑥   𝑥,𝑊   𝐴,,𝑥   𝑆,,𝑖,𝑥
Allowed substitution hints:   𝜑()   𝐴(𝑖)   𝑃(𝑖)   𝑊(,𝑖)   0 (𝑖)

Proof of Theorem dpjidcl
Dummy variables 𝑘 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dpjidcl.3 . . . 4 (𝜑𝐴 ∈ (𝐺 DProd 𝑆))
2 dpjfval.2 . . . . 5 (𝜑 → dom 𝑆 = 𝐼)
3 dpjidcl.0 . . . . . 6 0 = (0g𝐺)
4 dpjidcl.w . . . . . 6 𝑊 = {X𝑖𝐼 (𝑆𝑖) ∣ finSupp 0 }
53, 4eldprd 19048 . . . . 5 (dom 𝑆 = 𝐼 → (𝐴 ∈ (𝐺 DProd 𝑆) ↔ (𝐺dom DProd 𝑆 ∧ ∃𝑓𝑊 𝐴 = (𝐺 Σg 𝑓))))
62, 5syl 17 . . . 4 (𝜑 → (𝐴 ∈ (𝐺 DProd 𝑆) ↔ (𝐺dom DProd 𝑆 ∧ ∃𝑓𝑊 𝐴 = (𝐺 Σg 𝑓))))
71, 6mpbid 233 . . 3 (𝜑 → (𝐺dom DProd 𝑆 ∧ ∃𝑓𝑊 𝐴 = (𝐺 Σg 𝑓)))
87simprd 496 . 2 (𝜑 → ∃𝑓𝑊 𝐴 = (𝐺 Σg 𝑓))
9 dpjfval.1 . . . . 5 (𝜑𝐺dom DProd 𝑆)
109adantr 481 . . . 4 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → 𝐺dom DProd 𝑆)
112adantr 481 . . . 4 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → dom 𝑆 = 𝐼)
129ad2antrr 722 . . . . . 6 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝐺dom DProd 𝑆)
132ad2antrr 722 . . . . . 6 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → dom 𝑆 = 𝐼)
14 dpjfval.p . . . . . 6 𝑃 = (𝐺dProj𝑆)
15 simpr 485 . . . . . 6 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝑥𝐼)
1612, 13, 14, 15dpjf 19101 . . . . 5 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑃𝑥):(𝐺 DProd 𝑆)⟶(𝑆𝑥))
171ad2antrr 722 . . . . 5 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝐴 ∈ (𝐺 DProd 𝑆))
1816, 17ffvelrnd 6847 . . . 4 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → ((𝑃𝑥)‘𝐴) ∈ (𝑆𝑥))
199, 2dprddomcld 19045 . . . . . . 7 (𝜑𝐼 ∈ V)
2019mptexd 6985 . . . . . 6 (𝜑 → (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) ∈ V)
2120adantr 481 . . . . 5 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) ∈ V)
22 funmpt 6389 . . . . . 6 Fun (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴))
2322a1i 11 . . . . 5 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → Fun (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)))
24 simprl 767 . . . . . 6 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → 𝑓𝑊)
254, 10, 11, 24dprdffsupp 19058 . . . . 5 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → 𝑓 finSupp 0 )
26 eldifi 4106 . . . . . . . 8 (𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 )) → 𝑥𝐼)
27 eqid 2825 . . . . . . . . . 10 (proj1𝐺) = (proj1𝐺)
2812, 13, 14, 27, 15dpjval 19100 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑃𝑥) = ((𝑆𝑥)(proj1𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥})))))
2928fveq1d 6668 . . . . . . . 8 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → ((𝑃𝑥)‘𝐴) = (((𝑆𝑥)(proj1𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))‘𝐴))
3026, 29sylan2 592 . . . . . . 7 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → ((𝑃𝑥)‘𝐴) = (((𝑆𝑥)(proj1𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))‘𝐴))
31 simplrr 774 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → 𝐴 = (𝐺 Σg 𝑓))
32 eqid 2825 . . . . . . . . . . 11 (Base‘𝐺) = (Base‘𝐺)
33 eqid 2825 . . . . . . . . . . 11 (Cntz‘𝐺) = (Cntz‘𝐺)
34 dprdgrp 19049 . . . . . . . . . . . . 13 (𝐺dom DProd 𝑆𝐺 ∈ Grp)
35 grpmnd 18042 . . . . . . . . . . . . 13 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
3610, 34, 353syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → 𝐺 ∈ Mnd)
3736adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → 𝐺 ∈ Mnd)
3819ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → 𝐼 ∈ V)
394, 10, 11, 24, 32dprdff 19056 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → 𝑓:𝐼⟶(Base‘𝐺))
4039adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → 𝑓:𝐼⟶(Base‘𝐺))
4124adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝑓𝑊)
424, 12, 13, 41, 33dprdfcntz 19059 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → ran 𝑓 ⊆ ((Cntz‘𝐺)‘ran 𝑓))
4326, 42sylan2 592 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → ran 𝑓 ⊆ ((Cntz‘𝐺)‘ran 𝑓))
44 snssi 4739 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 )) → {𝑥} ⊆ (𝐼 ∖ (𝑓 supp 0 )))
4544adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → {𝑥} ⊆ (𝐼 ∖ (𝑓 supp 0 )))
4645difss2d 4114 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → {𝑥} ⊆ 𝐼)
47 suppssdm 7837 . . . . . . . . . . . . . . 15 (𝑓 supp 0 ) ⊆ dom 𝑓
4847, 39fssdm 6526 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → (𝑓 supp 0 ) ⊆ 𝐼)
4948adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → (𝑓 supp 0 ) ⊆ 𝐼)
50 ssconb 4117 . . . . . . . . . . . . 13 (({𝑥} ⊆ 𝐼 ∧ (𝑓 supp 0 ) ⊆ 𝐼) → ({𝑥} ⊆ (𝐼 ∖ (𝑓 supp 0 )) ↔ (𝑓 supp 0 ) ⊆ (𝐼 ∖ {𝑥})))
5146, 49, 50syl2anc 584 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → ({𝑥} ⊆ (𝐼 ∖ (𝑓 supp 0 )) ↔ (𝑓 supp 0 ) ⊆ (𝐼 ∖ {𝑥})))
5245, 51mpbid 233 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → (𝑓 supp 0 ) ⊆ (𝐼 ∖ {𝑥}))
5325adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → 𝑓 finSupp 0 )
5432, 3, 33, 37, 38, 40, 43, 52, 53gsumzres 18951 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → (𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥}))) = (𝐺 Σg 𝑓))
5531, 54eqtr4d 2863 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → 𝐴 = (𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥}))))
56 eqid 2825 . . . . . . . . . . 11 {X𝑖 ∈ (𝐼 ∖ {𝑥})((𝑆 ↾ (𝐼 ∖ {𝑥}))‘𝑖) ∣ finSupp 0 } = {X𝑖 ∈ (𝐼 ∖ {𝑥})((𝑆 ↾ (𝐼 ∖ {𝑥}))‘𝑖) ∣ finSupp 0 }
57 difss 4111 . . . . . . . . . . . . . 14 (𝐼 ∖ {𝑥}) ⊆ 𝐼
5857a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐼 ∖ {𝑥}) ⊆ 𝐼)
5912, 13, 58dprdres 19072 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐺dom DProd (𝑆 ↾ (𝐼 ∖ {𝑥})) ∧ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))) ⊆ (𝐺 DProd 𝑆)))
6059simpld 495 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝐺dom DProd (𝑆 ↾ (𝐼 ∖ {𝑥})))
6112, 13dprdf2 19051 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝑆:𝐼⟶(SubGrp‘𝐺))
62 fssres 6540 . . . . . . . . . . . . 13 ((𝑆:𝐼⟶(SubGrp‘𝐺) ∧ (𝐼 ∖ {𝑥}) ⊆ 𝐼) → (𝑆 ↾ (𝐼 ∖ {𝑥})):(𝐼 ∖ {𝑥})⟶(SubGrp‘𝐺))
6361, 57, 62sylancl 586 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑆 ↾ (𝐼 ∖ {𝑥})):(𝐼 ∖ {𝑥})⟶(SubGrp‘𝐺))
6463fdmd 6519 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → dom (𝑆 ↾ (𝐼 ∖ {𝑥})) = (𝐼 ∖ {𝑥}))
6539adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝑓:𝐼⟶(Base‘𝐺))
6665feqmptd 6729 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝑓 = (𝑘𝐼 ↦ (𝑓𝑘)))
6766reseq1d 5850 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑓 ↾ (𝐼 ∖ {𝑥})) = ((𝑘𝐼 ↦ (𝑓𝑘)) ↾ (𝐼 ∖ {𝑥})))
68 resmpt 5903 . . . . . . . . . . . . . 14 ((𝐼 ∖ {𝑥}) ⊆ 𝐼 → ((𝑘𝐼 ↦ (𝑓𝑘)) ↾ (𝐼 ∖ {𝑥})) = (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)))
6957, 68ax-mp 5 . . . . . . . . . . . . 13 ((𝑘𝐼 ↦ (𝑓𝑘)) ↾ (𝐼 ∖ {𝑥})) = (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘))
7067, 69syl6eq 2876 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑓 ↾ (𝐼 ∖ {𝑥})) = (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)))
71 eldifi 4106 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐼 ∖ {𝑥}) → 𝑘𝐼)
724, 12, 13, 41dprdfcl 19057 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) ∧ 𝑘𝐼) → (𝑓𝑘) ∈ (𝑆𝑘))
7371, 72sylan2 592 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) ∧ 𝑘 ∈ (𝐼 ∖ {𝑥})) → (𝑓𝑘) ∈ (𝑆𝑘))
74 fvres 6685 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐼 ∖ {𝑥}) → ((𝑆 ↾ (𝐼 ∖ {𝑥}))‘𝑘) = (𝑆𝑘))
7574adantl 482 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) ∧ 𝑘 ∈ (𝐼 ∖ {𝑥})) → ((𝑆 ↾ (𝐼 ∖ {𝑥}))‘𝑘) = (𝑆𝑘))
7673, 75eleqtrrd 2920 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) ∧ 𝑘 ∈ (𝐼 ∖ {𝑥})) → (𝑓𝑘) ∈ ((𝑆 ↾ (𝐼 ∖ {𝑥}))‘𝑘))
77 difexg 5227 . . . . . . . . . . . . . . . . 17 (𝐼 ∈ V → (𝐼 ∖ {𝑥}) ∈ V)
7819, 77syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐼 ∖ {𝑥}) ∈ V)
7978mptexd 6985 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)) ∈ V)
8079ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)) ∈ V)
81 funmpt 6389 . . . . . . . . . . . . . . 15 Fun (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘))
8281a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → Fun (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)))
8325adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝑓 finSupp 0 )
84 ssdif 4119 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∖ {𝑥}) ⊆ 𝐼 → ((𝐼 ∖ {𝑥}) ∖ (𝑓 supp 0 )) ⊆ (𝐼 ∖ (𝑓 supp 0 )))
8557, 84ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝐼 ∖ {𝑥}) ∖ (𝑓 supp 0 )) ⊆ (𝐼 ∖ (𝑓 supp 0 ))
8685sseli 3966 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((𝐼 ∖ {𝑥}) ∖ (𝑓 supp 0 )) → 𝑘 ∈ (𝐼 ∖ (𝑓 supp 0 )))
87 ssidd 3993 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑓 supp 0 ) ⊆ (𝑓 supp 0 ))
8819ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝐼 ∈ V)
893fvexi 6680 . . . . . . . . . . . . . . . . . 18 0 ∈ V
9089a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 0 ∈ V)
9165, 87, 88, 90suppssr 7855 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) ∧ 𝑘 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → (𝑓𝑘) = 0 )
9286, 91sylan2 592 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) ∧ 𝑘 ∈ ((𝐼 ∖ {𝑥}) ∖ (𝑓 supp 0 ))) → (𝑓𝑘) = 0 )
9378ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐼 ∖ {𝑥}) ∈ V)
9492, 93suppss2 7858 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → ((𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)) supp 0 ) ⊆ (𝑓 supp 0 ))
95 fsuppsssupp 8841 . . . . . . . . . . . . . 14 ((((𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)) ∈ V ∧ Fun (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘))) ∧ (𝑓 finSupp 0 ∧ ((𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)) supp 0 ) ⊆ (𝑓 supp 0 ))) → (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)) finSupp 0 )
9680, 82, 83, 94, 95syl22anc 836 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)) finSupp 0 )
9756, 60, 64, 76, 96dprdwd 19055 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑘 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑓𝑘)) ∈ {X𝑖 ∈ (𝐼 ∖ {𝑥})((𝑆 ↾ (𝐼 ∖ {𝑥}))‘𝑖) ∣ finSupp 0 })
9870, 97eqeltrd 2917 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑓 ↾ (𝐼 ∖ {𝑥})) ∈ {X𝑖 ∈ (𝐼 ∖ {𝑥})((𝑆 ↾ (𝐼 ∖ {𝑥}))‘𝑖) ∣ finSupp 0 })
993, 56, 60, 64, 98eldprdi 19062 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥}))) ∈ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))
10026, 99sylan2 592 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → (𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥}))) ∈ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))
10155, 100eqeltrd 2917 . . . . . . . 8 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → 𝐴 ∈ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))
102 eqid 2825 . . . . . . . . . 10 (+g𝐺) = (+g𝐺)
103 eqid 2825 . . . . . . . . . 10 (LSSum‘𝐺) = (LSSum‘𝐺)
10461, 15ffvelrnd 6847 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑆𝑥) ∈ (SubGrp‘𝐺))
105 dprdsubg 19068 . . . . . . . . . . 11 (𝐺dom DProd (𝑆 ↾ (𝐼 ∖ {𝑥})) → (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
10660, 105syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))) ∈ (SubGrp‘𝐺))
10712, 13, 15, 3dpjdisj 19097 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → ((𝑆𝑥) ∩ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥})))) = { 0 })
10812, 13, 15, 33dpjcntz 19096 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥})))))
109102, 103, 3, 33, 104, 106, 107, 108, 27pj1rid 18750 . . . . . . . . 9 ((((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) ∧ 𝐴 ∈ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥})))) → (((𝑆𝑥)(proj1𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))‘𝐴) = 0 )
11026, 109sylanl2 677 . . . . . . . 8 ((((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) ∧ 𝐴 ∈ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥})))) → (((𝑆𝑥)(proj1𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))‘𝐴) = 0 )
111101, 110mpdan 683 . . . . . . 7 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → (((𝑆𝑥)(proj1𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))‘𝐴) = 0 )
11230, 111eqtrd 2860 . . . . . 6 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥 ∈ (𝐼 ∖ (𝑓 supp 0 ))) → ((𝑃𝑥)‘𝐴) = 0 )
11319adantr 481 . . . . . 6 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → 𝐼 ∈ V)
114112, 113suppss2 7858 . . . . 5 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → ((𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) supp 0 ) ⊆ (𝑓 supp 0 ))
115 fsuppsssupp 8841 . . . . 5 ((((𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) ∈ V ∧ Fun (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴))) ∧ (𝑓 finSupp 0 ∧ ((𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) supp 0 ) ⊆ (𝑓 supp 0 ))) → (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) finSupp 0 )
11621, 23, 25, 114, 115syl22anc 836 . . . 4 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) finSupp 0 )
1174, 10, 11, 18, 116dprdwd 19055 . . 3 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) ∈ 𝑊)
118 simprr 769 . . . 4 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → 𝐴 = (𝐺 Σg 𝑓))
11939feqmptd 6729 . . . . . 6 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → 𝑓 = (𝑥𝐼 ↦ (𝑓𝑥)))
120 simplrr 774 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝐴 = (𝐺 Σg 𝑓))
12112, 34, 353syl 18 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝐺 ∈ Mnd)
1224, 12, 13, 41dprdffsupp 19058 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝑓 finSupp 0 )
123 disjdif 4423 . . . . . . . . . . . . 13 ({𝑥} ∩ (𝐼 ∖ {𝑥})) = ∅
124123a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → ({𝑥} ∩ (𝐼 ∖ {𝑥})) = ∅)
125 undif2 4427 . . . . . . . . . . . . 13 ({𝑥} ∪ (𝐼 ∖ {𝑥})) = ({𝑥} ∪ 𝐼)
12615snssd 4740 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → {𝑥} ⊆ 𝐼)
127 ssequn1 4159 . . . . . . . . . . . . . 14 ({𝑥} ⊆ 𝐼 ↔ ({𝑥} ∪ 𝐼) = 𝐼)
128126, 127sylib 219 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → ({𝑥} ∪ 𝐼) = 𝐼)
129125, 128syl5req 2873 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝐼 = ({𝑥} ∪ (𝐼 ∖ {𝑥})))
13032, 3, 102, 33, 121, 88, 65, 42, 122, 124, 129gsumzsplit 18969 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐺 Σg 𝑓) = ((𝐺 Σg (𝑓 ↾ {𝑥}))(+g𝐺)(𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥})))))
13165, 126feqresmpt 6730 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑓 ↾ {𝑥}) = (𝑘 ∈ {𝑥} ↦ (𝑓𝑘)))
132131oveq2d 7167 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐺 Σg (𝑓 ↾ {𝑥})) = (𝐺 Σg (𝑘 ∈ {𝑥} ↦ (𝑓𝑘))))
13365, 15ffvelrnd 6847 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ (Base‘𝐺))
134 fveq2 6666 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝑓𝑘) = (𝑓𝑥))
13532, 134gsumsn 18996 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑥𝐼 ∧ (𝑓𝑥) ∈ (Base‘𝐺)) → (𝐺 Σg (𝑘 ∈ {𝑥} ↦ (𝑓𝑘))) = (𝑓𝑥))
136121, 15, 133, 135syl3anc 1365 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐺 Σg (𝑘 ∈ {𝑥} ↦ (𝑓𝑘))) = (𝑓𝑥))
137132, 136eqtrd 2860 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐺 Σg (𝑓 ↾ {𝑥})) = (𝑓𝑥))
138137oveq1d 7166 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → ((𝐺 Σg (𝑓 ↾ {𝑥}))(+g𝐺)(𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥})))) = ((𝑓𝑥)(+g𝐺)(𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥})))))
139120, 130, 1383eqtrd 2864 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝐴 = ((𝑓𝑥)(+g𝐺)(𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥})))))
14012, 13, 15, 103dpjlsm 19098 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐺 DProd 𝑆) = ((𝑆𝑥)(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥})))))
14117, 140eleqtrd 2919 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → 𝐴 ∈ ((𝑆𝑥)(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥})))))
1424, 10, 11, 24dprdfcl 19057 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ (𝑆𝑥))
143102, 103, 3, 33, 104, 106, 107, 108, 27, 141, 142, 99pj1eq 18748 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (𝐴 = ((𝑓𝑥)(+g𝐺)(𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥})))) ↔ ((((𝑆𝑥)(proj1𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))‘𝐴) = (𝑓𝑥) ∧ (((𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥})))(proj1𝐺)(𝑆𝑥))‘𝐴) = (𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥}))))))
144139, 143mpbid 233 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → ((((𝑆𝑥)(proj1𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))‘𝐴) = (𝑓𝑥) ∧ (((𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥})))(proj1𝐺)(𝑆𝑥))‘𝐴) = (𝐺 Σg (𝑓 ↾ (𝐼 ∖ {𝑥})))))
145144simpld 495 . . . . . . . 8 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → (((𝑆𝑥)(proj1𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑥}))))‘𝐴) = (𝑓𝑥))
14629, 145eqtrd 2860 . . . . . . 7 (((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) ∧ 𝑥𝐼) → ((𝑃𝑥)‘𝐴) = (𝑓𝑥))
147146mpteq2dva 5157 . . . . . 6 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) = (𝑥𝐼 ↦ (𝑓𝑥)))
148119, 147eqtr4d 2863 . . . . 5 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → 𝑓 = (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)))
149148oveq2d 7167 . . . 4 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → (𝐺 Σg 𝑓) = (𝐺 Σg (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴))))
150118, 149eqtrd 2860 . . 3 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → 𝐴 = (𝐺 Σg (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴))))
151117, 150jca 512 . 2 ((𝜑 ∧ (𝑓𝑊𝐴 = (𝐺 Σg 𝑓))) → ((𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) ∈ 𝑊𝐴 = (𝐺 Σg (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)))))
1528, 151rexlimddv 3295 1 (𝜑 → ((𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)) ∈ 𝑊𝐴 = (𝐺 Σg (𝑥𝐼 ↦ ((𝑃𝑥)‘𝐴)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1530   ∈ wcel 2107  ∃wrex 3143  {crab 3146  Vcvv 3499   ∖ cdif 3936   ∪ cun 3937   ∩ cin 3938   ⊆ wss 3939  ∅c0 4294  {csn 4563   class class class wbr 5062   ↦ cmpt 5142  dom cdm 5553  ran crn 5554   ↾ cres 5555  Fun wfun 6345  ⟶wf 6347  ‘cfv 6351  (class class class)co 7151   supp csupp 7824  Xcixp 8453   finSupp cfsupp 8825  Basecbs 16475  +gcplusg 16557  0gc0g 16705   Σg cgsu 16706  Mndcmnd 17902  Grpcgrp 18035  SubGrpcsubg 18205  Cntzccntz 18377  LSSumclsm 18681  proj1cpj1 18682   DProd cdprd 19037  dProjcdpj 19038 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7402  df-om 7572  df-1st 7683  df-2nd 7684  df-supp 7825  df-tpos 7886  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8282  df-map 8401  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-oi 8966  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-n0 11890  df-z 11974  df-uz 12236  df-fz 12886  df-fzo 13027  df-seq 13363  df-hash 13684  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-0g 16707  df-gsum 16708  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17892  df-mnd 17903  df-mhm 17946  df-submnd 17947  df-grp 18038  df-minusg 18039  df-sbg 18040  df-mulg 18157  df-subg 18208  df-ghm 18288  df-gim 18331  df-cntz 18379  df-oppg 18406  df-lsm 18683  df-pj1 18684  df-cmn 18830  df-dprd 19039  df-dpj 19040 This theorem is referenced by:  dpjeq  19103  dpjid  19104
 Copyright terms: Public domain W3C validator