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 dom 1 G dom 1 abs F + f × i × f G dom 1

Proof

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