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	ffvelcdmda	\|- ( ( 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 )

Metamath Proof Explorer

Theorem suppssof1

Proof