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	$$⊢\phi \to A\mathrm{supp}Y\subseteq L$$
	suppssof1.o	$$⊢\left(\phi \wedge v\in R\right)\to YOv=Z$$
	suppssof1.a	$$⊢\phi \to A:D⟶V$$
	suppssof1.b	$$⊢\phi \to B:D⟶R$$
	suppssof1.d	$$⊢\phi \to D\in W$$
	suppssof1.y	$$⊢\phi \to Y\in U$$
Assertion	suppssof1	$$⊢\phi \to \left(A{O}_{f}B\right)\mathrm{supp}Z\subseteq L$$

Proof

Step	Hyp	Ref	Expression
1		suppssof1.s	$$⊢\phi \to A\mathrm{supp}Y\subseteq L$$
2		suppssof1.o	$$⊢\left(\phi \wedge v\in R\right)\to YOv=Z$$
3		suppssof1.a	$$⊢\phi \to A:D⟶V$$
4		suppssof1.b	$$⊢\phi \to B:D⟶R$$
5		suppssof1.d	$$⊢\phi \to D\in W$$
6		suppssof1.y	$$⊢\phi \to Y\in U$$
7	3	ffnd	$$⊢\phi \to AFnD$$
8	4	ffnd	$$⊢\phi \to BFnD$$
9		inidm	$$⊢D\cap D=D$$
10		eqidd	$$⊢\left(\phi \wedge x\in D\right)\to A\left(x\right)=A\left(x\right)$$
11		eqidd	$$⊢\left(\phi \wedge x\in D\right)\to B\left(x\right)=B\left(x\right)$$
12	7 8 5 5 9 10 11	offval	$$⊢\phi \to A{O}_{f}B=\left(x\in D⟼A\left(x\right)OB\left(x\right)\right)$$
13	12	oveq1d	$$⊢\phi \to \left(A{O}_{f}B\right)\mathrm{supp}Z=\left(x\in D⟼A\left(x\right)OB\left(x\right)\right)\mathrm{supp}Z$$
14	3	feqmptd	$$⊢\phi \to A=\left(x\in D⟼A\left(x\right)\right)$$
15	14	oveq1d	$$⊢\phi \to A\mathrm{supp}Y=\left(x\in D⟼A\left(x\right)\right)\mathrm{supp}Y$$
16	15 1	eqsstrrd	$$⊢\phi \to \left(x\in D⟼A\left(x\right)\right)\mathrm{supp}Y\subseteq L$$
17		fvexd	$$⊢\left(\phi \wedge x\in D\right)\to A\left(x\right)\in \mathrm{V}$$
18	4	ffvelcdmda	$$⊢\left(\phi \wedge x\in D\right)\to B\left(x\right)\in R$$
19	16 2 17 18 6	suppssov1	$$⊢\phi \to \left(x\in D⟼A\left(x\right)OB\left(x\right)\right)\mathrm{supp}Z\subseteq L$$
20	13 19	eqsstrd	$$⊢\phi \to \left(A{O}_{f}B\right)\mathrm{supp}Z\subseteq L$$