Theorem stoweidlem33

Description: If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem33.1	|- F/_ t F
	stoweidlem33.2	|- F/_ t G
	stoweidlem33.3	|- F/ t ph
	stoweidlem33.4	|- ( ( ph /\ f e. A ) -> f : T --> RR )
	stoweidlem33.5	|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
	stoweidlem33.6	|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
	stoweidlem33.7	|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
Assertion	stoweidlem33	|- ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) ) e. A )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem33.1	|- F/_ t F
2		stoweidlem33.2	|- F/_ t G
3		stoweidlem33.3	|- F/ t ph
4		stoweidlem33.4	|- ( ( ph /\ f e. A ) -> f : T --> RR )
5		stoweidlem33.5	|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
6		stoweidlem33.6	|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
7		stoweidlem33.7	|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
8		eqid	|- ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) ) = ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) )
9		eqid	|- ( t e. T |-> -u 1 ) = ( t e. T |-> -u 1 )
10		eqid	|- ( t e. T |-> ( ( ( t e. T |-> -u 1 ) ` t ) x. ( G ` t ) ) ) = ( t e. T |-> ( ( ( t e. T |-> -u 1 ) ` t ) x. ( G ` t ) ) )
11	3 1 2 8 9 10 4 5 6 7	stoweidlem22	|- ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) ) e. A )