This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → A supp Y ⊆ L
suppssof1.o ⊢ φ ∧ v ∈ R → Y O v = Z
suppssof1.a ⊢ φ → A : D ⟶ V
suppssof1.b ⊢ φ → B : D ⟶ R
suppssof1.d ⊢ φ → D ∈ W
suppssof1.y ⊢ φ → Y ∈ U
Assertion suppssof1 ⊢ φ → A O f B supp Z ⊆ L

Proof

Step Hyp Ref Expression
1 suppssof1.s ⊢ φ → A supp Y ⊆ L
2 suppssof1.o ⊢ φ ∧ v ∈ R → Y O v = Z
3 suppssof1.a ⊢ φ → A : D ⟶ V
4 suppssof1.b ⊢ φ → B : D ⟶ R
5 suppssof1.d ⊢ φ → D ∈ W
6 suppssof1.y ⊢ φ → Y ∈ U
7 3 ffnd ⊢ φ → A Fn D
8 4 ffnd ⊢ φ → B Fn D
9 inidm ⊢ D ∩ D = D
10 eqidd ⊢ φ ∧ x ∈ D → A ⁡ x = A ⁡ x
11 eqidd ⊢ φ ∧ x ∈ D → B ⁡ x = B ⁡ x
12 7 8 5 5 9 10 11 offval ⊢ φ → A O f B = x ∈ D ⟼ A ⁡ x O B ⁡ x
13 12 oveq1d ⊢ φ → A O f B supp Z = x ∈ D ⟼ A ⁡ x O B ⁡ x supp Z
14 3 feqmptd ⊢ φ → A = x ∈ D ⟼ A ⁡ x
15 14 oveq1d ⊢ φ → A supp Y = x ∈ D ⟼ A ⁡ x supp Y
16 15 1 eqsstrrd ⊢ φ → x ∈ D ⟼ A ⁡ x supp Y ⊆ L
17 fvexd ⊢ φ ∧ x ∈ D → A ⁡ x ∈ V
18 4 ffvelcdmda ⊢ φ ∧ x ∈ D → B ⁡ x ∈ R
19 16 2 17 18 6 suppssov1 ⊢ φ → x ∈ D ⟼ A ⁡ x O B ⁡ x supp Z ⊆ L
20 13 19 eqsstrd ⊢ φ → A O f B supp Z ⊆ L