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 
|- ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( abs o. ( F oF + ( ( RR X. { _i } ) oF x. G ) ) ) e. dom S.1 )

Proof

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