Metamath Proof Explorer

Theorem stoweidlem6

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

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

Proof

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