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

Proof

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

Metamath Proof Explorer

Theorem suppssof1

Proof