Theorem itg1add

Description: The integral of a sum of simple functions is the sum of the integrals. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Hypotheses	i1fadd.1	|- ( ph -> F e. dom S.1 )
	i1fadd.2	|- ( ph -> G e. dom S.1 )
Assertion	itg1add	|- ( ph -> ( S.1 ` ( F oF + G ) ) = ( ( S.1 ` F ) + ( S.1 ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		i1fadd.1	|- ( ph -> F e. dom S.1 )
2		i1fadd.2	|- ( ph -> G e. dom S.1 )
3		eqid	|- ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) ) = ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) )
4		eqid	|- ( + |` ( ran F X. ran G ) ) = ( + |` ( ran F X. ran G ) )
5	1 2 3 4	itg1addlem5	|- ( ph -> ( S.1 ` ( F oF + G ) ) = ( ( S.1 ` F ) + ( S.1 ` G ) ) )