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

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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
0oval.6 ⊢ 𝑍 = ( 0vec ‘ 𝑊 )
0oval.0 ⊢ 𝑂 = ( 𝑈 0op 𝑊 )
Assertion 0oval ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 0oval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 0oval.6 ⊢ 𝑍 = ( 0vec ‘ 𝑊 )
3 0oval.0 ⊢ 𝑂 = ( 𝑈 0op 𝑊 )
4 1 2 3 0ofval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑂 = ( 𝑋 × { 𝑍 } ) )
5 4 fveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑂 ‘ 𝐴 ) = ( ( 𝑋 × { 𝑍 } ) ‘ 𝐴 ) )
6 5 3adant3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = ( ( 𝑋 × { 𝑍 } ) ‘ 𝐴 ) )
7 2 fvexi ⊢ 𝑍 ∈ V
8 7 fvconst2 ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑋 × { 𝑍 } ) ‘ 𝐴 ) = 𝑍 )
9 8 3ad2ant3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑋 × { 𝑍 } ) ‘ 𝐴 ) = 𝑍 )
10 6 9 eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = 𝑍 )