Theorem 0oo

Description: The zero operator is an operator. (Contributed by NM, 28-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	0oo.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	0oo.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	0oo.0	⊢ 𝑍 = ( 𝑈 0op 𝑊 )
Assertion	0oo	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 : 𝑋 ⟶ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		0oo.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		0oo.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		0oo.0	⊢ 𝑍 = ( 𝑈 0op 𝑊 )
4		fvex	⊢ ( 0vec ‘ 𝑊 ) ∈ V
5	4	fconst	⊢ ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ { ( 0vec ‘ 𝑊 ) }
6		eqid	⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
7	2 6	nvzcl	⊢ ( 𝑊 ∈ NrmCVec → ( 0vec ‘ 𝑊 ) ∈ 𝑌 )
8	7	snssd	⊢ ( 𝑊 ∈ NrmCVec → { ( 0vec ‘ 𝑊 ) } ⊆ 𝑌 )
9		fss	⊢ ( ( ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ { ( 0vec ‘ 𝑊 ) } ∧ { ( 0vec ‘ 𝑊 ) } ⊆ 𝑌 ) → ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ 𝑌 )
10	5 8 9	sylancr	⊢ ( 𝑊 ∈ NrmCVec → ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ 𝑌 )
11	10	adantl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ 𝑌 )
12	1 6 3	0ofval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 = ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) )
13	12	feq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑍 : 𝑋 ⟶ 𝑌 ↔ ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ 𝑌 ) )
14	11 13	mpbird	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 : 𝑋 ⟶ 𝑌 )