Metamath Proof Explorer

Theorem itgsubsticclem

Description: lemma for itgsubsticc . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgsubsticclem.1 ⊢ F = u ∈ K L ⟼ C
itgsubsticclem.2 ⊢ G = u ∈ ℝ ⟼ if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L
itgsubsticclem.3 ⊢ φ → X ∈ ℝ
itgsubsticclem.4 ⊢ φ → Y ∈ ℝ
itgsubsticclem.5 ⊢ φ → X ≤ Y
itgsubsticclem.6 ⊢ φ → x ∈ X Y ⟼ A : X Y ⟶cn K L
itgsubsticclem.7 ⊢ φ → x ∈ X Y ⟼ B ∈ X Y ⟶cn ℂ ∩ 𝐿 1
itgsubsticclem.8 ⊢ φ → F : K L ⟶cn ℂ
itgsubsticclem.9 ⊢ φ → K ∈ ℝ
itgsubsticclem.10 ⊢ φ → L ∈ ℝ
itgsubsticclem.11 ⊢ φ → K ≤ L
itgsubsticclem.12 ⊢ φ → dx ∈ X Y A d ℝ x = x ∈ X Y ⟼ B
itgsubsticclem.13 ⊢ u = A → C = E
itgsubsticclem.14 ⊢ x = X → A = K
itgsubsticclem.15 ⊢ x = Y → A = L
Assertion itgsubsticclem ⊢ φ → ∫ K L C du = ∫ X Y E ⁢ B dx

Proof

