Theorem nvo00

Description: Two ways to express a zero operator. (Contributed by NM, 27-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nvo00.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
Assertion	nvo00	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑇 = ( 𝑋 × { 𝑍 } ) ↔ ran 𝑇 = { 𝑍 } ) )

Proof

Step	Hyp	Ref	Expression
1		nvo00.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		ffn	⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → 𝑇 Fn 𝑋 )
3		eqid	⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
4	1 3	nvzcl	⊢ ( 𝑈 ∈ NrmCVec → ( 0vec ‘ 𝑈 ) ∈ 𝑋 )
5	4	ne0d	⊢ ( 𝑈 ∈ NrmCVec → 𝑋 ≠ ∅ )
6		fconst5	⊢ ( ( 𝑇 Fn 𝑋 ∧ 𝑋 ≠ ∅ ) → ( 𝑇 = ( 𝑋 × { 𝑍 } ) ↔ ran 𝑇 = { 𝑍 } ) )
7	2 5 6	syl2anr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑇 = ( 𝑋 × { 𝑍 } ) ↔ ran 𝑇 = { 𝑍 } ) )