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

Metamath Proof Explorer

Theorem 0ofval

Description: The zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses 0oval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
0oval.6 ⊢ 𝑍 = ( 0vec ‘ 𝑊 )
0oval.0 ⊢ 𝑂 = ( 𝑈 0op 𝑊 )
Assertion 0ofval ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑂 = ( 𝑋 × { 𝑍 } ) )

Proof

Step Hyp Ref Expression
1 0oval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 0oval.6 ⊢ 𝑍 = ( 0vec ‘ 𝑊 )
3 0oval.0 ⊢ 𝑂 = ( 𝑈 0op 𝑊 )
4 fveq2 ⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = ( BaseSet ‘ 𝑈 ) )
5 4 1 eqtr4di ⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = 𝑋 )
6 5 xpeq1d ⊢ ( 𝑢 = 𝑈 → ( ( BaseSet ‘ 𝑢 ) × { ( 0vec ‘ 𝑤 ) } ) = ( 𝑋 × { ( 0vec ‘ 𝑤 ) } ) )
7 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 0vec ‘ 𝑤 ) = ( 0vec ‘ 𝑊 ) )
8 7 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( 0vec ‘ 𝑤 ) = 𝑍 )
9 8 sneqd ⊢ ( 𝑤 = 𝑊 → { ( 0vec ‘ 𝑤 ) } = { 𝑍 } )
10 9 xpeq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑋 × { ( 0vec ‘ 𝑤 ) } ) = ( 𝑋 × { 𝑍 } ) )
11 df-0o ⊢ 0op = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ ( ( BaseSet ‘ 𝑢 ) × { ( 0vec ‘ 𝑤 ) } ) )
12 1 fvexi ⊢ 𝑋 ∈ V
13 snex ⊢ { 𝑍 } ∈ V
14 12 13 xpex ⊢ ( 𝑋 × { 𝑍 } ) ∈ V
15 6 10 11 14 ovmpo ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑈 0op 𝑊 ) = ( 𝑋 × { 𝑍 } ) )
16 3 15 eqtrid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑂 = ( 𝑋 × { 𝑍 } ) )