Step Hyp Ref Expression
1 itgsubsticclem.1 ⊢ F = u ∈ K L ⟼ C
2 itgsubsticclem.2 ⊢ G = u ∈ ℝ ⟼ if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L
3 itgsubsticclem.3 ⊢ φ → X ∈ ℝ
4 itgsubsticclem.4 ⊢ φ → Y ∈ ℝ
5 itgsubsticclem.5 ⊢ φ → X ≤ Y
6 itgsubsticclem.6 ⊢ φ → x ∈ X Y ⟼ A : X Y ⟶cn K L
7 itgsubsticclem.7 ⊢ φ → x ∈ X Y ⟼ B ∈ X Y ⟶cn ℂ ∩ 𝐿 1
8 itgsubsticclem.8 ⊢ φ → F : K L ⟶cn ℂ
9 itgsubsticclem.9 ⊢ φ → K ∈ ℝ
10 itgsubsticclem.10 ⊢ φ → L ∈ ℝ
11 itgsubsticclem.11 ⊢ φ → K ≤ L
12 itgsubsticclem.12 ⊢ φ → dx ∈ X Y A d ℝ x = x ∈ X Y ⟼ B
13 itgsubsticclem.13 ⊢ u = A → C = E
14 itgsubsticclem.14 ⊢ x = X → A = K
15 itgsubsticclem.15 ⊢ x = Y → A = L
16 fveq2 ⊢ u = w → G ⁡ u = G ⁡ w
17 nfcv ⊢ Ⅎ _ w G ⁡ u
18 nfmpt1 ⊢ Ⅎ _ u u ∈ ℝ ⟼ if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L
19 2 18 nfcxfr ⊢ Ⅎ _ u G
20 nfcv ⊢ Ⅎ _ u w
21 19 20 nffv ⊢ Ⅎ _ u G ⁡ w
22 16 17 21 cbvditg ⊢ ∫ K L G ⁡ u du = ∫ K L G ⁡ w dw
23 9 10 iccssred ⊢ φ → K L ⊆ ℝ
24 23 adantr ⊢ φ ∧ u ∈ K L → K L ⊆ ℝ
25 ioossicc ⊢ K L ⊆ K L
26 25 sseli ⊢ u ∈ K L → u ∈ K L
27 26 adantl ⊢ φ ∧ u ∈ K L → u ∈ K L
28 24 27 sseldd ⊢ φ ∧ u ∈ K L → u ∈ ℝ
29 27 iftrued ⊢ φ ∧ u ∈ K L → if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L = F ⁡ u
30 1 a1i ⊢ φ → F = u ∈ K L ⟼ C
31 cncff ⊢ F : K L ⟶cn ℂ → F : K L ⟶ ℂ
32 8 31 syl ⊢ φ → F : K L ⟶ ℂ
33 30 32 feq1dd ⊢ φ → u ∈ K L ⟼ C : K L ⟶ ℂ
34 33 fvmptelrn ⊢ φ ∧ u ∈ K L → C ∈ ℂ
35 27 34 syldan ⊢ φ ∧ u ∈ K L → C ∈ ℂ
36 1 fvmpt2 ⊢ u ∈ K L ∧ C ∈ ℂ → F ⁡ u = C
37 27 35 36 syl2anc ⊢ φ ∧ u ∈ K L → F ⁡ u = C
38 37 35 eqeltrd ⊢ φ ∧ u ∈ K L → F ⁡ u ∈ ℂ
39 29 38 eqeltrd ⊢ φ ∧ u ∈ K L → if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L ∈ ℂ
40 2 fvmpt2 ⊢ u ∈ ℝ ∧ if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L ∈ ℂ → G ⁡ u = if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L
41 28 39 40 syl2anc ⊢ φ ∧ u ∈ K L → G ⁡ u = if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L
42 41 29 37 3eqtrd ⊢ φ ∧ u ∈ K L → G ⁡ u = C
43 11 42 ditgeq3d ⊢ φ → ∫ K L G ⁡ u du = ∫ K L C du
44 mnfxr ⊢ −∞ ∈ ℝ *
45 44 a1i ⊢ φ → −∞ ∈ ℝ *
46 pnfxr ⊢ +∞ ∈ ℝ *
47 46 a1i ⊢ φ → +∞ ∈ ℝ *
48 ioomax ⊢ −∞ +∞ = ℝ
49 48 eqcomi ⊢ ℝ = −∞ +∞
50 49 a1i ⊢ φ → ℝ = −∞ +∞
51 23 50 sseqtrd ⊢ φ → K L ⊆ −∞ +∞
52 ax-resscn ⊢ ℝ ⊆ ℂ
53 50 52 eqsstrrdi ⊢ φ → −∞ +∞ ⊆ ℂ
54 cncfss ⊢ K L ⊆ −∞ +∞ ∧ −∞ +∞ ⊆ ℂ → X Y ⟶cn K L ⊆ X Y ⟶cn −∞ +∞
55 51 53 54 syl2anc ⊢ φ → X Y ⟶cn K L ⊆ X Y ⟶cn −∞ +∞
56 55 6 sseldd ⊢ φ → x ∈ X Y ⟼ A : X Y ⟶cn −∞ +∞
57 nfmpt1 ⊢ Ⅎ _ u u ∈ K L ⟼ C
58 1 57 nfcxfr ⊢ Ⅎ _ u F
59 eqid ⊢ topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ .
60 eqid ⊢ ⋃ TopOpen ⁡ ℂ fld = ⋃ TopOpen ⁡ ℂ fld
61 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
62 61 cnfldtop ⊢ TopOpen ⁡ ℂ fld ∈ Top
63 62 a1i ⊢ φ → TopOpen ⁡ ℂ fld ∈ Top
64 23 52 sstrdi ⊢ φ → K L ⊆ ℂ
65 ssid ⊢ ℂ ⊆ ℂ
66 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 K L = TopOpen ⁡ ℂ fld ↾ 𝑡 K L
67 unicntop ⊢ ℂ = ⋃ TopOpen ⁡ ℂ fld
68 67 restid ⊢ TopOpen ⁡ ℂ fld ∈ Top → TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ = TopOpen ⁡ ℂ fld
69 62 68 ax-mp ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ = TopOpen ⁡ ℂ fld
70 69 eqcomi ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
71 61 66 70 cncfcn ⊢ K L ⊆ ℂ ∧ ℂ ⊆ ℂ → K L ⟶cn ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 K L Cn TopOpen ⁡ ℂ fld
72 64 65 71 sylancl ⊢ φ → K L ⟶cn ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 K L Cn TopOpen ⁡ ℂ fld
73 reex ⊢ ℝ ∈ V
74 73 a1i ⊢ φ → ℝ ∈ V
75 restabs ⊢ TopOpen ⁡ ℂ fld ∈ Top ∧ K L ⊆ ℝ ∧ ℝ ∈ V → TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ↾ 𝑡 K L = TopOpen ⁡ ℂ fld ↾ 𝑡 K L
76 63 23 74 75 syl3anc ⊢ φ → TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ↾ 𝑡 K L = TopOpen ⁡ ℂ fld ↾ 𝑡 K L
77 61 tgioo2 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
78 77 eqcomi ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ = topGen ⁡ ran ⁡ .
79 78 a1i ⊢ φ → TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ = topGen ⁡ ran ⁡ .
80 79 oveq1d ⊢ φ → TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ↾ 𝑡 K L = topGen ⁡ ran ⁡ . ↾ 𝑡 K L
81 76 80 eqtr3d ⊢ φ → TopOpen ⁡ ℂ fld ↾ 𝑡 K L = topGen ⁡ ran ⁡ . ↾ 𝑡 K L
82 81 oveq1d ⊢ φ → TopOpen ⁡ ℂ fld ↾ 𝑡 K L Cn TopOpen ⁡ ℂ fld = topGen ⁡ ran ⁡ . ↾ 𝑡 K L Cn TopOpen ⁡ ℂ fld
83 72 82 eqtrd ⊢ φ → K L ⟶cn ℂ = topGen ⁡ ran ⁡ . ↾ 𝑡 K L Cn TopOpen ⁡ ℂ fld
84 8 83 eleqtrd ⊢ φ → F ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 K L Cn TopOpen ⁡ ℂ fld
85 58 59 60 2 9 10 11 63 84 icccncfext ⊢ φ → G ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F ∧ G ↾ K L = F
86 85 simpld ⊢ φ → G ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F
87 uniretop ⊢ ℝ = ⋃ topGen ⁡ ran ⁡ .
88 eqid ⊢ ⋃ TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F = ⋃ TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F
89 87 88 cnf ⊢ G ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F → G : ℝ ⟶ ⋃ TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F
90 86 89 syl ⊢ φ → G : ℝ ⟶ ⋃ TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F
91 50 feq2d ⊢ φ → G : ℝ ⟶ ⋃ TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F ↔ G : −∞ +∞ ⟶ ⋃ TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F
92 90 91 mpbid ⊢ φ → G : −∞ +∞ ⟶ ⋃ TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F
93 92 feqmptd ⊢ φ → G = w ∈ −∞ +∞ ⟼ G ⁡ w
94 32 frnd ⊢ φ → ran ⁡ F ⊆ ℂ
95 cncfss ⊢ ran ⁡ F ⊆ ℂ ∧ ℂ ⊆ ℂ → −∞ +∞ ⟶cn ran ⁡ F ⊆ −∞ +∞ ⟶cn ℂ
96 94 65 95 sylancl ⊢ φ → −∞ +∞ ⟶cn ran ⁡ F ⊆ −∞ +∞ ⟶cn ℂ
97 49 oveq2i ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ = TopOpen ⁡ ℂ fld ↾ 𝑡 −∞ +∞
98 77 97 eqtri ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 −∞ +∞
99 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F = TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F
100 61 98 99 cncfcn ⊢ −∞ +∞ ⊆ ℂ ∧ ran ⁡ F ⊆ ℂ → −∞ +∞ ⟶cn ran ⁡ F = topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F
101 53 94 100 syl2anc ⊢ φ → −∞ +∞ ⟶cn ran ⁡ F = topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F
102 101 eqcomd ⊢ φ → topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ran ⁡ F = −∞ +∞ ⟶cn ran ⁡ F
103 86 102 eleqtrd ⊢ φ → G : −∞ +∞ ⟶cn ran ⁡ F
104 96 103 sseldd ⊢ φ → G : −∞ +∞ ⟶cn ℂ
105 93 104 eqeltrrd ⊢ φ → w ∈ −∞ +∞ ⟼ G ⁡ w : −∞ +∞ ⟶cn ℂ
106 fveq2 ⊢ w = A → G ⁡ w = G ⁡ A
107 3 4 5 45 47 56 7 105 12 106 14 15 itgsubst ⊢ φ → ∫ K L G ⁡ w dw = ∫ X Y G ⁡ A ⁢ B dx
108 22 43 107 3eqtr3a ⊢ φ → ∫ K L C du = ∫ X Y G ⁡ A ⁢ B dx
109 2 a1i ⊢ φ ∧ x ∈ X Y → G = u ∈ ℝ ⟼ if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L
110 simpr ⊢ φ ∧ x ∈ X Y ∧ u = A → u = A
111 61 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
112 3 4 iccssred ⊢ φ → X Y ⊆ ℝ
113 112 52 sstrdi ⊢ φ → X Y ⊆ ℂ
114 resttopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ X Y ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 X Y ∈ TopOn ⁡ X Y
115 111 113 114 sylancr ⊢ φ → TopOpen ⁡ ℂ fld ↾ 𝑡 X Y ∈ TopOn ⁡ X Y
116 resttopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ K L ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 K L ∈ TopOn ⁡ K L
117 111 64 116 sylancr ⊢ φ → TopOpen ⁡ ℂ fld ↾ 𝑡 K L ∈ TopOn ⁡ K L
118 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 X Y = TopOpen ⁡ ℂ fld ↾ 𝑡 X Y
119 61 118 66 cncfcn ⊢ X Y ⊆ ℂ ∧ K L ⊆ ℂ → X Y ⟶cn K L = TopOpen ⁡ ℂ fld ↾ 𝑡 X Y Cn TopOpen ⁡ ℂ fld ↾ 𝑡 K L
120 113 64 119 syl2anc ⊢ φ → X Y ⟶cn K L = TopOpen ⁡ ℂ fld ↾ 𝑡 X Y Cn TopOpen ⁡ ℂ fld ↾ 𝑡 K L
121 6 120 eleqtrd ⊢ φ → x ∈ X Y ⟼ A ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 X Y Cn TopOpen ⁡ ℂ fld ↾ 𝑡 K L
122 cnf2 ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 X Y ∈ TopOn ⁡ X Y ∧ TopOpen ⁡ ℂ fld ↾ 𝑡 K L ∈ TopOn ⁡ K L ∧ x ∈ X Y ⟼ A ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 X Y Cn TopOpen ⁡ ℂ fld ↾ 𝑡 K L → x ∈ X Y ⟼ A : X Y ⟶ K L
123 115 117 121 122 syl3anc ⊢ φ → x ∈ X Y ⟼ A : X Y ⟶ K L
124 123 adantr ⊢ φ ∧ x ∈ X Y → x ∈ X Y ⟼ A : X Y ⟶ K L
125 eqid ⊢ x ∈ X Y ⟼ A = x ∈ X Y ⟼ A
126 125 fmpt ⊢ ∀ x ∈ X Y A ∈ K L ↔ x ∈ X Y ⟼ A : X Y ⟶ K L
127 124 126 sylibr ⊢ φ ∧ x ∈ X Y → ∀ x ∈ X Y A ∈ K L
128 ioossicc ⊢ X Y ⊆ X Y
129 128 sseli ⊢ x ∈ X Y → x ∈ X Y
130 129 adantl ⊢ φ ∧ x ∈ X Y → x ∈ X Y
131 rsp ⊢ ∀ x ∈ X Y A ∈ K L → x ∈ X Y → A ∈ K L
132 127 130 131 sylc ⊢ φ ∧ x ∈ X Y → A ∈ K L
133 132 adantr ⊢ φ ∧ x ∈ X Y ∧ u = A → A ∈ K L
134 110 133 eqeltrd ⊢ φ ∧ x ∈ X Y ∧ u = A → u ∈ K L
135 134 iftrued ⊢ φ ∧ x ∈ X Y ∧ u = A → if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L = F ⁡ u
136 simpll ⊢ φ ∧ x ∈ X Y ∧ u = A → φ
137 136 134 34 syl2anc ⊢ φ ∧ x ∈ X Y ∧ u = A → C ∈ ℂ
138 134 137 36 syl2anc ⊢ φ ∧ x ∈ X Y ∧ u = A → F ⁡ u = C
139 13 adantl ⊢ φ ∧ x ∈ X Y ∧ u = A → C = E
140 135 138 139 3eqtrd ⊢ φ ∧ x ∈ X Y ∧ u = A → if u ∈ K L F ⁡ u if u < K F ⁡ K F ⁡ L = E
141 23 adantr ⊢ φ ∧ x ∈ X Y → K L ⊆ ℝ
142 141 132 sseldd ⊢ φ ∧ x ∈ X Y → A ∈ ℝ
143 elex ⊢ A ∈ K L → A ∈ V
144 132 143 syl ⊢ φ ∧ x ∈ X Y → A ∈ V
145 isset ⊢ A ∈ V ↔ ∃ u u = A
146 144 145 sylib ⊢ φ ∧ x ∈ X Y → ∃ u u = A
147 139 137 eqeltrrd ⊢ φ ∧ x ∈ X Y ∧ u = A → E ∈ ℂ
148 146 147 exlimddv ⊢ φ ∧ x ∈ X Y → E ∈ ℂ
149 109 140 142 148 fvmptd ⊢ φ ∧ x ∈ X Y → G ⁡ A = E
150 149 oveq1d ⊢ φ ∧ x ∈ X Y → G ⁡ A ⁢ B = E ⁢ B
151 5 150 ditgeq3d ⊢ φ → ∫ X Y G ⁡ A ⁢ B dx = ∫ X Y E ⁢ B dx
152 108 151 eqtrd ⊢ φ → ∫ K L C du = ∫ X Y E ⁢ B dx