Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ftc1anclem3 Structured version   Visualization version   GIF version

Theorem ftc1anclem3 33146
Description: Lemma for ftc1anc 33152- the absolute value of the sum of a simple function and i times another simple function is itself a simple function. (Contributed by Brendan Leahy, 27-May-2018.)
Assertion
Ref Expression
ftc1anclem3 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (abs ∘ (𝐹𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺))) ∈ dom ∫1)

Proof of Theorem ftc1anclem3
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 i1ff 23362 . . . . . . . 8 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
21ffvelrnda 6320 . . . . . . 7 ((𝐹 ∈ dom ∫1𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
3 i1ff 23362 . . . . . . . 8 (𝐺 ∈ dom ∫1𝐺:ℝ⟶ℝ)
43ffvelrnda 6320 . . . . . . 7 ((𝐺 ∈ dom ∫1𝑥 ∈ ℝ) → (𝐺𝑥) ∈ ℝ)
5 absreim 13974 . . . . . . 7 (((𝐹𝑥) ∈ ℝ ∧ (𝐺𝑥) ∈ ℝ) → (abs‘((𝐹𝑥) + (i · (𝐺𝑥)))) = (√‘(((𝐹𝑥)↑2) + ((𝐺𝑥)↑2))))
62, 4, 5syl2an 494 . . . . . 6 (((𝐹 ∈ dom ∫1𝑥 ∈ ℝ) ∧ (𝐺 ∈ dom ∫1𝑥 ∈ ℝ)) → (abs‘((𝐹𝑥) + (i · (𝐺𝑥)))) = (√‘(((𝐹𝑥)↑2) + ((𝐺𝑥)↑2))))
76anandirs 873 . . . . 5 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (abs‘((𝐹𝑥) + (i · (𝐺𝑥)))) = (√‘(((𝐹𝑥)↑2) + ((𝐺𝑥)↑2))))
82recnd 10019 . . . . . . . . 9 ((𝐹 ∈ dom ∫1𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℂ)
98sqvald 12952 . . . . . . . 8 ((𝐹 ∈ dom ∫1𝑥 ∈ ℝ) → ((𝐹𝑥)↑2) = ((𝐹𝑥) · (𝐹𝑥)))
104recnd 10019 . . . . . . . . 9 ((𝐺 ∈ dom ∫1𝑥 ∈ ℝ) → (𝐺𝑥) ∈ ℂ)
1110sqvald 12952 . . . . . . . 8 ((𝐺 ∈ dom ∫1𝑥 ∈ ℝ) → ((𝐺𝑥)↑2) = ((𝐺𝑥) · (𝐺𝑥)))
129, 11oveqan12d 6629 . . . . . . 7 (((𝐹 ∈ dom ∫1𝑥 ∈ ℝ) ∧ (𝐺 ∈ dom ∫1𝑥 ∈ ℝ)) → (((𝐹𝑥)↑2) + ((𝐺𝑥)↑2)) = (((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥))))
1312anandirs 873 . . . . . 6 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (((𝐹𝑥)↑2) + ((𝐺𝑥)↑2)) = (((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥))))
1413fveq2d 6157 . . . . 5 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (√‘(((𝐹𝑥)↑2) + ((𝐺𝑥)↑2))) = (√‘(((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥)))))
157, 14eqtrd 2655 . . . 4 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (abs‘((𝐹𝑥) + (i · (𝐺𝑥)))) = (√‘(((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥)))))
1615mpteq2dva 4709 . . 3 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ (abs‘((𝐹𝑥) + (i · (𝐺𝑥))))) = (𝑥 ∈ ℝ ↦ (√‘(((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥))))))
17 ax-icn 9946 . . . . . . 7 i ∈ ℂ
18 mulcl 9971 . . . . . . 7 ((i ∈ ℂ ∧ (𝐺𝑥) ∈ ℂ) → (i · (𝐺𝑥)) ∈ ℂ)
1917, 10, 18sylancr 694 . . . . . 6 ((𝐺 ∈ dom ∫1𝑥 ∈ ℝ) → (i · (𝐺𝑥)) ∈ ℂ)
20 addcl 9969 . . . . . 6 (((𝐹𝑥) ∈ ℂ ∧ (i · (𝐺𝑥)) ∈ ℂ) → ((𝐹𝑥) + (i · (𝐺𝑥))) ∈ ℂ)
218, 19, 20syl2an 494 . . . . 5 (((𝐹 ∈ dom ∫1𝑥 ∈ ℝ) ∧ (𝐺 ∈ dom ∫1𝑥 ∈ ℝ)) → ((𝐹𝑥) + (i · (𝐺𝑥))) ∈ ℂ)
2221anandirs 873 . . . 4 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) + (i · (𝐺𝑥))) ∈ ℂ)
23 reex 9978 . . . . . 6 ℝ ∈ V
2423a1i 11 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ℝ ∈ V)
252adantlr 750 . . . . 5 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
26 ovex 6638 . . . . . 6 (i · (𝐺𝑥)) ∈ V
2726a1i 11 . . . . 5 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (i · (𝐺𝑥)) ∈ V)
281feqmptd 6211 . . . . . 6 (𝐹 ∈ dom ∫1𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
2928adantr 481 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
3023a1i 11 . . . . . . 7 (𝐺 ∈ dom ∫1 → ℝ ∈ V)
3117a1i 11 . . . . . . 7 ((𝐺 ∈ dom ∫1𝑥 ∈ ℝ) → i ∈ ℂ)
32 fconstmpt 5128 . . . . . . . 8 (ℝ × {i}) = (𝑥 ∈ ℝ ↦ i)
3332a1i 11 . . . . . . 7 (𝐺 ∈ dom ∫1 → (ℝ × {i}) = (𝑥 ∈ ℝ ↦ i))
343feqmptd 6211 . . . . . . 7 (𝐺 ∈ dom ∫1𝐺 = (𝑥 ∈ ℝ ↦ (𝐺𝑥)))
3530, 31, 4, 33, 34offval2 6874 . . . . . 6 (𝐺 ∈ dom ∫1 → ((ℝ × {i}) ∘𝑓 · 𝐺) = (𝑥 ∈ ℝ ↦ (i · (𝐺𝑥))))
3635adantl 482 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ((ℝ × {i}) ∘𝑓 · 𝐺) = (𝑥 ∈ ℝ ↦ (i · (𝐺𝑥))))
3724, 25, 27, 29, 36offval2 6874 . . . 4 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (𝐹𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺)) = (𝑥 ∈ ℝ ↦ ((𝐹𝑥) + (i · (𝐺𝑥)))))
38 absf 14018 . . . . . 6 abs:ℂ⟶ℝ
3938a1i 11 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → abs:ℂ⟶ℝ)
4039feqmptd 6211 . . . 4 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → abs = (𝑦 ∈ ℂ ↦ (abs‘𝑦)))
41 fveq2 6153 . . . 4 (𝑦 = ((𝐹𝑥) + (i · (𝐺𝑥))) → (abs‘𝑦) = (abs‘((𝐹𝑥) + (i · (𝐺𝑥)))))
4222, 37, 40, 41fmptco 6357 . . 3 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (abs ∘ (𝐹𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺))) = (𝑥 ∈ ℝ ↦ (abs‘((𝐹𝑥) + (i · (𝐺𝑥))))))
438, 8mulcld 10011 . . . . . 6 ((𝐹 ∈ dom ∫1𝑥 ∈ ℝ) → ((𝐹𝑥) · (𝐹𝑥)) ∈ ℂ)
4410, 10mulcld 10011 . . . . . 6 ((𝐺 ∈ dom ∫1𝑥 ∈ ℝ) → ((𝐺𝑥) · (𝐺𝑥)) ∈ ℂ)
45 addcl 9969 . . . . . 6 ((((𝐹𝑥) · (𝐹𝑥)) ∈ ℂ ∧ ((𝐺𝑥) · (𝐺𝑥)) ∈ ℂ) → (((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥))) ∈ ℂ)
4643, 44, 45syl2an 494 . . . . 5 (((𝐹 ∈ dom ∫1𝑥 ∈ ℝ) ∧ (𝐺 ∈ dom ∫1𝑥 ∈ ℝ)) → (((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥))) ∈ ℂ)
4746anandirs 873 . . . 4 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥))) ∈ ℂ)
4843adantlr 750 . . . . 5 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) · (𝐹𝑥)) ∈ ℂ)
4944adantll 749 . . . . 5 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝐺𝑥) · (𝐺𝑥)) ∈ ℂ)
5023a1i 11 . . . . . . 7 (𝐹 ∈ dom ∫1 → ℝ ∈ V)
5150, 2, 2, 28, 28offval2 6874 . . . . . 6 (𝐹 ∈ dom ∫1 → (𝐹𝑓 · 𝐹) = (𝑥 ∈ ℝ ↦ ((𝐹𝑥) · (𝐹𝑥))))
5251adantr 481 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (𝐹𝑓 · 𝐹) = (𝑥 ∈ ℝ ↦ ((𝐹𝑥) · (𝐹𝑥))))
5330, 4, 4, 34, 34offval2 6874 . . . . . 6 (𝐺 ∈ dom ∫1 → (𝐺𝑓 · 𝐺) = (𝑥 ∈ ℝ ↦ ((𝐺𝑥) · (𝐺𝑥))))
5453adantl 482 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (𝐺𝑓 · 𝐺) = (𝑥 ∈ ℝ ↦ ((𝐺𝑥) · (𝐺𝑥))))
5524, 48, 49, 52, 54offval2 6874 . . . 4 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) = (𝑥 ∈ ℝ ↦ (((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥)))))
56 sqrtf 14044 . . . . . 6 √:ℂ⟶ℂ
5756a1i 11 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → √:ℂ⟶ℂ)
5857feqmptd 6211 . . . 4 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → √ = (𝑦 ∈ ℂ ↦ (√‘𝑦)))
59 fveq2 6153 . . . 4 (𝑦 = (((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥))) → (√‘𝑦) = (√‘(((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥)))))
6047, 55, 58, 59fmptco 6357 . . 3 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) = (𝑥 ∈ ℝ ↦ (√‘(((𝐹𝑥) · (𝐹𝑥)) + ((𝐺𝑥) · (𝐺𝑥))))))
6116, 42, 603eqtr4d 2665 . 2 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (abs ∘ (𝐹𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺))) = (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))))
62 elrege0 12227 . . . . . . 7 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
63 resqrtcl 13935 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (√‘𝑥) ∈ ℝ)
6462, 63sylbi 207 . . . . . 6 (𝑥 ∈ (0[,)+∞) → (√‘𝑥) ∈ ℝ)
6564adantl 482 . . . . 5 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ (0[,)+∞)) → (√‘𝑥) ∈ ℝ)
66 id 22 . . . . . . . . 9 (√:ℂ⟶ℂ → √:ℂ⟶ℂ)
6766feqmptd 6211 . . . . . . . 8 (√:ℂ⟶ℂ → √ = (𝑥 ∈ ℂ ↦ (√‘𝑥)))
6856, 67ax-mp 5 . . . . . . 7 √ = (𝑥 ∈ ℂ ↦ (√‘𝑥))
6968reseq1i 5357 . . . . . 6 (√ ↾ (0[,)+∞)) = ((𝑥 ∈ ℂ ↦ (√‘𝑥)) ↾ (0[,)+∞))
70 rge0ssre 12229 . . . . . . . 8 (0[,)+∞) ⊆ ℝ
71 ax-resscn 9944 . . . . . . . 8 ℝ ⊆ ℂ
7270, 71sstri 3596 . . . . . . 7 (0[,)+∞) ⊆ ℂ
73 resmpt 5413 . . . . . . 7 ((0[,)+∞) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (√‘𝑥)) ↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦ (√‘𝑥)))
7472, 73ax-mp 5 . . . . . 6 ((𝑥 ∈ ℂ ↦ (√‘𝑥)) ↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦ (√‘𝑥))
7569, 74eqtri 2643 . . . . 5 (√ ↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦ (√‘𝑥))
7665, 75fmptd 6346 . . . 4 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (√ ↾ (0[,)+∞)):(0[,)+∞)⟶ℝ)
77 ge0addcl 12233 . . . . . 6 ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
7877adantl 482 . . . . 5 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞))
79 oveq12 6619 . . . . . . . . 9 ((𝑧 = 𝐹𝑧 = 𝐹) → (𝑧𝑓 · 𝑧) = (𝐹𝑓 · 𝐹))
8079anidms 676 . . . . . . . 8 (𝑧 = 𝐹 → (𝑧𝑓 · 𝑧) = (𝐹𝑓 · 𝐹))
8180feq1d 5992 . . . . . . 7 (𝑧 = 𝐹 → ((𝑧𝑓 · 𝑧):ℝ⟶(0[,)+∞) ↔ (𝐹𝑓 · 𝐹):ℝ⟶(0[,)+∞)))
82 i1ff 23362 . . . . . . . . . . . 12 (𝑧 ∈ dom ∫1𝑧:ℝ⟶ℝ)
8382ffvelrnda 6320 . . . . . . . . . . 11 ((𝑧 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑧𝑥) ∈ ℝ)
8483, 83remulcld 10021 . . . . . . . . . 10 ((𝑧 ∈ dom ∫1𝑥 ∈ ℝ) → ((𝑧𝑥) · (𝑧𝑥)) ∈ ℝ)
8583msqge0d 10547 . . . . . . . . . 10 ((𝑧 ∈ dom ∫1𝑥 ∈ ℝ) → 0 ≤ ((𝑧𝑥) · (𝑧𝑥)))
86 elrege0 12227 . . . . . . . . . 10 (((𝑧𝑥) · (𝑧𝑥)) ∈ (0[,)+∞) ↔ (((𝑧𝑥) · (𝑧𝑥)) ∈ ℝ ∧ 0 ≤ ((𝑧𝑥) · (𝑧𝑥))))
8784, 85, 86sylanbrc 697 . . . . . . . . 9 ((𝑧 ∈ dom ∫1𝑥 ∈ ℝ) → ((𝑧𝑥) · (𝑧𝑥)) ∈ (0[,)+∞))
88 eqid 2621 . . . . . . . . 9 (𝑥 ∈ ℝ ↦ ((𝑧𝑥) · (𝑧𝑥))) = (𝑥 ∈ ℝ ↦ ((𝑧𝑥) · (𝑧𝑥)))
8987, 88fmptd 6346 . . . . . . . 8 (𝑧 ∈ dom ∫1 → (𝑥 ∈ ℝ ↦ ((𝑧𝑥) · (𝑧𝑥))):ℝ⟶(0[,)+∞))
9023a1i 11 . . . . . . . . . 10 (𝑧 ∈ dom ∫1 → ℝ ∈ V)
9182feqmptd 6211 . . . . . . . . . 10 (𝑧 ∈ dom ∫1𝑧 = (𝑥 ∈ ℝ ↦ (𝑧𝑥)))
9290, 83, 83, 91, 91offval2 6874 . . . . . . . . 9 (𝑧 ∈ dom ∫1 → (𝑧𝑓 · 𝑧) = (𝑥 ∈ ℝ ↦ ((𝑧𝑥) · (𝑧𝑥))))
9392feq1d 5992 . . . . . . . 8 (𝑧 ∈ dom ∫1 → ((𝑧𝑓 · 𝑧):ℝ⟶(0[,)+∞) ↔ (𝑥 ∈ ℝ ↦ ((𝑧𝑥) · (𝑧𝑥))):ℝ⟶(0[,)+∞)))
9489, 93mpbird 247 . . . . . . 7 (𝑧 ∈ dom ∫1 → (𝑧𝑓 · 𝑧):ℝ⟶(0[,)+∞))
9581, 94vtoclga 3261 . . . . . 6 (𝐹 ∈ dom ∫1 → (𝐹𝑓 · 𝐹):ℝ⟶(0[,)+∞))
9695adantr 481 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (𝐹𝑓 · 𝐹):ℝ⟶(0[,)+∞))
97 oveq12 6619 . . . . . . . . 9 ((𝑧 = 𝐺𝑧 = 𝐺) → (𝑧𝑓 · 𝑧) = (𝐺𝑓 · 𝐺))
9897anidms 676 . . . . . . . 8 (𝑧 = 𝐺 → (𝑧𝑓 · 𝑧) = (𝐺𝑓 · 𝐺))
9998feq1d 5992 . . . . . . 7 (𝑧 = 𝐺 → ((𝑧𝑓 · 𝑧):ℝ⟶(0[,)+∞) ↔ (𝐺𝑓 · 𝐺):ℝ⟶(0[,)+∞)))
10099, 94vtoclga 3261 . . . . . 6 (𝐺 ∈ dom ∫1 → (𝐺𝑓 · 𝐺):ℝ⟶(0[,)+∞))
101100adantl 482 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (𝐺𝑓 · 𝐺):ℝ⟶(0[,)+∞))
102 inidm 3805 . . . . 5 (ℝ ∩ ℝ) = ℝ
10378, 96, 101, 24, 24, 102off 6872 . . . 4 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)):ℝ⟶(0[,)+∞))
104 fco2 6021 . . . 4 (((√ ↾ (0[,)+∞)):(0[,)+∞)⟶ℝ ∧ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)):ℝ⟶(0[,)+∞)) → (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))):ℝ⟶ℝ)
10576, 103, 104syl2anc 692 . . 3 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))):ℝ⟶ℝ)
106 rnco 5605 . . . 4 ran (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) = ran (√ ↾ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)))
107 ffn 6007 . . . . . . . 8 (√:ℂ⟶ℂ → √ Fn ℂ)
10856, 107ax-mp 5 . . . . . . 7 √ Fn ℂ
109 readdcl 9970 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
110109adantl 482 . . . . . . . . . 10 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
111 remulcl 9972 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
112111adantl 482 . . . . . . . . . . . 12 ((𝐹 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
113112, 1, 1, 50, 50, 102off 6872 . . . . . . . . . . 11 (𝐹 ∈ dom ∫1 → (𝐹𝑓 · 𝐹):ℝ⟶ℝ)
114113adantr 481 . . . . . . . . . 10 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (𝐹𝑓 · 𝐹):ℝ⟶ℝ)
115111adantl 482 . . . . . . . . . . . 12 ((𝐺 ∈ dom ∫1 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
116115, 3, 3, 30, 30, 102off 6872 . . . . . . . . . . 11 (𝐺 ∈ dom ∫1 → (𝐺𝑓 · 𝐺):ℝ⟶ℝ)
117116adantl 482 . . . . . . . . . 10 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (𝐺𝑓 · 𝐺):ℝ⟶ℝ)
118110, 114, 117, 24, 24, 102off 6872 . . . . . . . . 9 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)):ℝ⟶ℝ)
119 frn 6015 . . . . . . . . 9 (((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)):ℝ⟶ℝ → ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ⊆ ℝ)
120118, 119syl 17 . . . . . . . 8 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ⊆ ℝ)
121120, 71syl6ss 3599 . . . . . . 7 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ⊆ ℂ)
122 fnssres 5967 . . . . . . 7 ((√ Fn ℂ ∧ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ⊆ ℂ) → (√ ↾ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) Fn ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)))
123108, 121, 122sylancr 694 . . . . . 6 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (√ ↾ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) Fn ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)))
124 id 22 . . . . . . . . . 10 (𝐹 ∈ dom ∫1𝐹 ∈ dom ∫1)
125124, 124i1fmul 23382 . . . . . . . . 9 (𝐹 ∈ dom ∫1 → (𝐹𝑓 · 𝐹) ∈ dom ∫1)
126125adantr 481 . . . . . . . 8 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (𝐹𝑓 · 𝐹) ∈ dom ∫1)
127 id 22 . . . . . . . . . 10 (𝐺 ∈ dom ∫1𝐺 ∈ dom ∫1)
128127, 127i1fmul 23382 . . . . . . . . 9 (𝐺 ∈ dom ∫1 → (𝐺𝑓 · 𝐺) ∈ dom ∫1)
129128adantl 482 . . . . . . . 8 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (𝐺𝑓 · 𝐺) ∈ dom ∫1)
130126, 129i1fadd 23381 . . . . . . 7 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∈ dom ∫1)
131 i1frn 23363 . . . . . . 7 (((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∈ dom ∫1 → ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∈ Fin)
132130, 131syl 17 . . . . . 6 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∈ Fin)
133 fnfi 8189 . . . . . 6 (((√ ↾ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) Fn ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∧ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∈ Fin) → (√ ↾ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∈ Fin)
134123, 132, 133syl2anc 692 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (√ ↾ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∈ Fin)
135 rnfi 8200 . . . . 5 ((√ ↾ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∈ Fin → ran (√ ↾ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∈ Fin)
136134, 135syl 17 . . . 4 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ran (√ ↾ ran ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∈ Fin)
137106, 136syl5eqel 2702 . . 3 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ran (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∈ Fin)
138 cnvco 5273 . . . . . . 7 (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) = (((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∘ √)
139138imaeq1i 5427 . . . . . 6 ((√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) “ {𝑥}) = ((((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∘ √) “ {𝑥})
140 imaco 5604 . . . . . 6 ((((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∘ √) “ {𝑥}) = (((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) “ (√ “ {𝑥}))
141139, 140eqtri 2643 . . . . 5 ((√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) “ {𝑥}) = (((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) “ (√ “ {𝑥}))
142 i1fima 23364 . . . . . 6 (((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∈ dom ∫1 → (((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) “ (√ “ {𝑥})) ∈ dom vol)
143130, 142syl 17 . . . . 5 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) “ (√ “ {𝑥})) ∈ dom vol)
144141, 143syl5eqel 2702 . . . 4 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → ((√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) “ {𝑥}) ∈ dom vol)
145144adantr 481 . . 3 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ (ran (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∖ {0})) → ((√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) “ {𝑥}) ∈ dom vol)
146141fveq2i 6156 . . . 4 (vol‘((√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) “ {𝑥})) = (vol‘(((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) “ (√ “ {𝑥})))
147 eldifsni 4294 . . . . . . . 8 (𝑥 ∈ (ran (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∖ {0}) → 𝑥 ≠ 0)
148 c0ex 9985 . . . . . . . . . . . 12 0 ∈ V
149148elsn 4168 . . . . . . . . . . 11 (0 ∈ {𝑥} ↔ 0 = 𝑥)
150 eqcom 2628 . . . . . . . . . . 11 (0 = 𝑥𝑥 = 0)
151149, 150bitri 264 . . . . . . . . . 10 (0 ∈ {𝑥} ↔ 𝑥 = 0)
152151necon3bbii 2837 . . . . . . . . 9 (¬ 0 ∈ {𝑥} ↔ 𝑥 ≠ 0)
153 sqrt0 13923 . . . . . . . . . 10 (√‘0) = 0
154153eleq1i 2689 . . . . . . . . 9 ((√‘0) ∈ {𝑥} ↔ 0 ∈ {𝑥})
155152, 154xchnxbir 323 . . . . . . . 8 (¬ (√‘0) ∈ {𝑥} ↔ 𝑥 ≠ 0)
156147, 155sylibr 224 . . . . . . 7 (𝑥 ∈ (ran (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∖ {0}) → ¬ (√‘0) ∈ {𝑥})
157156olcd 408 . . . . . 6 (𝑥 ∈ (ran (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∖ {0}) → (¬ 0 ∈ ℂ ∨ ¬ (√‘0) ∈ {𝑥}))
158 ianor 509 . . . . . . 7 (¬ (0 ∈ ℂ ∧ (√‘0) ∈ {𝑥}) ↔ (¬ 0 ∈ ℂ ∨ ¬ (√‘0) ∈ {𝑥}))
159 elpreima 6298 . . . . . . . 8 (√ Fn ℂ → (0 ∈ (√ “ {𝑥}) ↔ (0 ∈ ℂ ∧ (√‘0) ∈ {𝑥})))
16056, 107, 159mp2b 10 . . . . . . 7 (0 ∈ (√ “ {𝑥}) ↔ (0 ∈ ℂ ∧ (√‘0) ∈ {𝑥}))
161158, 160xchnxbir 323 . . . . . 6 (¬ 0 ∈ (√ “ {𝑥}) ↔ (¬ 0 ∈ ℂ ∨ ¬ (√‘0) ∈ {𝑥}))
162157, 161sylibr 224 . . . . 5 (𝑥 ∈ (ran (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∖ {0}) → ¬ 0 ∈ (√ “ {𝑥}))
163 i1fima2 23365 . . . . 5 ((((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) ∈ dom ∫1 ∧ ¬ 0 ∈ (√ “ {𝑥})) → (vol‘(((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) “ (√ “ {𝑥}))) ∈ ℝ)
164130, 162, 163syl2an 494 . . . 4 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ (ran (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∖ {0})) → (vol‘(((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺)) “ (√ “ {𝑥}))) ∈ ℝ)
165146, 164syl5eqel 2702 . . 3 (((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) ∧ 𝑥 ∈ (ran (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∖ {0})) → (vol‘((√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) “ {𝑥})) ∈ ℝ)
166105, 137, 145, 165i1fd 23367 . 2 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (√ ∘ ((𝐹𝑓 · 𝐹) ∘𝑓 + (𝐺𝑓 · 𝐺))) ∈ dom ∫1)
16761, 166eqeltrd 2698 1 ((𝐹 ∈ dom ∫1𝐺 ∈ dom ∫1) → (abs ∘ (𝐹𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺))) ∈ dom ∫1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  wne 2790  Vcvv 3189  cdif 3556  wss 3559  {csn 4153   class class class wbr 4618  cmpt 4678   × cxp 5077  ccnv 5078  dom cdm 5079  ran crn 5080  cres 5081  cima 5082  ccom 5083   Fn wfn 5847  wf 5848  cfv 5852  (class class class)co 6610  𝑓 cof 6855  Fincfn 7906  cc 9885  cr 9886  0cc0 9887  ici 9889   + caddc 9890   · cmul 9892  +∞cpnf 10022  cle 10026  2c2 11021  [,)cico 12126  cexp 12807  csqrt 13914  abscabs 13915  volcvol 23151  1citg1 23303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-n0 11244  df-z 11329  df-uz 11639  df-q 11740  df-rp 11784  df-xadd 11898  df-ioo 12128  df-ico 12130  df-icc 12131  df-fz 12276  df-fzo 12414  df-fl 12540  df-seq 12749  df-exp 12808  df-hash 13065  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-clim 14160  df-sum 14358  df-xmet 19667  df-met 19668  df-ovol 23152  df-vol 23153  df-mbf 23307  df-itg1 23308
This theorem is referenced by:  ftc1anclem7  33150  ftc1anclem8  33151
  Copyright terms: Public domain W3C validator