Theorem 0oo 28162

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

Hypotheses

Ref	Expression
0oo.1	⊢ 𝑋 = (BaseSet‘𝑈)
0oo.2	⊢ 𝑌 = (BaseSet‘𝑊)
0oo.0	⊢ 𝑍 = (𝑈 0op 𝑊)

Assertion

Ref	Expression
0oo	⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:𝑋⟶𝑌)

Proof of Theorem 0oo

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

Syntax hints:   → wi 4   ∧ wa 385   = wceq 1653   ∈ wcel 2157   ⊆ wss 3768  {csn 4367   × cxp 5309  ⟶wf 6096  ‘cfv 6100  (class class class)co 6877  NrmCVeccnv 27957  BaseSetcba 27959  0_veccn0v 27961   0_op c0o 28116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-rep 4963  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4628  df-iun 4711  df-br 4843  df-opab 4905  df-mpt 4922  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-1st 7400  df-2nd 7401  df-grpo 27866  df-gid 27867  df-ablo 27918  df-vc 27932  df-nv 27965  df-va 27968  df-ba 27969  df-sm 27970  df-0v 27971  df-nmcv 27973  df-0o 28120

This theorem is referenced by:  0lno  28163  nmoo0  28164  nmlno0lem  28166