Metamath Proof Explorer

Theorem stoweidlem8

Description: Lemma for stoweid : two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem8.1 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem8.2 
|- F/_ t F
stoweidlem8.3 
|- F/_ t G
Assertion stoweidlem8 
|- ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) + ( G ` t ) ) ) e. A )

Proof

Step Hyp Ref Expression
1 stoweidlem8.1 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
2 stoweidlem8.2 
 |-  F/_ t F
3 stoweidlem8.3 
 |-  F/_ t G
4 simp3 
 |-  ( ( ph /\ F e. A /\ G e. A ) -> G e. A )
5 eleq1 
 |-  ( g = G -> ( g e. A <-> G e. A ) )
6 5 3anbi3d 
 |-  ( g = G -> ( ( ph /\ F e. A /\ g e. A ) <-> ( ph /\ F e. A /\ G e. A ) ) )
7 3 nfeq2 
 |-  F/ t g = G
8 fveq1 
 |-  ( g = G -> ( g ` t ) = ( G ` t ) )
9 8 oveq2d 
 |-  ( g = G -> ( ( F ` t ) + ( g ` t ) ) = ( ( F ` t ) + ( G ` t ) ) )
10 9 adantr 
 |-  ( ( g = G /\ t e. T ) -> ( ( F ` t ) + ( g ` t ) ) = ( ( F ` t ) + ( G ` t ) ) )
11 7 10 mpteq2da 
 |-  ( g = G -> ( t e. T |-> ( ( F ` t ) + ( g ` t ) ) ) = ( t e. T |-> ( ( F ` t ) + ( G ` t ) ) ) )
12 11 eleq1d 
 |-  ( g = G -> ( ( t e. T |-> ( ( F ` t ) + ( g ` t ) ) ) e. A <-> ( t e. T |-> ( ( F ` t ) + ( G ` t ) ) ) e. A ) )
13 6 12 imbi12d 
 |-  ( g = G -> ( ( ( ph /\ F e. A /\ g e. A ) -> ( t e. T |-> ( ( F ` t ) + ( g ` t ) ) ) e. A ) <-> ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) + ( G ` t ) ) ) e. A ) ) )
14 simp2 
 |-  ( ( ph /\ F e. A /\ g e. A ) -> F e. A )
15 eleq1 
 |-  ( f = F -> ( f e. A <-> F e. A ) )
16 15 3anbi2d 
 |-  ( f = F -> ( ( ph /\ f e. A /\ g e. A ) <-> ( ph /\ F e. A /\ g e. A ) ) )
17 2 nfeq2 
 |-  F/ t f = F
18 fveq1 
 |-  ( f = F -> ( f ` t ) = ( F ` t ) )
19 18 oveq1d 
 |-  ( f = F -> ( ( f ` t ) + ( g ` t ) ) = ( ( F ` t ) + ( g ` t ) ) )
20 19 adantr 
 |-  ( ( f = F /\ t e. T ) -> ( ( f ` t ) + ( g ` t ) ) = ( ( F ` t ) + ( g ` t ) ) )
21 17 20 mpteq2da 
 |-  ( f = F -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) = ( t e. T |-> ( ( F ` t ) + ( g ` t ) ) ) )
22 21 eleq1d 
 |-  ( f = F -> ( ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A <-> ( t e. T |-> ( ( F ` t ) + ( g ` t ) ) ) e. A ) )
23 16 22 imbi12d 
 |-  ( f = F -> ( ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A ) <-> ( ( ph /\ F e. A /\ g e. A ) -> ( t e. T |-> ( ( F ` t ) + ( g ` t ) ) ) e. A ) ) )
24 23 1 vtoclg 
 |-  ( F e. A -> ( ( ph /\ F e. A /\ g e. A ) -> ( t e. T |-> ( ( F ` t ) + ( g ` t ) ) ) e. A ) )
25 14 24 mpcom 
 |-  ( ( ph /\ F e. A /\ g e. A ) -> ( t e. T |-> ( ( F ` t ) + ( g ` t ) ) ) e. A )
26 13 25 vtoclg 
 |-  ( G e. A -> ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) + ( G ` t ) ) ) e. A ) )
27 4 26 mpcom 
 |-  ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) + ( G ` t ) ) ) e. A )