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

Theorem prodeq1f 15858
Description: Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
Hypotheses
Ref Expression
prodeq1f.1 โ„ฒ๐‘˜๐ด
prodeq1f.2 โ„ฒ๐‘˜๐ต
Assertion
Ref Expression
prodeq1f (๐ด = ๐ต โ†’ โˆ๐‘˜ โˆˆ ๐ด ๐ถ = โˆ๐‘˜ โˆˆ ๐ต ๐ถ)

Proof of Theorem prodeq1f
Dummy variables ๐‘“ ๐‘š ๐‘› ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 4002 . . . . . 6 (๐ด = ๐ต โ†’ (๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โ†” ๐ต โІ (โ„คโ‰ฅโ€˜๐‘š)))
2 prodeq1f.1 . . . . . . . . . . . . 13 โ„ฒ๐‘˜๐ด
3 prodeq1f.2 . . . . . . . . . . . . 13 โ„ฒ๐‘˜๐ต
42, 3nfeq 2910 . . . . . . . . . . . 12 โ„ฒ๐‘˜ ๐ด = ๐ต
5 eleq2 2816 . . . . . . . . . . . . . 14 (๐ด = ๐ต โ†’ (๐‘˜ โˆˆ ๐ด โ†” ๐‘˜ โˆˆ ๐ต))
65ifbid 4546 . . . . . . . . . . . . 13 (๐ด = ๐ต โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1) = if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))
76adantr 480 . . . . . . . . . . . 12 ((๐ด = ๐ต โˆง ๐‘˜ โˆˆ โ„ค) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1) = if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))
84, 7mpteq2da 5239 . . . . . . . . . . 11 (๐ด = ๐ต โ†’ (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1)) = (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1)))
98seqeq3d 13980 . . . . . . . . . 10 (๐ด = ๐ต โ†’ seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) = seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))))
109breq1d 5151 . . . . . . . . 9 (๐ด = ๐ต โ†’ (seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ โ†” seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ))
1110anbi2d 628 . . . . . . . 8 (๐ด = ๐ต โ†’ ((๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โ†” (๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ)))
1211exbidv 1916 . . . . . . 7 (๐ด = ๐ต โ†’ (โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โ†” โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ)))
1312rexbidv 3172 . . . . . 6 (๐ด = ๐ต โ†’ (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โ†” โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ)))
148seqeq3d 13980 . . . . . . 7 (๐ด = ๐ต โ†’ seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) = seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))))
1514breq1d 5151 . . . . . 6 (๐ด = ๐ต โ†’ (seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ โ†” seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ))
161, 13, 153anbi123d 1432 . . . . 5 (๐ด = ๐ต โ†’ ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ) โ†” (๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ)))
1716rexbidv 3172 . . . 4 (๐ด = ๐ต โ†’ (โˆƒ๐‘š โˆˆ โ„ค (๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ) โ†” โˆƒ๐‘š โˆˆ โ„ค (๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ)))
18 f1oeq3 6817 . . . . . . 7 (๐ด = ๐ต โ†’ (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โ†” ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต))
1918anbi1d 629 . . . . . 6 (๐ด = ๐ต โ†’ ((๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š)) โ†” (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š))))
2019exbidv 1916 . . . . 5 (๐ด = ๐ต โ†’ (โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š)) โ†” โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š))))
2120rexbidv 3172 . . . 4 (๐ด = ๐ต โ†’ (โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š)) โ†” โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š))))
2217, 21orbi12d 915 . . 3 (๐ด = ๐ต โ†’ ((โˆƒ๐‘š โˆˆ โ„ค (๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š))) โ†” (โˆƒ๐‘š โˆˆ โ„ค (๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š)))))
2322iotabidv 6521 . 2 (๐ด = ๐ต โ†’ (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค (๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š)))) = (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค (๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š)))))
24 df-prod 15856 . 2 โˆ๐‘˜ โˆˆ ๐ด ๐ถ = (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค (๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š))))
25 df-prod 15856 . 2 โˆ๐‘˜ โˆˆ ๐ต ๐ถ = (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค (๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š))))
2623, 24, 253eqtr4g 2791 1 (๐ด = ๐ต โ†’ โˆ๐‘˜ โˆˆ ๐ด ๐ถ = โˆ๐‘˜ โˆˆ ๐ต ๐ถ)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆจ wo 844   โˆง w3a 1084   = wceq 1533  โˆƒwex 1773   โˆˆ wcel 2098  โ„ฒwnfc 2877   โ‰  wne 2934  โˆƒwrex 3064  โฆ‹csb 3888   โІ wss 3943  ifcif 4523   class class class wbr 5141   โ†ฆ cmpt 5224  โ„ฉcio 6487  โ€“1-1-ontoโ†’wf1o 6536  โ€˜cfv 6537  (class class class)co 7405  0cc0 11112  1c1 11113   ยท cmul 11117  โ„•cn 12216  โ„คcz 12562  โ„คโ‰ฅcuz 12826  ...cfz 13490  seqcseq 13972   โ‡ cli 15434  โˆcprod 15855
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-mpt 5225  df-xp 5675  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-iota 6489  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7408  df-oprab 7409  df-mpo 7410  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-seq 13973  df-prod 15856
This theorem is referenced by:  prodeq1  15859
  Copyright terms: Public domain W3C validator