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	syl5eq	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑂 = ( 𝑋 × { 𝑍 } ) )