Metamath Proof Explorer


Theorem dprdfeq0

Description: The zero function is the only function that sums to zero in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses eldprdi.0 0 ˙ = 0 G
eldprdi.w W = h i I S i | finSupp 0 ˙ h
eldprdi.1 φ G dom DProd S
eldprdi.2 φ dom S = I
eldprdi.3 φ F W
Assertion dprdfeq0 φ G F = 0 ˙ F = x I 0 ˙

Proof

Step Hyp Ref Expression
1 eldprdi.0 0 ˙ = 0 G
2 eldprdi.w W = h i I S i | finSupp 0 ˙ h
3 eldprdi.1 φ G dom DProd S
4 eldprdi.2 φ dom S = I
5 eldprdi.3 φ F W
6 eqid Base G = Base G
7 2 3 4 5 6 dprdff φ F : I Base G
8 7 feqmptd φ F = x I F x
9 8 adantr φ G F = 0 ˙ F = x I F x
10 2 3 4 5 dprdfcl φ x I F x S x
11 10 adantlr φ G F = 0 ˙ x I F x S x
12 3 ad2antrr φ G F = 0 ˙ x I G dom DProd S
13 4 ad2antrr φ G F = 0 ˙ x I dom S = I
14 simpr φ G F = 0 ˙ x I x I
15 eqid y I if y = x F x 0 ˙ = y I if y = x F x 0 ˙
16 1 2 12 13 14 11 15 dprdfid φ G F = 0 ˙ x I y I if y = x F x 0 ˙ W G y I if y = x F x 0 ˙ = F x
17 16 simpld φ G F = 0 ˙ x I y I if y = x F x 0 ˙ W
18 5 ad2antrr φ G F = 0 ˙ x I F W
19 eqid - G = - G
20 1 2 12 13 17 18 19 dprdfsub φ G F = 0 ˙ x I y I if y = x F x 0 ˙ - G f F W G y I if y = x F x 0 ˙ - G f F = G y I if y = x F x 0 ˙ - G G F
21 20 simprd φ G F = 0 ˙ x I G y I if y = x F x 0 ˙ - G f F = G y I if y = x F x 0 ˙ - G G F
22 3 4 dprddomcld φ I V
23 22 ad2antrr φ G F = 0 ˙ x I I V
24 fvex F x V
25 1 fvexi 0 ˙ V
26 24 25 ifex if y = x F x 0 ˙ V
27 26 a1i φ G F = 0 ˙ x I y I if y = x F x 0 ˙ V
28 fvexd φ G F = 0 ˙ x I y I F y V
29 eqidd φ G F = 0 ˙ x I y I if y = x F x 0 ˙ = y I if y = x F x 0 ˙
30 7 ad2antrr φ G F = 0 ˙ x I F : I Base G
31 30 feqmptd φ G F = 0 ˙ x I F = y I F y
32 23 27 28 29 31 offval2 φ G F = 0 ˙ x I y I if y = x F x 0 ˙ - G f F = y I if y = x F x 0 ˙ - G F y
33 32 oveq2d φ G F = 0 ˙ x I G y I if y = x F x 0 ˙ - G f F = G y I if y = x F x 0 ˙ - G F y
34 16 simprd φ G F = 0 ˙ x I G y I if y = x F x 0 ˙ = F x
35 simplr φ G F = 0 ˙ x I G F = 0 ˙
36 34 35 oveq12d φ G F = 0 ˙ x I G y I if y = x F x 0 ˙ - G G F = F x - G 0 ˙
37 dprdgrp G dom DProd S G Grp
38 12 37 syl φ G F = 0 ˙ x I G Grp
39 30 14 ffvelrnd φ G F = 0 ˙ x I F x Base G
40 6 1 19 grpsubid1 G Grp F x Base G F x - G 0 ˙ = F x
41 38 39 40 syl2anc φ G F = 0 ˙ x I F x - G 0 ˙ = F x
42 36 41 eqtrd φ G F = 0 ˙ x I G y I if y = x F x 0 ˙ - G G F = F x
43 21 33 42 3eqtr3d φ G F = 0 ˙ x I G y I if y = x F x 0 ˙ - G F y = F x
44 eqid Cntz G = Cntz G
45 grpmnd G Grp G Mnd
46 3 37 45 3syl φ G Mnd
47 46 ad2antrr φ G F = 0 ˙ x I G Mnd
48 6 subgacs G Grp SubGrp G ACS Base G
49 acsmre SubGrp G ACS Base G SubGrp G Moore Base G
50 38 48 49 3syl φ G F = 0 ˙ x I SubGrp G Moore Base G
51 imassrn S I x ran S
52 3 4 dprdf2 φ S : I SubGrp G
53 52 ad2antrr φ G F = 0 ˙ x I S : I SubGrp G
54 53 frnd φ G F = 0 ˙ x I ran S SubGrp G
55 mresspw SubGrp G Moore Base G SubGrp G 𝒫 Base G
56 50 55 syl φ G F = 0 ˙ x I SubGrp G 𝒫 Base G
57 54 56 sstrd φ G F = 0 ˙ x I ran S 𝒫 Base G
58 51 57 sstrid φ G F = 0 ˙ x I S I x 𝒫 Base G
59 sspwuni S I x 𝒫 Base G S I x Base G
60 58 59 sylib φ G F = 0 ˙ x I S I x Base G
61 eqid mrCls SubGrp G = mrCls SubGrp G
62 61 mrccl SubGrp G Moore Base G S I x Base G mrCls SubGrp G S I x SubGrp G
63 50 60 62 syl2anc φ G F = 0 ˙ x I mrCls SubGrp G S I x SubGrp G
64 subgsubm mrCls SubGrp G S I x SubGrp G mrCls SubGrp G S I x SubMnd G
65 63 64 syl φ G F = 0 ˙ x I mrCls SubGrp G S I x SubMnd G
66 oveq1 F x = if y = x F x 0 ˙ F x - G F y = if y = x F x 0 ˙ - G F y
67 66 eleq1d F x = if y = x F x 0 ˙ F x - G F y mrCls SubGrp G S I x if y = x F x 0 ˙ - G F y mrCls SubGrp G S I x
68 oveq1 0 ˙ = if y = x F x 0 ˙ 0 ˙ - G F y = if y = x F x 0 ˙ - G F y
69 68 eleq1d 0 ˙ = if y = x F x 0 ˙ 0 ˙ - G F y mrCls SubGrp G S I x if y = x F x 0 ˙ - G F y mrCls SubGrp G S I x
70 simpr φ G F = 0 ˙ x I y I y = x y = x
71 70 fveq2d φ G F = 0 ˙ x I y I y = x F y = F x
72 71 oveq2d φ G F = 0 ˙ x I y I y = x F x - G F y = F x - G F x
73 6 1 19 grpsubid G Grp F x Base G F x - G F x = 0 ˙
74 38 39 73 syl2anc φ G F = 0 ˙ x I F x - G F x = 0 ˙
75 1 subg0cl mrCls SubGrp G S I x SubGrp G 0 ˙ mrCls SubGrp G S I x
76 63 75 syl φ G F = 0 ˙ x I 0 ˙ mrCls SubGrp G S I x
77 74 76 eqeltrd φ G F = 0 ˙ x I F x - G F x mrCls SubGrp G S I x
78 77 ad2antrr φ G F = 0 ˙ x I y I y = x F x - G F x mrCls SubGrp G S I x
79 72 78 eqeltrd φ G F = 0 ˙ x I y I y = x F x - G F y mrCls SubGrp G S I x
80 63 ad2antrr φ G F = 0 ˙ x I y I ¬ y = x mrCls SubGrp G S I x SubGrp G
81 80 75 syl φ G F = 0 ˙ x I y I ¬ y = x 0 ˙ mrCls SubGrp G S I x
82 50 61 60 mrcssidd φ G F = 0 ˙ x I S I x mrCls SubGrp G S I x
83 82 ad2antrr φ G F = 0 ˙ x I y I ¬ y = x S I x mrCls SubGrp G S I x
84 2 12 13 18 dprdfcl φ G F = 0 ˙ x I y I F y S y
85 84 adantr φ G F = 0 ˙ x I y I ¬ y = x F y S y
86 53 ffnd φ G F = 0 ˙ x I S Fn I
87 86 ad2antrr φ G F = 0 ˙ x I y I ¬ y = x S Fn I
88 difssd φ G F = 0 ˙ x I y I ¬ y = x I x I
89 df-ne y x ¬ y = x
90 eldifsn y I x y I y x
91 90 biimpri y I y x y I x
92 89 91 sylan2br y I ¬ y = x y I x
93 92 adantll φ G F = 0 ˙ x I y I ¬ y = x y I x
94 fnfvima S Fn I I x I y I x S y S I x
95 87 88 93 94 syl3anc φ G F = 0 ˙ x I y I ¬ y = x S y S I x
96 elunii F y S y S y S I x F y S I x
97 85 95 96 syl2anc φ G F = 0 ˙ x I y I ¬ y = x F y S I x
98 83 97 sseldd φ G F = 0 ˙ x I y I ¬ y = x F y mrCls SubGrp G S I x
99 19 subgsubcl mrCls SubGrp G S I x SubGrp G 0 ˙ mrCls SubGrp G S I x F y mrCls SubGrp G S I x 0 ˙ - G F y mrCls SubGrp G S I x
100 80 81 98 99 syl3anc φ G F = 0 ˙ x I y I ¬ y = x 0 ˙ - G F y mrCls SubGrp G S I x
101 67 69 79 100 ifbothda φ G F = 0 ˙ x I y I if y = x F x 0 ˙ - G F y mrCls SubGrp G S I x
102 101 fmpttd φ G F = 0 ˙ x I y I if y = x F x 0 ˙ - G F y : I mrCls SubGrp G S I x
103 20 simpld φ G F = 0 ˙ x I y I if y = x F x 0 ˙ - G f F W
104 32 103 eqeltrrd φ G F = 0 ˙ x I y I if y = x F x 0 ˙ - G F y W
105 2 12 13 104 44 dprdfcntz φ G F = 0 ˙ x I ran y I if y = x F x 0 ˙ - G F y Cntz G ran y I if y = x F x 0 ˙ - G F y
106 2 12 13 104 dprdffsupp φ G F = 0 ˙ x I finSupp 0 ˙ y I if y = x F x 0 ˙ - G F y
107 1 44 47 23 65 102 105 106 gsumzsubmcl φ G F = 0 ˙ x I G y I if y = x F x 0 ˙ - G F y mrCls SubGrp G S I x
108 43 107 eqeltrrd φ G F = 0 ˙ x I F x mrCls SubGrp G S I x
109 11 108 elind φ G F = 0 ˙ x I F x S x mrCls SubGrp G S I x
110 12 13 14 1 61 dprddisj φ G F = 0 ˙ x I S x mrCls SubGrp G S I x = 0 ˙
111 109 110 eleqtrd φ G F = 0 ˙ x I F x 0 ˙
112 elsni F x 0 ˙ F x = 0 ˙
113 111 112 syl φ G F = 0 ˙ x I F x = 0 ˙
114 113 mpteq2dva φ G F = 0 ˙ x I F x = x I 0 ˙
115 9 114 eqtrd φ G F = 0 ˙ F = x I 0 ˙
116 115 ex φ G F = 0 ˙ F = x I 0 ˙
117 1 gsumz G Mnd I V G x I 0 ˙ = 0 ˙
118 46 22 117 syl2anc φ G x I 0 ˙ = 0 ˙
119 oveq2 F = x I 0 ˙ G F = G x I 0 ˙
120 119 eqeq1d F = x I 0 ˙ G F = 0 ˙ G x I 0 ˙ = 0 ˙
121 118 120 syl5ibrcom φ F = x I 0 ˙ G F = 0 ˙
122 116 121 impbid φ G F = 0 ˙ F = x I 0 ˙