Metamath Proof Explorer

Theorem 0oval

Description: Value of the zero operator. (Contributed by NM, 28-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses 0oval.1 ⊢ X = BaseSet ⁡ U
0oval.6 ⊢ Z = 0 vec ⁡ W
0oval.0 ⊢ O = U 0 op W
Assertion 0oval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ A ∈ X → O ⁡ A = Z

Proof

Step Hyp Ref Expression
1 0oval.1 ⊢ X = BaseSet ⁡ U
2 0oval.6 ⊢ Z = 0 vec ⁡ W
3 0oval.0 ⊢ O = U 0 op W
4 1 2 3 0ofval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → O = X × Z
5 4 fveq1d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → O ⁡ A = X × Z ⁡ A
6 5 3adant3 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ A ∈ X → O ⁡ A = X × Z ⁡ A
7 2 fvexi ⊢ Z ∈ V
8 7 fvconst2 ⊢ A ∈ X → X × Z ⁡ A = Z
9 8 3ad2ant3 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ A ∈ X → X × Z ⁡ A = Z
10 6 9 eqtrd ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ A ∈ X → O ⁡ A = Z