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 \in dom \int^{1} \land G \in dom \int^{1}) \to abs \circ (F +_{f} ((ℝ \times \{i\}) \times_{f} G)) \in dom \int^{1}$

Proof

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

Metamath Proof Explorer

Theorem ftc1anclem3

Proof