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	⊢ ( 𝜑 → ( 𝐴 supp 𝑌 ) ⊆ 𝐿 )
	suppssof1.o	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑅 ) → ( 𝑌 𝑂 𝑣 ) = 𝑍 )
	suppssof1.a	⊢ ( 𝜑 → 𝐴 : 𝐷 ⟶ 𝑉 )
	suppssof1.b	⊢ ( 𝜑 → 𝐵 : 𝐷 ⟶ 𝑅 )
	suppssof1.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
	suppssof1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Assertion	suppssof1	⊢ ( 𝜑 → ( ( 𝐴 ∘_f 𝑂 𝐵 ) supp 𝑍 ) ⊆ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		suppssof1.s	⊢ ( 𝜑 → ( 𝐴 supp 𝑌 ) ⊆ 𝐿 )
2		suppssof1.o	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑅 ) → ( 𝑌 𝑂 𝑣 ) = 𝑍 )
3		suppssof1.a	⊢ ( 𝜑 → 𝐴 : 𝐷 ⟶ 𝑉 )
4		suppssof1.b	⊢ ( 𝜑 → 𝐵 : 𝐷 ⟶ 𝑅 )
5		suppssof1.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
6		suppssof1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
7	3	ffnd	⊢ ( 𝜑 → 𝐴 Fn 𝐷 )
8	4	ffnd	⊢ ( 𝜑 → 𝐵 Fn 𝐷 )
9		inidm	⊢ ( 𝐷 ∩ 𝐷 ) = 𝐷
10		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
11		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
12	7 8 5 5 9 10 11	offval	⊢ ( 𝜑 → ( 𝐴 ∘_f 𝑂 𝐵 ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐴 ‘ 𝑥 ) 𝑂 ( 𝐵 ‘ 𝑥 ) ) ) )
13	12	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 ∘_f 𝑂 𝐵 ) supp 𝑍 ) = ( ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐴 ‘ 𝑥 ) 𝑂 ( 𝐵 ‘ 𝑥 ) ) ) supp 𝑍 ) )
14	3	feqmptd	⊢ ( 𝜑 → 𝐴 = ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 ‘ 𝑥 ) ) )
15	14	oveq1d	⊢ ( 𝜑 → ( 𝐴 supp 𝑌 ) = ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 ‘ 𝑥 ) ) supp 𝑌 ) )
16	15 1	eqsstrrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 ‘ 𝑥 ) ) supp 𝑌 ) ⊆ 𝐿 )
17		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 ‘ 𝑥 ) ∈ V )
18	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 )
19	16 2 17 18 6	suppssov1	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐴 ‘ 𝑥 ) 𝑂 ( 𝐵 ‘ 𝑥 ) ) ) supp 𝑍 ) ⊆ 𝐿 )
20	13 19	eqsstrd	⊢ ( 𝜑 → ( ( 𝐴 ∘_f 𝑂 𝐵 ) supp 𝑍 ) ⊆ 𝐿 )

Metamath Proof Explorer

Theorem suppssof1

Proof