Metamath Proof Explorer

Theorem ftc1anclem3

Description: Lemma for ftc1anc - 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)

Ref Expression
Assertion ftc1anclem3 ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( abs ∘ ( 𝐹 ∘f + ( ( ℝ × { i } ) ∘f · 𝐺 ) ) ) ∈ dom ∫1 )

Proof

Step Hyp Ref Expression
1 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
2 1 ffvelrnda ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
3 i1ff ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
4 3 ffvelrnda ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
5 absreim ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℝ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ) = ( √ ‘ ( ( ( 𝐹 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ) ) )
6 2 4 5 syl2an ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ) = ( √ ‘ ( ( ( 𝐹 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ) ) )
7 6 anandirs ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ) = ( √ ‘ ( ( ( 𝐹 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ) ) )
8 2 recnd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
9 8 sqvald ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ↑ 2 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) )
10 4 recnd ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
11 10 sqvald ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) = ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
12 9 11 oveqan12d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
13 12 anandirs ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
14 13 fveq2d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( √ ‘ ( ( ( 𝐹 ‘ 𝑥 ) ↑ 2 ) + ( ( 𝐺 ‘ 𝑥 ) ↑ 2 ) ) ) = ( √ ‘ ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) )
15 7 14 eqtrd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ) = ( √ ‘ ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) )
16 15 mpteq2dva ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( √ ‘ ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
17 ax-icn ⊢ i ∈ ℂ
18 mulcl ⊢ ( ( i ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℂ ) → ( i · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
19 17 10 18 sylancr ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( i · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
20 addcl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℂ ∧ ( i · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ ) → ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℂ )
21 8 19 20 syl2an ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℂ )
22 21 anandirs ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℂ )
23 reex ⊢ ℝ ∈ V
24 23 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ℝ ∈ V )
25 2 adantlr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
26 ovexd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( i · ( 𝐺 ‘ 𝑥 ) ) ∈ V )
27 1 feqmptd ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
28 27 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
29 23 a1i ⊢ ( 𝐺 ∈ dom ∫1 → ℝ ∈ V )
30 17 a1i ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → i ∈ ℂ )
31 fconstmpt ⊢ ( ℝ × { i } ) = ( 𝑥 ∈ ℝ ↦ i )
32 31 a1i ⊢ ( 𝐺 ∈ dom ∫1 → ( ℝ × { i } ) = ( 𝑥 ∈ ℝ ↦ i ) )
33 3 feqmptd ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 = ( 𝑥 ∈ ℝ ↦ ( 𝐺 ‘ 𝑥 ) ) )
34 29 30 4 32 33 offval2 ⊢ ( 𝐺 ∈ dom ∫1 → ( ( ℝ × { i } ) ∘f · 𝐺 ) = ( 𝑥 ∈ ℝ ↦ ( i · ( 𝐺 ‘ 𝑥 ) ) ) )
35 34 adantl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( ℝ × { i } ) ∘f · 𝐺 ) = ( 𝑥 ∈ ℝ ↦ ( i · ( 𝐺 ‘ 𝑥 ) ) ) )
36 24 25 26 28 35 offval2 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f + ( ( ℝ × { i } ) ∘f · 𝐺 ) ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ) )
37 absf ⊢ abs : ℂ ⟶ ℝ
38 37 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → abs : ℂ ⟶ ℝ )
39 38 feqmptd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → abs = ( 𝑦 ∈ ℂ ↦ ( abs ‘ 𝑦 ) ) )
40 fveq2 ⊢ ( 𝑦 = ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) → ( abs ‘ 𝑦 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ) )
41 22 36 39 40 fmptco ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( abs ∘ ( 𝐹 ∘f + ( ( ℝ × { i } ) ∘f · 𝐺 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) + ( i · ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
42 8 8 mulcld ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
43 10 10 mulcld ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
44 addcl ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ ∧ ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ ) → ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℂ )
45 42 43 44 syl2an ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐺 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) ) → ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℂ )
46 45 anandirs ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℂ )
47 42 adantlr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
48 43 adantll ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
49 23 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ℝ ∈ V )
50 49 2 2 27 27 offval2 ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝐹 ∘f · 𝐹 ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) )
51 50 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f · 𝐹 ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) )
52 29 4 4 33 33 offval2 ⊢ ( 𝐺 ∈ dom ∫1 → ( 𝐺 ∘f · 𝐺 ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
53 52 adantl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐺 ∘f · 𝐺 ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
54 24 47 48 51 53 offval2 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) = ( 𝑥 ∈ ℝ ↦ ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) )
55 sqrtf ⊢ √ : ℂ ⟶ ℂ
56 55 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → √ : ℂ ⟶ ℂ )
57 56 feqmptd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → √ = ( 𝑦 ∈ ℂ ↦ ( √ ‘ 𝑦 ) ) )
58 fveq2 ⊢ ( 𝑦 = ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) → ( √ ‘ 𝑦 ) = ( √ ‘ ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) )
59 46 54 57 58 fmptco ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( √ ‘ ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) + ( ( 𝐺 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
60 16 41 59 3eqtr4d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( abs ∘ ( 𝐹 ∘f + ( ( ℝ × { i } ) ∘f · 𝐺 ) ) ) = ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) )
61 elrege0 ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
62 resqrtcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( √ ‘ 𝑥 ) ∈ ℝ )
63 61 62 sylbi ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → ( √ ‘ 𝑥 ) ∈ ℝ )
64 63 adantl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ( 0 [,) +∞ ) ) → ( √ ‘ 𝑥 ) ∈ ℝ )
65 id ⊢ ( √ : ℂ ⟶ ℂ → √ : ℂ ⟶ ℂ )
66 65 feqmptd ⊢ ( √ : ℂ ⟶ ℂ → √ = ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) )
67 55 66 ax-mp ⊢ √ = ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) )
68 67 reseq1i ⊢ ( √ ↾ ( 0 [,) +∞ ) ) = ( ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) ↾ ( 0 [,) +∞ ) )
69 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
70 ax-resscn ⊢ ℝ ⊆ ℂ
71 69 70 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
72 resmpt ⊢ ( ( 0 [,) +∞ ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) ↾ ( 0 [,) +∞ ) ) = ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) )
73 71 72 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) ↾ ( 0 [,) +∞ ) ) = ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) )
74 68 73 eqtri ⊢ ( √ ↾ ( 0 [,) +∞ ) ) = ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) )
75 64 74 fmptd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( √ ↾ ( 0 [,) +∞ ) ) : ( 0 [,) +∞ ) ⟶ ℝ )
76 ge0addcl ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
77 76 adantl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
78 oveq12 ⊢ ( ( 𝑧 = 𝐹 ∧ 𝑧 = 𝐹 ) → ( 𝑧 ∘f · 𝑧 ) = ( 𝐹 ∘f · 𝐹 ) )
79 78 anidms ⊢ ( 𝑧 = 𝐹 → ( 𝑧 ∘f · 𝑧 ) = ( 𝐹 ∘f · 𝐹 ) )
80 79 feq1d ⊢ ( 𝑧 = 𝐹 → ( ( 𝑧 ∘f · 𝑧 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐹 ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,) +∞ ) ) )
81 i1ff ⊢ ( 𝑧 ∈ dom ∫1 → 𝑧 : ℝ ⟶ ℝ )
82 81 ffvelrnda ⊢ ( ( 𝑧 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝑧 ‘ 𝑥 ) ∈ ℝ )
83 82 82 remulcld ⊢ ( ( 𝑧 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑧 ‘ 𝑥 ) · ( 𝑧 ‘ 𝑥 ) ) ∈ ℝ )
84 82 msqge0d ⊢ ( ( 𝑧 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( 𝑧 ‘ 𝑥 ) · ( 𝑧 ‘ 𝑥 ) ) )
85 elrege0 ⊢ ( ( ( 𝑧 ‘ 𝑥 ) · ( 𝑧 ‘ 𝑥 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 𝑧 ‘ 𝑥 ) · ( 𝑧 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑧 ‘ 𝑥 ) · ( 𝑧 ‘ 𝑥 ) ) ) )
86 83 84 85 sylanbrc ⊢ ( ( 𝑧 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑧 ‘ 𝑥 ) · ( 𝑧 ‘ 𝑥 ) ) ∈ ( 0 [,) +∞ ) )
87 86 fmpttd ⊢ ( 𝑧 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( ( 𝑧 ‘ 𝑥 ) · ( 𝑧 ‘ 𝑥 ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
88 23 a1i ⊢ ( 𝑧 ∈ dom ∫1 → ℝ ∈ V )
89 81 feqmptd ⊢ ( 𝑧 ∈ dom ∫1 → 𝑧 = ( 𝑥 ∈ ℝ ↦ ( 𝑧 ‘ 𝑥 ) ) )
90 88 82 82 89 89 offval2 ⊢ ( 𝑧 ∈ dom ∫1 → ( 𝑧 ∘f · 𝑧 ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝑧 ‘ 𝑥 ) · ( 𝑧 ‘ 𝑥 ) ) ) )
91 90 feq1d ⊢ ( 𝑧 ∈ dom ∫1 → ( ( 𝑧 ∘f · 𝑧 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ↦ ( ( 𝑧 ‘ 𝑥 ) · ( 𝑧 ‘ 𝑥 ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) ) )
92 87 91 mpbird ⊢ ( 𝑧 ∈ dom ∫1 → ( 𝑧 ∘f · 𝑧 ) : ℝ ⟶ ( 0 [,) +∞ ) )
93 80 92 vtoclga ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝐹 ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,) +∞ ) )
94 93 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,) +∞ ) )
95 oveq12 ⊢ ( ( 𝑧 = 𝐺 ∧ 𝑧 = 𝐺 ) → ( 𝑧 ∘f · 𝑧 ) = ( 𝐺 ∘f · 𝐺 ) )
96 95 anidms ⊢ ( 𝑧 = 𝐺 → ( 𝑧 ∘f · 𝑧 ) = ( 𝐺 ∘f · 𝐺 ) )
97 96 feq1d ⊢ ( 𝑧 = 𝐺 → ( ( 𝑧 ∘f · 𝑧 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐺 ∘f · 𝐺 ) : ℝ ⟶ ( 0 [,) +∞ ) ) )
98 97 92 vtoclga ⊢ ( 𝐺 ∈ dom ∫1 → ( 𝐺 ∘f · 𝐺 ) : ℝ ⟶ ( 0 [,) +∞ ) )
99 98 adantl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐺 ∘f · 𝐺 ) : ℝ ⟶ ( 0 [,) +∞ ) )
100 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
101 77 94 99 24 24 100 off ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
102 fco2 ⊢ ( ( ( √ ↾ ( 0 [,) +∞ ) ) : ( 0 [,) +∞ ) ⟶ ℝ ∧ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) : ℝ ⟶ ( 0 [,) +∞ ) ) → ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) : ℝ ⟶ ℝ )
103 75 101 102 syl2anc ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) : ℝ ⟶ ℝ )
104 rnco ⊢ ran ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) = ran ( √ ↾ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) )
105 ffn ⊢ ( √ : ℂ ⟶ ℂ → √ Fn ℂ )
106 55 105 ax-mp ⊢ √ Fn ℂ
107 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
108 107 adantl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
109 remulcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
110 109 adantl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
111 110 1 1 49 49 100 off ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝐹 ∘f · 𝐹 ) : ℝ ⟶ ℝ )
112 111 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f · 𝐹 ) : ℝ ⟶ ℝ )
113 109 adantl ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
114 113 3 3 29 29 100 off ⊢ ( 𝐺 ∈ dom ∫1 → ( 𝐺 ∘f · 𝐺 ) : ℝ ⟶ ℝ )
115 114 adantl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐺 ∘f · 𝐺 ) : ℝ ⟶ ℝ )
116 108 112 115 24 24 100 off ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) : ℝ ⟶ ℝ )
117 116 frnd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ⊆ ℝ )
118 117 70 sstrdi ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ⊆ ℂ )
119 fnssres ⊢ ( ( √ Fn ℂ ∧ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ⊆ ℂ ) → ( √ ↾ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) Fn ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) )
120 106 118 119 sylancr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( √ ↾ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) Fn ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) )
121 id ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ dom ∫1 )
122 121 121 i1fmul ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝐹 ∘f · 𝐹 ) ∈ dom ∫1 )
123 122 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f · 𝐹 ) ∈ dom ∫1 )
124 id ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 ∈ dom ∫1 )
125 124 124 i1fmul ⊢ ( 𝐺 ∈ dom ∫1 → ( 𝐺 ∘f · 𝐺 ) ∈ dom ∫1 )
126 125 adantl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐺 ∘f · 𝐺 ) ∈ dom ∫1 )
127 123 126 i1fadd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∈ dom ∫1 )
128 i1frn ⊢ ( ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∈ dom ∫1 → ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∈ Fin )
129 127 128 syl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∈ Fin )
130 fnfi ⊢ ( ( ( √ ↾ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) Fn ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∧ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∈ Fin ) → ( √ ↾ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∈ Fin )
131 120 129 130 syl2anc ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( √ ↾ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∈ Fin )
132 rnfi ⊢ ( ( √ ↾ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∈ Fin → ran ( √ ↾ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∈ Fin )
133 131 132 syl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ran ( √ ↾ ran ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∈ Fin )
134 104 133 eqeltrid ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ran ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∈ Fin )
135 cnvco ⊢ ◡ ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) = ( ◡ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∘ ◡ √ )
136 135 imaeq1i ⊢ ( ◡ ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) “ { 𝑥 } ) = ( ( ◡ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∘ ◡ √ ) “ { 𝑥 } )
137 imaco ⊢ ( ( ◡ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∘ ◡ √ ) “ { 𝑥 } ) = ( ◡ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) “ ( ◡ √ “ { 𝑥 } ) )
138 136 137 eqtri ⊢ ( ◡ ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) “ { 𝑥 } ) = ( ◡ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) “ ( ◡ √ “ { 𝑥 } ) )
139 i1fima ⊢ ( ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∈ dom ∫1 → ( ◡ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) “ ( ◡ √ “ { 𝑥 } ) ) ∈ dom vol )
140 127 139 syl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ◡ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) “ ( ◡ √ “ { 𝑥 } ) ) ∈ dom vol )
141 138 140 eqeltrid ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ◡ ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) “ { 𝑥 } ) ∈ dom vol )
142 141 adantr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ( ran ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∖ { 0 } ) ) → ( ◡ ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) “ { 𝑥 } ) ∈ dom vol )
143 138 fveq2i ⊢ ( vol ‘ ( ◡ ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) “ { 𝑥 } ) ) = ( vol ‘ ( ◡ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) “ ( ◡ √ “ { 𝑥 } ) ) )
144 eldifsni ⊢ ( 𝑥 ∈ ( ran ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∖ { 0 } ) → 𝑥 ≠ 0 )
145 c0ex ⊢ 0 ∈ V
146 145 elsn ⊢ ( 0 ∈ { 𝑥 } ↔ 0 = 𝑥 )
147 eqcom ⊢ ( 0 = 𝑥 ↔ 𝑥 = 0 )
148 146 147 bitri ⊢ ( 0 ∈ { 𝑥 } ↔ 𝑥 = 0 )
149 148 necon3bbii ⊢ ( ¬ 0 ∈ { 𝑥 } ↔ 𝑥 ≠ 0 )
150 sqrt0 ⊢ ( √ ‘ 0 ) = 0
151 150 eleq1i ⊢ ( ( √ ‘ 0 ) ∈ { 𝑥 } ↔ 0 ∈ { 𝑥 } )
152 149 151 xchnxbir ⊢ ( ¬ ( √ ‘ 0 ) ∈ { 𝑥 } ↔ 𝑥 ≠ 0 )
153 144 152 sylibr ⊢ ( 𝑥 ∈ ( ran ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∖ { 0 } ) → ¬ ( √ ‘ 0 ) ∈ { 𝑥 } )
154 153 olcd ⊢ ( 𝑥 ∈ ( ran ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∖ { 0 } ) → ( ¬ 0 ∈ ℂ ∨ ¬ ( √ ‘ 0 ) ∈ { 𝑥 } ) )
155 ianor ⊢ ( ¬ ( 0 ∈ ℂ ∧ ( √ ‘ 0 ) ∈ { 𝑥 } ) ↔ ( ¬ 0 ∈ ℂ ∨ ¬ ( √ ‘ 0 ) ∈ { 𝑥 } ) )
156 elpreima ⊢ ( √ Fn ℂ → ( 0 ∈ ( ◡ √ “ { 𝑥 } ) ↔ ( 0 ∈ ℂ ∧ ( √ ‘ 0 ) ∈ { 𝑥 } ) ) )
157 55 105 156 mp2b ⊢ ( 0 ∈ ( ◡ √ “ { 𝑥 } ) ↔ ( 0 ∈ ℂ ∧ ( √ ‘ 0 ) ∈ { 𝑥 } ) )
158 155 157 xchnxbir ⊢ ( ¬ 0 ∈ ( ◡ √ “ { 𝑥 } ) ↔ ( ¬ 0 ∈ ℂ ∨ ¬ ( √ ‘ 0 ) ∈ { 𝑥 } ) )
159 154 158 sylibr ⊢ ( 𝑥 ∈ ( ran ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∖ { 0 } ) → ¬ 0 ∈ ( ◡ √ “ { 𝑥 } ) )
160 i1fima2 ⊢ ( ( ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ∈ dom ∫1 ∧ ¬ 0 ∈ ( ◡ √ “ { 𝑥 } ) ) → ( vol ‘ ( ◡ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) “ ( ◡ √ “ { 𝑥 } ) ) ) ∈ ℝ )
161 127 159 160 syl2an ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ( ran ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) “ ( ◡ √ “ { 𝑥 } ) ) ) ∈ ℝ )
162 143 161 eqeltrid ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ( ran ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) “ { 𝑥 } ) ) ∈ ℝ )
163 103 134 142 162 i1fd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( √ ∘ ( ( 𝐹 ∘f · 𝐹 ) ∘f + ( 𝐺 ∘f · 𝐺 ) ) ) ∈ dom ∫1 )
164 60 163 eqeltrd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( abs ∘ ( 𝐹 ∘f + ( ( ℝ × { i } ) ∘f · 𝐺 ) ) ) ∈ dom ∫1 )