Metamath Proof Explorer

Theorem 3factsumint

Description: Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024)

Ref Expression
Hypotheses 3factsumint.1 
|- A = ( L [,] U )
3factsumint.2 
|- ( ph -> B e. Fin )
3factsumint.3 
|- ( ph -> L e. RR )
3factsumint.4 
|- ( ph -> U e. RR )
3factsumint.5 
|- ( ph -> ( x e. A |-> F ) e. ( A -cn-> CC ) )
3factsumint.6 
|- ( ( ph /\ k e. B ) -> G e. CC )
3factsumint.7 
|- ( ( ph /\ k e. B ) -> ( x e. A |-> H ) e. ( A -cn-> CC ) )
Assertion 3factsumint 
|- ( ph -> S. A ( F x. sum_ k e. B ( G x. H ) ) _d x = sum_ k e. B ( G x. S. A ( F x. H ) _d x ) )

Proof

Step Hyp Ref Expression
1 3factsumint.1 
 |-  A = ( L [,] U )
2 3factsumint.2 
 |-  ( ph -> B e. Fin )
3 3factsumint.3 
 |-  ( ph -> L e. RR )
4 3factsumint.4 
 |-  ( ph -> U e. RR )
5 3factsumint.5 
 |-  ( ph -> ( x e. A |-> F ) e. ( A -cn-> CC ) )
6 3factsumint.6 
 |-  ( ( ph /\ k e. B ) -> G e. CC )
7 3factsumint.7 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> H ) e. ( A -cn-> CC ) )
8 cncff 
 |-  ( ( x e. A |-> F ) e. ( A -cn-> CC ) -> ( x e. A |-> F ) : A --> CC )
9 5 8 syl 
 |-  ( ph -> ( x e. A |-> F ) : A --> CC )
10 eqid 
 |-  ( x e. A |-> F ) = ( x e. A |-> F )
11 10 fmpt 
 |-  ( A. x e. A F e. CC <-> ( x e. A |-> F ) : A --> CC )
12 9 11 sylibr 
 |-  ( ph -> A. x e. A F e. CC )
13 12 r19.21bi 
 |-  ( ( ph /\ x e. A ) -> F e. CC )
14 cncff 
 |-  ( ( x e. A |-> H ) e. ( A -cn-> CC ) -> ( x e. A |-> H ) : A --> CC )
15 7 14 syl 
 |-  ( ( ph /\ k e. B ) -> ( x e. A |-> H ) : A --> CC )
16 eqid 
 |-  ( x e. A |-> H ) = ( x e. A |-> H )
17 16 fmpt 
 |-  ( A. x e. A H e. CC <-> ( x e. A |-> H ) : A --> CC )
18 15 17 sylibr 
 |-  ( ( ph /\ k e. B ) -> A. x e. A H e. CC )
19 18 r19.21bi 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) -> H e. CC )
20 anass 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) <-> ( ph /\ ( k e. B /\ x e. A ) ) )
21 ancom 
 |-  ( ( k e. B /\ x e. A ) <-> ( x e. A /\ k e. B ) )
22 21 anbi2i 
 |-  ( ( ph /\ ( k e. B /\ x e. A ) ) <-> ( ph /\ ( x e. A /\ k e. B ) ) )
23 20 22 bitri 
 |-  ( ( ( ph /\ k e. B ) /\ x e. A ) <-> ( ph /\ ( x e. A /\ k e. B ) ) )
24 23 imbi1i 
 |-  ( ( ( ( ph /\ k e. B ) /\ x e. A ) -> H e. CC ) <-> ( ( ph /\ ( x e. A /\ k e. B ) ) -> H e. CC ) )
25 19 24 mpbi 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> H e. CC )
26 2 13 6 25 3factsumint4 
 |-  ( ph -> S. A sum_ k e. B ( F x. ( G x. H ) ) _d x = S. A ( F x. sum_ k e. B ( G x. H ) ) _d x )
27 1 2 3 4 13 5 6 25 7 3factsumint1 
 |-  ( ph -> S. A sum_ k e. B ( F x. ( G x. H ) ) _d x = sum_ k e. B S. A ( F x. ( G x. H ) ) _d x )
28 26 27 eqtr3d 
 |-  ( ph -> S. A ( F x. sum_ k e. B ( G x. H ) ) _d x = sum_ k e. B S. A ( F x. ( G x. H ) ) _d x )
29 13 6 25 3factsumint2 
 |-  ( ph -> sum_ k e. B S. A ( F x. ( G x. H ) ) _d x = sum_ k e. B S. A ( G x. ( F x. H ) ) _d x )
30 1 3 4 13 5 6 25 7 3factsumint3 
 |-  ( ph -> sum_ k e. B S. A ( G x. ( F x. H ) ) _d x = sum_ k e. B ( G x. S. A ( F x. H ) _d x ) )
31 28 29 30 3eqtrd 
 |-  ( ph -> S. A ( F x. sum_ k e. B ( G x. H ) ) _d x = sum_ k e. B ( G x. S. A ( F x. H ) _d x ) )