MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvcmulf Structured version   Visualization version   GIF version

Theorem dvcmulf 23949
Description: The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
Hypotheses
Ref Expression
dvcmul.s (𝜑𝑆 ∈ {ℝ, ℂ})
dvcmul.f (𝜑𝐹:𝑋⟶ℂ)
dvcmul.a (𝜑𝐴 ∈ ℂ)
dvcmulf.df (𝜑 → dom (𝑆 D 𝐹) = 𝑋)
Assertion
Ref Expression
dvcmulf (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ∘𝑓 · 𝐹)) = ((𝑆 × {𝐴}) ∘𝑓 · (𝑆 D 𝐹)))

Proof of Theorem dvcmulf
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dvcmul.s . . 3 (𝜑𝑆 ∈ {ℝ, ℂ})
2 dvcmul.a . . . . 5 (𝜑𝐴 ∈ ℂ)
3 fconstg 6247 . . . . 5 (𝐴 ∈ ℂ → (𝑋 × {𝐴}):𝑋⟶{𝐴})
42, 3syl 17 . . . 4 (𝜑 → (𝑋 × {𝐴}):𝑋⟶{𝐴})
52snssd 4486 . . . 4 (𝜑 → {𝐴} ⊆ ℂ)
64, 5fssd 6210 . . 3 (𝜑 → (𝑋 × {𝐴}):𝑋⟶ℂ)
7 dvcmul.f . . 3 (𝜑𝐹:𝑋⟶ℂ)
8 c0ex 10257 . . . . . 6 0 ∈ V
98fconst 6246 . . . . 5 (𝑋 × {0}):𝑋⟶{0}
10 recnprss 23909 . . . . . . . . 9 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
111, 10syl 17 . . . . . . . 8 (𝜑𝑆 ⊆ ℂ)
12 fconstg 6247 . . . . . . . . . 10 (𝐴 ∈ ℂ → (𝑆 × {𝐴}):𝑆⟶{𝐴})
132, 12syl 17 . . . . . . . . 9 (𝜑 → (𝑆 × {𝐴}):𝑆⟶{𝐴})
1413, 5fssd 6210 . . . . . . . 8 (𝜑 → (𝑆 × {𝐴}):𝑆⟶ℂ)
15 ssid 3780 . . . . . . . . 9 𝑆𝑆
1615a1i 11 . . . . . . . 8 (𝜑𝑆𝑆)
17 dvcmulf.df . . . . . . . . 9 (𝜑 → dom (𝑆 D 𝐹) = 𝑋)
18 dvbsss 23907 . . . . . . . . . 10 dom (𝑆 D 𝐹) ⊆ 𝑆
1918a1i 11 . . . . . . . . 9 (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑆)
2017, 19eqsstr3d 3796 . . . . . . . 8 (𝜑𝑋𝑆)
21 eqid 2774 . . . . . . . . 9 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
22 eqid 2774 . . . . . . . . 9 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
2321, 22dvres 23916 . . . . . . . 8 (((𝑆 ⊆ ℂ ∧ (𝑆 × {𝐴}):𝑆⟶ℂ) ∧ (𝑆𝑆𝑋𝑆)) → (𝑆 D ((𝑆 × {𝐴}) ↾ 𝑋)) = ((𝑆 D (𝑆 × {𝐴})) ↾ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)))
2411, 14, 16, 20, 23syl22anc 856 . . . . . . 7 (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ↾ 𝑋)) = ((𝑆 D (𝑆 × {𝐴})) ↾ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)))
2520resmptd 5603 . . . . . . . . 9 (𝜑 → ((𝑥𝑆𝐴) ↾ 𝑋) = (𝑥𝑋𝐴))
26 fconstmpt 5315 . . . . . . . . . 10 (𝑆 × {𝐴}) = (𝑥𝑆𝐴)
2726reseq1i 5542 . . . . . . . . 9 ((𝑆 × {𝐴}) ↾ 𝑋) = ((𝑥𝑆𝐴) ↾ 𝑋)
28 fconstmpt 5315 . . . . . . . . 9 (𝑋 × {𝐴}) = (𝑥𝑋𝐴)
2925, 27, 283eqtr4g 2833 . . . . . . . 8 (𝜑 → ((𝑆 × {𝐴}) ↾ 𝑋) = (𝑋 × {𝐴}))
3029oveq2d 6828 . . . . . . 7 (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ↾ 𝑋)) = (𝑆 D (𝑋 × {𝐴})))
3120resmptd 5603 . . . . . . . 8 (𝜑 → ((𝑥𝑆 ↦ 0) ↾ 𝑋) = (𝑥𝑋 ↦ 0))
32 fconstg 6247 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (ℂ × {𝐴}):ℂ⟶{𝐴})
332, 32syl 17 . . . . . . . . . . . . 13 (𝜑 → (ℂ × {𝐴}):ℂ⟶{𝐴})
3433, 5fssd 6210 . . . . . . . . . . . 12 (𝜑 → (ℂ × {𝐴}):ℂ⟶ℂ)
35 ssid 3780 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
3635a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ⊆ ℂ)
37 dvconst 23921 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → (ℂ D (ℂ × {𝐴})) = (ℂ × {0}))
382, 37syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (ℂ D (ℂ × {𝐴})) = (ℂ × {0}))
3938dmeqd 5476 . . . . . . . . . . . . . 14 (𝜑 → dom (ℂ D (ℂ × {𝐴})) = dom (ℂ × {0}))
408fconst 6246 . . . . . . . . . . . . . . 15 (ℂ × {0}):ℂ⟶{0}
4140fdmi 6206 . . . . . . . . . . . . . 14 dom (ℂ × {0}) = ℂ
4239, 41syl6eq 2824 . . . . . . . . . . . . 13 (𝜑 → dom (ℂ D (ℂ × {𝐴})) = ℂ)
4311, 42sseqtr4d 3798 . . . . . . . . . . . 12 (𝜑𝑆 ⊆ dom (ℂ D (ℂ × {𝐴})))
44 dvres3 23918 . . . . . . . . . . . 12 (((𝑆 ∈ {ℝ, ℂ} ∧ (ℂ × {𝐴}):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ 𝑆 ⊆ dom (ℂ D (ℂ × {𝐴})))) → (𝑆 D ((ℂ × {𝐴}) ↾ 𝑆)) = ((ℂ D (ℂ × {𝐴})) ↾ 𝑆))
451, 34, 36, 43, 44syl22anc 856 . . . . . . . . . . 11 (𝜑 → (𝑆 D ((ℂ × {𝐴}) ↾ 𝑆)) = ((ℂ D (ℂ × {𝐴})) ↾ 𝑆))
46 xpssres 5585 . . . . . . . . . . . . 13 (𝑆 ⊆ ℂ → ((ℂ × {𝐴}) ↾ 𝑆) = (𝑆 × {𝐴}))
4711, 46syl 17 . . . . . . . . . . . 12 (𝜑 → ((ℂ × {𝐴}) ↾ 𝑆) = (𝑆 × {𝐴}))
4847oveq2d 6828 . . . . . . . . . . 11 (𝜑 → (𝑆 D ((ℂ × {𝐴}) ↾ 𝑆)) = (𝑆 D (𝑆 × {𝐴})))
4938reseq1d 5545 . . . . . . . . . . . 12 (𝜑 → ((ℂ D (ℂ × {𝐴})) ↾ 𝑆) = ((ℂ × {0}) ↾ 𝑆))
50 xpssres 5585 . . . . . . . . . . . . 13 (𝑆 ⊆ ℂ → ((ℂ × {0}) ↾ 𝑆) = (𝑆 × {0}))
5111, 50syl 17 . . . . . . . . . . . 12 (𝜑 → ((ℂ × {0}) ↾ 𝑆) = (𝑆 × {0}))
5249, 51eqtrd 2808 . . . . . . . . . . 11 (𝜑 → ((ℂ D (ℂ × {𝐴})) ↾ 𝑆) = (𝑆 × {0}))
5345, 48, 523eqtr3d 2816 . . . . . . . . . 10 (𝜑 → (𝑆 D (𝑆 × {𝐴})) = (𝑆 × {0}))
54 fconstmpt 5315 . . . . . . . . . 10 (𝑆 × {0}) = (𝑥𝑆 ↦ 0)
5553, 54syl6eq 2824 . . . . . . . . 9 (𝜑 → (𝑆 D (𝑆 × {𝐴})) = (𝑥𝑆 ↦ 0))
5621cnfldtopon 22826 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
57 resttopon 21206 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
5856, 11, 57sylancr 576 . . . . . . . . . . . 12 (𝜑 → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
59 topontop 20958 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
6058, 59syl 17 . . . . . . . . . . 11 (𝜑 → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
61 toponuni 20959 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
6258, 61syl 17 . . . . . . . . . . . 12 (𝜑𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
6320, 62sseqtrd 3797 . . . . . . . . . . 11 (𝜑𝑋 ((TopOpen‘ℂfld) ↾t 𝑆))
64 eqid 2774 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
6564ntrss2 21102 . . . . . . . . . . 11 ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ 𝑋 ((TopOpen‘ℂfld) ↾t 𝑆)) → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋) ⊆ 𝑋)
6660, 63, 65syl2anc 574 . . . . . . . . . 10 (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋) ⊆ 𝑋)
6711, 7, 20, 22, 21dvbssntr 23905 . . . . . . . . . . 11 (𝜑 → dom (𝑆 D 𝐹) ⊆ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋))
6817, 67eqsstr3d 3796 . . . . . . . . . 10 (𝜑𝑋 ⊆ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋))
6966, 68eqssd 3775 . . . . . . . . 9 (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋) = 𝑋)
7055, 69reseq12d 5547 . . . . . . . 8 (𝜑 → ((𝑆 D (𝑆 × {𝐴})) ↾ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)) = ((𝑥𝑆 ↦ 0) ↾ 𝑋))
71 fconstmpt 5315 . . . . . . . . 9 (𝑋 × {0}) = (𝑥𝑋 ↦ 0)
7271a1i 11 . . . . . . . 8 (𝜑 → (𝑋 × {0}) = (𝑥𝑋 ↦ 0))
7331, 70, 723eqtr4d 2818 . . . . . . 7 (𝜑 → ((𝑆 D (𝑆 × {𝐴})) ↾ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝑋)) = (𝑋 × {0}))
7424, 30, 733eqtr3d 2816 . . . . . 6 (𝜑 → (𝑆 D (𝑋 × {𝐴})) = (𝑋 × {0}))
7574feq1d 6181 . . . . 5 (𝜑 → ((𝑆 D (𝑋 × {𝐴})):𝑋⟶{0} ↔ (𝑋 × {0}):𝑋⟶{0}))
769, 75mpbiri 249 . . . 4 (𝜑 → (𝑆 D (𝑋 × {𝐴})):𝑋⟶{0})
7776fdmd 6205 . . 3 (𝜑 → dom (𝑆 D (𝑋 × {𝐴})) = 𝑋)
781, 6, 7, 77, 17dvmulf 23947 . 2 (𝜑 → (𝑆 D ((𝑋 × {𝐴}) ∘𝑓 · 𝐹)) = (((𝑆 D (𝑋 × {𝐴})) ∘𝑓 · 𝐹) ∘𝑓 + ((𝑆 D 𝐹) ∘𝑓 · (𝑋 × {𝐴}))))
79 sseqin2 3975 . . . . . 6 (𝑋𝑆 ↔ (𝑆𝑋) = 𝑋)
8020, 79sylib 209 . . . . 5 (𝜑 → (𝑆𝑋) = 𝑋)
8180mpteq1d 4885 . . . 4 (𝜑 → (𝑥 ∈ (𝑆𝑋) ↦ (𝐴 · (𝐹𝑥))) = (𝑥𝑋 ↦ (𝐴 · (𝐹𝑥))))
8213ffnd 6197 . . . . 5 (𝜑 → (𝑆 × {𝐴}) Fn 𝑆)
837ffnd 6197 . . . . 5 (𝜑𝐹 Fn 𝑋)
841, 20ssexd 4953 . . . . 5 (𝜑𝑋 ∈ V)
85 eqid 2774 . . . . 5 (𝑆𝑋) = (𝑆𝑋)
86 fvconst2g 6630 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑥𝑆) → ((𝑆 × {𝐴})‘𝑥) = 𝐴)
872, 86sylan 570 . . . . 5 ((𝜑𝑥𝑆) → ((𝑆 × {𝐴})‘𝑥) = 𝐴)
88 eqidd 2775 . . . . 5 ((𝜑𝑥𝑋) → (𝐹𝑥) = (𝐹𝑥))
8982, 83, 1, 84, 85, 87, 88offval 7072 . . . 4 (𝜑 → ((𝑆 × {𝐴}) ∘𝑓 · 𝐹) = (𝑥 ∈ (𝑆𝑋) ↦ (𝐴 · (𝐹𝑥))))
904ffnd 6197 . . . . 5 (𝜑 → (𝑋 × {𝐴}) Fn 𝑋)
91 inidm 3978 . . . . 5 (𝑋𝑋) = 𝑋
92 fvconst2g 6630 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑥𝑋) → ((𝑋 × {𝐴})‘𝑥) = 𝐴)
932, 92sylan 570 . . . . 5 ((𝜑𝑥𝑋) → ((𝑋 × {𝐴})‘𝑥) = 𝐴)
9490, 83, 84, 84, 91, 93, 88offval 7072 . . . 4 (𝜑 → ((𝑋 × {𝐴}) ∘𝑓 · 𝐹) = (𝑥𝑋 ↦ (𝐴 · (𝐹𝑥))))
9581, 89, 943eqtr4d 2818 . . 3 (𝜑 → ((𝑆 × {𝐴}) ∘𝑓 · 𝐹) = ((𝑋 × {𝐴}) ∘𝑓 · 𝐹))
9695oveq2d 6828 . 2 (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ∘𝑓 · 𝐹)) = (𝑆 D ((𝑋 × {𝐴}) ∘𝑓 · 𝐹)))
9780mpteq1d 4885 . . 3 (𝜑 → (𝑥 ∈ (𝑆𝑋) ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥))) = (𝑥𝑋 ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥))))
98 dvfg 23911 . . . . . . 7 (𝑆 ∈ {ℝ, ℂ} → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)
991, 98syl 17 . . . . . 6 (𝜑 → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)
10017feq2d 6182 . . . . . 6 (𝜑 → ((𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ ↔ (𝑆 D 𝐹):𝑋⟶ℂ))
10199, 100mpbid 223 . . . . 5 (𝜑 → (𝑆 D 𝐹):𝑋⟶ℂ)
102101ffnd 6197 . . . 4 (𝜑 → (𝑆 D 𝐹) Fn 𝑋)
103 eqidd 2775 . . . 4 ((𝜑𝑥𝑋) → ((𝑆 D 𝐹)‘𝑥) = ((𝑆 D 𝐹)‘𝑥))
10482, 102, 1, 84, 85, 87, 103offval 7072 . . 3 (𝜑 → ((𝑆 × {𝐴}) ∘𝑓 · (𝑆 D 𝐹)) = (𝑥 ∈ (𝑆𝑋) ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥))))
105 0cnd 10256 . . . . 5 ((𝜑𝑥𝑋) → 0 ∈ ℂ)
106 ovexd 6846 . . . . 5 ((𝜑𝑥𝑋) → (((𝑆 D 𝐹)‘𝑥) · 𝐴) ∈ V)
10774oveq1d 6827 . . . . . . 7 (𝜑 → ((𝑆 D (𝑋 × {𝐴})) ∘𝑓 · 𝐹) = ((𝑋 × {0}) ∘𝑓 · 𝐹))
108 0cnd 10256 . . . . . . . 8 (𝜑 → 0 ∈ ℂ)
109 mul02 10437 . . . . . . . . 9 (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
110109adantl 468 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
11184, 7, 108, 108, 110caofid2 7096 . . . . . . 7 (𝜑 → ((𝑋 × {0}) ∘𝑓 · 𝐹) = (𝑋 × {0}))
112107, 111eqtrd 2808 . . . . . 6 (𝜑 → ((𝑆 D (𝑋 × {𝐴})) ∘𝑓 · 𝐹) = (𝑋 × {0}))
113112, 71syl6eq 2824 . . . . 5 (𝜑 → ((𝑆 D (𝑋 × {𝐴})) ∘𝑓 · 𝐹) = (𝑥𝑋 ↦ 0))
114 fvexd 6361 . . . . . 6 ((𝜑𝑥𝑋) → ((𝑆 D 𝐹)‘𝑥) ∈ V)
1152adantr 467 . . . . . 6 ((𝜑𝑥𝑋) → 𝐴 ∈ ℂ)
116101feqmptd 6408 . . . . . 6 (𝜑 → (𝑆 D 𝐹) = (𝑥𝑋 ↦ ((𝑆 D 𝐹)‘𝑥)))
11728a1i 11 . . . . . 6 (𝜑 → (𝑋 × {𝐴}) = (𝑥𝑋𝐴))
11884, 114, 115, 116, 117offval2 7082 . . . . 5 (𝜑 → ((𝑆 D 𝐹) ∘𝑓 · (𝑋 × {𝐴})) = (𝑥𝑋 ↦ (((𝑆 D 𝐹)‘𝑥) · 𝐴)))
11984, 105, 106, 113, 118offval2 7082 . . . 4 (𝜑 → (((𝑆 D (𝑋 × {𝐴})) ∘𝑓 · 𝐹) ∘𝑓 + ((𝑆 D 𝐹) ∘𝑓 · (𝑋 × {𝐴}))) = (𝑥𝑋 ↦ (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴))))
120101ffvelrnda 6519 . . . . . . . 8 ((𝜑𝑥𝑋) → ((𝑆 D 𝐹)‘𝑥) ∈ ℂ)
121120, 115mulcld 10283 . . . . . . 7 ((𝜑𝑥𝑋) → (((𝑆 D 𝐹)‘𝑥) · 𝐴) ∈ ℂ)
122121addid2d 10460 . . . . . 6 ((𝜑𝑥𝑋) → (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴)) = (((𝑆 D 𝐹)‘𝑥) · 𝐴))
123120, 115mulcomd 10284 . . . . . 6 ((𝜑𝑥𝑋) → (((𝑆 D 𝐹)‘𝑥) · 𝐴) = (𝐴 · ((𝑆 D 𝐹)‘𝑥)))
124122, 123eqtrd 2808 . . . . 5 ((𝜑𝑥𝑋) → (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴)) = (𝐴 · ((𝑆 D 𝐹)‘𝑥)))
125124mpteq2dva 4891 . . . 4 (𝜑 → (𝑥𝑋 ↦ (0 + (((𝑆 D 𝐹)‘𝑥) · 𝐴))) = (𝑥𝑋 ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥))))
126119, 125eqtrd 2808 . . 3 (𝜑 → (((𝑆 D (𝑋 × {𝐴})) ∘𝑓 · 𝐹) ∘𝑓 + ((𝑆 D 𝐹) ∘𝑓 · (𝑋 × {𝐴}))) = (𝑥𝑋 ↦ (𝐴 · ((𝑆 D 𝐹)‘𝑥))))
12797, 104, 1263eqtr4d 2818 . 2 (𝜑 → ((𝑆 × {𝐴}) ∘𝑓 · (𝑆 D 𝐹)) = (((𝑆 D (𝑋 × {𝐴})) ∘𝑓 · 𝐹) ∘𝑓 + ((𝑆 D 𝐹) ∘𝑓 · (𝑋 × {𝐴}))))
12878, 96, 1273eqtr4d 2818 1 (𝜑 → (𝑆 D ((𝑆 × {𝐴}) ∘𝑓 · 𝐹)) = ((𝑆 × {𝐴}) ∘𝑓 · (𝑆 D 𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1634  wcel 2148  Vcvv 3355  cin 3728  wss 3729  {csn 4326  {cpr 4328   cuni 4585  cmpt 4876   × cxp 5261  dom cdm 5263  cres 5265  wf 6038  cfv 6042  (class class class)co 6812  𝑓 cof 7063  cc 10157  cr 10158  0cc0 10159   + caddc 10162   · cmul 10164  t crest 16309  TopOpenctopn 16310  fldccnfld 19981  Topctop 20938  TopOnctopon 20955  intcnt 21062   D cdv 23868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-inf2 8723  ax-cnex 10215  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236  ax-pre-sup 10237  ax-addf 10238  ax-mulf 10239
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-iin 4668  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-se 5223  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-isom 6051  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-of 7065  df-om 7234  df-1st 7336  df-2nd 7337  df-supp 7468  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-1o 7734  df-2o 7735  df-oadd 7738  df-er 7917  df-map 8032  df-pm 8033  df-ixp 8084  df-en 8131  df-dom 8132  df-sdom 8133  df-fin 8134  df-fsupp 8453  df-fi 8494  df-sup 8525  df-inf 8526  df-oi 8592  df-card 8986  df-cda 9213  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-div 10908  df-nn 11244  df-2 11302  df-3 11303  df-4 11304  df-5 11305  df-6 11306  df-7 11307  df-8 11308  df-9 11309  df-n0 11517  df-z 11602  df-dec 11718  df-uz 11911  df-q 12014  df-rp 12053  df-xneg 12168  df-xadd 12169  df-xmul 12170  df-icc 12406  df-fz 12556  df-fzo 12696  df-seq 13031  df-exp 13090  df-hash 13344  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-abs 14206  df-struct 16086  df-ndx 16087  df-slot 16088  df-base 16090  df-sets 16091  df-ress 16092  df-plusg 16182  df-mulr 16183  df-starv 16184  df-sca 16185  df-vsca 16186  df-ip 16187  df-tset 16188  df-ple 16189  df-ds 16192  df-unif 16193  df-hom 16194  df-cco 16195  df-rest 16311  df-topn 16312  df-0g 16330  df-gsum 16331  df-topgen 16332  df-pt 16333  df-prds 16336  df-xrs 16390  df-qtop 16395  df-imas 16396  df-xps 16398  df-mre 16474  df-mrc 16475  df-acs 16477  df-mgm 17470  df-sgrp 17512  df-mnd 17523  df-submnd 17564  df-mulg 17769  df-cntz 17977  df-cmn 18422  df-psmet 19973  df-xmet 19974  df-met 19975  df-bl 19976  df-mopn 19977  df-fbas 19978  df-fg 19979  df-cnfld 19982  df-top 20939  df-topon 20956  df-topsp 20978  df-bases 20991  df-cld 21064  df-ntr 21065  df-cls 21066  df-nei 21143  df-lp 21181  df-perf 21182  df-cn 21272  df-cnp 21273  df-haus 21360  df-tx 21606  df-hmeo 21799  df-fil 21890  df-fm 21982  df-flim 21983  df-flf 21984  df-xms 22365  df-ms 22366  df-tms 22367  df-cncf 22921  df-limc 23871  df-dv 23872
This theorem is referenced by:  dvsinax  40651
  Copyright terms: Public domain W3C validator