Metamath Proof Explorer


Theorem prodss

Description: Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017)

Ref Expression
Hypotheses prodss.1 φAB
prodss.2 φkAC
prodss.3 φnMyy0seqn×kMifkBC1y
prodss.4 φkBAC=1
prodss.5 φBM
Assertion prodss φkAC=kBC

Proof

Step Hyp Ref Expression
1 prodss.1 φAB
2 prodss.2 φkAC
3 prodss.3 φnMyy0seqn×kMifkBC1y
4 prodss.4 φkBAC=1
5 prodss.5 φBM
6 eqid M=M
7 simpr φMM
8 3 adantr φMnMyy0seqn×kMifkBC1y
9 1 5 sstrd φAM
10 9 adantr φMAM
11 simpr φMmMmM
12 iftrue mBifmBm/kC1=m/kC
13 12 adantl φmBifmBm/kC1=m/kC
14 2 ex φkAC
15 14 adantr φkBkAC
16 eldif kBAkB¬kA
17 ax-1cn 1
18 4 17 eqeltrdi φkBAC
19 16 18 sylan2br φkB¬kAC
20 19 expr φkB¬kAC
21 15 20 pm2.61d φkBC
22 21 ralrimiva φkBC
23 nfcsb1v _km/kC
24 23 nfel1 km/kC
25 csbeq1a k=mC=m/kC
26 25 eleq1d k=mCm/kC
27 24 26 rspc mBkBCm/kC
28 22 27 mpan9 φmBm/kC
29 13 28 eqeltrd φmBifmBm/kC1
30 iffalse ¬mBifmBm/kC1=1
31 30 17 eqeltrdi ¬mBifmBm/kC1
32 31 adantl φ¬mBifmBm/kC1
33 29 32 pm2.61dan φifmBm/kC1
34 33 adantr φMifmBm/kC1
35 34 adantr φMmMifmBm/kC1
36 nfcv _km
37 nfv kmB
38 nfcv _k1
39 37 23 38 nfif _kifmBm/kC1
40 eleq1w k=mkBmB
41 40 25 ifbieq1d k=mifkBC1=ifmBm/kC1
42 eqid kMifkBC1=kMifkBC1
43 36 39 41 42 fvmptf mMifmBm/kC1kMifkBC1m=ifmBm/kC1
44 11 35 43 syl2anc φMmMkMifkBC1m=ifmBm/kC1
45 iftrue mAifmAkACm1=kACm
46 45 adantl φMmAifmAkACm1=kACm
47 simpr φMmAmA
48 1 adantr φMAB
49 48 sselda φMmAmB
50 28 adantlr φMmBm/kC
51 49 50 syldan φMmAm/kC
52 eqid kAC=kAC
53 52 fvmpts mAm/kCkACm=m/kC
54 47 51 53 syl2anc φMmAkACm=m/kC
55 46 54 eqtrd φMmAifmAkACm1=m/kC
56 55 ex φMmAifmAkACm1=m/kC
57 56 adantr φMmBmAifmAkACm1=m/kC
58 iffalse ¬mAifmAkACm1=1
59 58 adantl mB¬mAifmAkACm1=1
60 59 adantl φMmB¬mAifmAkACm1=1
61 eldif mBAmB¬mA
62 4 ralrimiva φkBAC=1
63 62 adantr φMkBAC=1
64 23 nfeq1 km/kC=1
65 25 eqeq1d k=mC=1m/kC=1
66 64 65 rspc mBAkBAC=1m/kC=1
67 63 66 mpan9 φMmBAm/kC=1
68 61 67 sylan2br φMmB¬mAm/kC=1
69 60 68 eqtr4d φMmB¬mAifmAkACm1=m/kC
70 69 expr φMmB¬mAifmAkACm1=m/kC
71 57 70 pm2.61d φMmBifmAkACm1=m/kC
72 12 adantl φMmBifmBm/kC1=m/kC
73 71 72 eqtr4d φMmBifmAkACm1=ifmBm/kC1
74 48 ssneld φM¬mB¬mA
75 74 imp φM¬mB¬mA
76 75 58 syl φM¬mBifmAkACm1=1
77 30 adantl φM¬mBifmBm/kC1=1
78 76 77 eqtr4d φM¬mBifmAkACm1=ifmBm/kC1
79 73 78 pm2.61dan φMifmAkACm1=ifmBm/kC1
80 79 adantr φMmMifmAkACm1=ifmBm/kC1
81 44 80 eqtr4d φMmMkMifkBC1m=ifmAkACm1
82 2 fmpttd φkAC:A
83 82 adantr φMkAC:A
84 83 ffvelrnda φMmAkACm
85 6 7 8 10 81 84 zprod φMmAkACm=seqM×kMifkBC1
86 5 adantr φMBM
87 43 ancoms ifmBm/kC1mMkMifkBC1m=ifmBm/kC1
88 34 87 sylan φMmMkMifkBC1m=ifmBm/kC1
89 simpr φMmBmB
90 eqid kBC=kBC
91 90 fvmpts mBm/kCkBCm=m/kC
92 89 50 91 syl2anc φMmBkBCm=m/kC
93 92 ifeq1d φMmBifmBkBCm1=ifmBm/kC1
94 93 adantlr φMmMmBifmBkBCm1=ifmBm/kC1
95 iffalse ¬mBifmBkBCm1=1
96 95 30 eqtr4d ¬mBifmBkBCm1=ifmBm/kC1
97 96 adantl φMmM¬mBifmBkBCm1=ifmBm/kC1
98 94 97 pm2.61dan φMmMifmBkBCm1=ifmBm/kC1
99 88 98 eqtr4d φMmMkMifkBC1m=ifmBkBCm1
100 21 fmpttd φkBC:B
101 100 adantr φMkBC:B
102 101 ffvelrnda φMmBkBCm
103 6 7 8 86 99 102 zprod φMmBkBCm=seqM×kMifkBC1
104 85 103 eqtr4d φMmAkACm=mBkBCm
105 prodfc mAkACm=kAC
106 prodfc mBkBCm=kBC
107 104 105 106 3eqtr3g φMkAC=kBC
108 1 adantr φ¬MAB
109 5 adantr φ¬MBM
110 uzf :𝒫
111 110 fdmi dom=
112 111 eleq2i MdomM
113 ndmfv ¬MdomM=
114 112 113 sylnbir ¬MM=
115 114 adantl φ¬MM=
116 109 115 sseqtrd φ¬MB
117 108 116 sstrd φ¬MA
118 ss0 AA=
119 117 118 syl φ¬MA=
120 ss0 BB=
121 116 120 syl φ¬MB=
122 119 121 eqtr4d φ¬MA=B
123 122 prodeq1d φ¬MkAC=kBC
124 107 123 pm2.61dan φkAC=kBC