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

Theorem prodeq1f 15894
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 4007 . . . . . 6 (๐ด = ๐ต โ†’ (๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โ†” ๐ต โІ (โ„คโ‰ฅโ€˜๐‘š)))
2 prodeq1f.1 . . . . . . . . . . . . 13 โ„ฒ๐‘˜๐ด
3 prodeq1f.2 . . . . . . . . . . . . 13 โ„ฒ๐‘˜๐ต
42, 3nfeq 2913 . . . . . . . . . . . 12 โ„ฒ๐‘˜ ๐ด = ๐ต
5 eleq2 2818 . . . . . . . . . . . . . 14 (๐ด = ๐ต โ†’ (๐‘˜ โˆˆ ๐ด โ†” ๐‘˜ โˆˆ ๐ต))
65ifbid 4555 . . . . . . . . . . . . 13 (๐ด = ๐ต โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1) = if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))
76adantr 479 . . . . . . . . . . . 12 ((๐ด = ๐ต โˆง ๐‘˜ โˆˆ โ„ค) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1) = if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))
84, 7mpteq2da 5250 . . . . . . . . . . 11 (๐ด = ๐ต โ†’ (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1)) = (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1)))
98seqeq3d 14016 . . . . . . . . . 10 (๐ด = ๐ต โ†’ seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) = seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))))
109breq1d 5162 . . . . . . . . 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 3176 . . . . . 6 (๐ด = ๐ต โ†’ (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โ†” โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ)))
148seqeq3d 14016 . . . . . . 7 (๐ด = ๐ต โ†’ seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) = seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))))
1514breq1d 5162 . . . . . 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 3176 . . . 4 (๐ด = ๐ต โ†’ (โˆƒ๐‘š โˆˆ โ„ค (๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ) โ†” โˆƒ๐‘š โˆˆ โ„ค (๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ)))
18 f1oeq3 6834 . . . . . . 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 3176 . . . 4 (๐ด = ๐ต โ†’ (โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š)) โ†” โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š))))
2217, 21orbi12d 916 . . 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 6537 . 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 15892 . 2 โˆ๐‘˜ โˆˆ ๐ด ๐ถ = (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค (๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š))))
25 df-prod 15892 . 2 โˆ๐‘˜ โˆˆ ๐ต ๐ถ = (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค (๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ))โ€˜๐‘š))))
2623, 24, 253eqtr4g 2793 1 (๐ด = ๐ต โ†’ โˆ๐‘˜ โˆˆ ๐ด ๐ถ = โˆ๐‘˜ โˆˆ ๐ต ๐ถ)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 394   โˆจ wo 845   โˆง w3a 1084   = wceq 1533  โˆƒwex 1773   โˆˆ wcel 2098  โ„ฒwnfc 2879   โ‰  wne 2937  โˆƒwrex 3067  โฆ‹csb 3894   โІ wss 3949  ifcif 4532   class class class wbr 5152   โ†ฆ cmpt 5235  โ„ฉcio 6503  โ€“1-1-ontoโ†’wf1o 6552  โ€˜cfv 6553  (class class class)co 7426  0cc0 11148  1c1 11149   ยท cmul 11153  โ„•cn 12252  โ„คcz 12598  โ„คโ‰ฅcuz 12862  ...cfz 13526  seqcseq 14008   โ‡ cli 15470  โˆcprod 15891
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 2166  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-xp 5688  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-iota 6505  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-seq 14009  df-prod 15892
This theorem is referenced by:  prodeq1  15895
  Copyright terms: Public domain W3C validator