Theorem suppssof1

Description: Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 28-May-2019)

	Ref	Expression
Hypotheses	suppssof1.s	|- ( ph -> ( A supp Y ) C_ L )
	suppssof1.o	|- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )
	suppssof1.a	|- ( ph -> A : D --> V )
	suppssof1.b	|- ( ph -> B : D --> R )
	suppssof1.d	|- ( ph -> D e. W )
	suppssof1.y	|- ( ph -> Y e. U )
Assertion	suppssof1	|- ( ph -> ( ( A oF O B ) supp Z ) C_ L )

Proof

Step	Hyp	Ref	Expression
1		suppssof1.s	|- ( ph -> ( A supp Y ) C_ L )
2		suppssof1.o	|- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )
3		suppssof1.a	|- ( ph -> A : D --> V )
4		suppssof1.b	|- ( ph -> B : D --> R )
5		suppssof1.d	|- ( ph -> D e. W )
6		suppssof1.y	|- ( ph -> Y e. U )
7	3	ffnd	|- ( ph -> A Fn D )
8	4	ffnd	|- ( ph -> B Fn D )
9		inidm	|- ( D i^i D ) = D
10		eqidd	|- ( ( ph /\ x e. D ) -> ( A ` x ) = ( A ` x ) )
11		eqidd	|- ( ( ph /\ x e. D ) -> ( B ` x ) = ( B ` x ) )
12	7 8 5 5 9 10 11	offval	|- ( ph -> ( A oF O B ) = ( x e. D |-> ( ( A ` x ) O ( B ` x ) ) ) )
13	12	oveq1d	|- ( ph -> ( ( A oF O B ) supp Z ) = ( ( x e. D |-> ( ( A ` x ) O ( B ` x ) ) ) supp Z ) )
14	3	feqmptd	|- ( ph -> A = ( x e. D |-> ( A ` x ) ) )
15	14	oveq1d	|- ( ph -> ( A supp Y ) = ( ( x e. D |-> ( A ` x ) ) supp Y ) )
16	15 1	eqsstrrd	|- ( ph -> ( ( x e. D |-> ( A ` x ) ) supp Y ) C_ L )
17		fvexd	|- ( ( ph /\ x e. D ) -> ( A ` x ) e. _V )
18	4	ffvelrnda	|- ( ( ph /\ x e. D ) -> ( B ` x ) e. R )
19	16 2 17 18 6	suppssov1	|- ( ph -> ( ( x e. D |-> ( ( A ` x ) O ( B ` x ) ) ) supp Z ) C_ L )
20	13 19	eqsstrd	|- ( ph -> ( ( A oF O B ) supp Z ) C_ L )