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 )