P. 439 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43801-43900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	smfco 43801	The composition of a Borel sigma-measurable function with a sigma-measurable function, is sigma-measurable. Proposition 121E (g) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝐻 ∈ (SMblFn‘𝐵))    ⇒   ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ (SMblFn‘𝑆))
Theorem	smfneg 43802*	The negative of a sigma-measurable function is measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ (SMblFn‘𝑆))
Theorem	smffmpt 43803*	A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ)
Theorem	smflim2 43804*	The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). TODO: this has fewer distinct variable conditions than smflim 43777 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfpimcclem 43805*	Lemma for smfpimcc 43806 given the choice function 𝐶. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝜑    &   ⊢ 𝑍 ∈ 𝑉    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑛) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑛))})) → (𝐶‘𝑦) ∈ 𝑦)    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝐶‘{𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑛) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑛))}))    ⇒   ⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))))
Theorem	smfpimcc 43806*	Given a countable set of sigma-measurable functions, and a Borel set 𝐴 there exists a choice function ℎ that, for each measurable function, chooses a measurable set that, when intersected with the function's domain, gives the preimage of 𝐴. This is a generalization of the observation at the beginning of the proof of Proposition 121F of [Fremlin1] p. 39 . The statement would also be provable for uncountable sets, but in most cases it will suffice to consider the countable case, and only the axiom of countable choice will be needed. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))))
Theorem	issmfle2d 43807*	A sufficient condition for "𝐹 being a measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,]𝑎)) ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	smflimmpt 43808*	The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). 𝐴 can contain 𝑚 as a free variable, in other words it can be thought as an indexed collection 𝐴(𝑚). 𝐵 can be thought as a collection with two indices 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∣ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfsuplem1 43809*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐻:𝑍⟶𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((𝐻‘𝑛) ∩ dom (𝐹‘𝑛)))    ⇒   ⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷))
Theorem	smfsuplem2 43810*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷))
Theorem	smfsuplem3 43811*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfsup 43812*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfsupmpt 43813*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 𝐴 ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfsupxr 43814*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ*, < ) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ*, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfinflem 43815*	The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfinf 43816*	The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfinfmpt 43817*	The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 𝐴 ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smflimsuplem1 43818*	If 𝐻 converges, the lim sup of 𝐹 is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑍)    ⇒   ⊢ (𝜑 → dom (𝐻‘𝐾) ⊆ dom (𝐹‘𝐾))
Theorem	smflimsuplem2 43819*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )))    &   ⊢ (𝜑 → 𝑛 ∈ 𝑍)    &   ⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → 𝑋 ∈ dom (𝐻‘𝑛))
Theorem	smflimsuplem3 43820*	The limit of the (𝐻‘𝑛) functions is sigma-measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )))    ⇒   ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑛 ∈ (ℤ≥‘𝑘)dom (𝐻‘𝑛) ∣ (𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑥)))) ∈ (SMblFn‘𝑆))
Theorem	smflimsuplem4 43821*	If 𝐻 converges, the lim sup of 𝐹 is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )))    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑥 ∈ ∩ 𝑛 ∈ (ℤ≥‘𝑁)dom (𝐻‘𝑛))    &   ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑥)) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ)
Theorem	smflimsuplem5 43822*	𝐻 converges to the superior limit of 𝐹. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑚𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )))    &   ⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑁)dom (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘𝑁) ↦ ((𝐻‘𝑛)‘𝑋)) ⇝ (lim sup‘(𝑚 ∈ (ℤ≥‘𝑁) ↦ ((𝐹‘𝑚)‘𝑋))))
Theorem	smflimsuplem6 43823*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑚𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐸 = (𝑛 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑛) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑛) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )))    &   ⊢ (𝜑 → (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑁)dom (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ((𝐻‘𝑛)‘𝑋)) ∈ dom ⇝ )
Theorem	smflimsuplem7 43824*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}    &   ⊢ 𝐸 = (𝑘 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})    &   ⊢ 𝐻 = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )))    ⇒   ⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑘 ∈ (ℤ≥‘𝑛)dom (𝐻‘𝑘) ∣ (𝑘 ∈ 𝑍 ↦ ((𝐻‘𝑘)‘𝑥)) ∈ dom ⇝ })
Theorem	smflimsuplem8 43825*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ 𝐸 = (𝑘 ∈ 𝑍 ↦ {𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑘)dom (𝐹‘𝑚) ∣ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})    &   ⊢ 𝐻 = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ (𝐸‘𝑘) ↦ sup(ran (𝑚 ∈ (ℤ≥‘𝑘) ↦ ((𝐹‘𝑚)‘𝑥)), ℝ*, < )))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smflimsup 43826*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smflimsupmpt 43827*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . 𝐴 can contain 𝑚 as a free variable, in other words it can be thought of as an indexed collection 𝐴(𝑚). 𝐵 can be thought of as a collection with two indices 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfliminflem 43828*	The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfliminf 43829*	The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfliminfmpt 43830*	The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . 𝐴 can contain 𝑚 as a free variable, in other words it can be thought of as an indexed collection 𝐴(𝑚). 𝐵 can be thought of as a collection with two indices 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
20.38  Mathbox for Saveliy Skresanov
20.38.1  Ceva's theorem
Theorem	sigarval 43831*	Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = (ℑ‘((∗‘𝐴) · 𝐵)))
Theorem	sigarim 43832*	Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) ∈ ℝ)
Theorem	sigarac 43833*	Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = -(𝐵𝐺𝐴))
Theorem	sigaraf 43834*	Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶)𝐺𝐵) = ((𝐴𝐺𝐵) + (𝐶𝐺𝐵)))
Theorem	sigarmf 43835*	Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺𝐵) = ((𝐴𝐺𝐵) − (𝐶𝐺𝐵)))
Theorem	sigaras 43836*	Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 + 𝐶)) = ((𝐴𝐺𝐵) + (𝐴𝐺𝐶)))
Theorem	sigarms 43837*	Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 − 𝐶)) = ((𝐴𝐺𝐵) − (𝐴𝐺𝐶)))
Theorem	sigarls 43838*	Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ) → (𝐴𝐺(𝐵 · 𝐶)) = ((𝐴𝐺𝐵) · 𝐶))
Theorem	sigarid 43839*	Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ (𝐴 ∈ ℂ → (𝐴𝐺𝐴) = 0)
Theorem	sigarexp 43840*	Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = (((𝐴𝐺𝐵) − (𝐴𝐺𝐶)) − (𝐶𝐺𝐵)))
Theorem	sigarperm 43841*	Signed area (𝐴 − 𝐶)𝐺(𝐵 − 𝐶) acts as a double area of a triangle 𝐴𝐵𝐶. Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = ((𝐵 − 𝐴)𝐺(𝐶 − 𝐴)))
Theorem	sigardiv 43842*	If signed area between vectors 𝐵 − 𝐴 and 𝐶 − 𝐴 is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → ¬ 𝐶 = 𝐴)    &   ⊢ (𝜑 → ((𝐵 − 𝐴)𝐺(𝐶 − 𝐴)) = 0)    ⇒   ⊢ (𝜑 → ((𝐵 − 𝐴) / (𝐶 − 𝐴)) ∈ ℝ)
Theorem	sigarimcd 43843*	Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))    ⇒   ⊢ (𝜑 → (𝐴𝐺𝐵) ∈ ℂ)
Theorem	sigariz 43844*	If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))    &   ⊢ (𝜑 → (𝐴𝐺𝐵) = 0)    ⇒   ⊢ (𝜑 → (𝐵𝐺𝐴) = 0)
Theorem	sigarcol 43845*	Given three points 𝐴, 𝐵 and 𝐶 such that ¬ 𝐴 = 𝐵, the point 𝐶 lies on the line going through 𝐴 and 𝐵 iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = 0 ↔ ∃𝑡 ∈ ℝ 𝐶 = (𝐵 + (𝑡 · (𝐴 − 𝐵)))))
Theorem	sharhght 43846*	Let 𝐴𝐵𝐶 be a triangle, and let 𝐷 lie on the line 𝐴𝐵. Then (doubled) areas of triangles 𝐴𝐷𝐶 and 𝐶𝐷𝐵 relate as lengths of corresponding bases 𝐴𝐷 and 𝐷𝐵. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0))    ⇒   ⊢ (𝜑 → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷)))
Theorem	sigaradd 43847*	Subtracting (double) area of 𝐴𝐷𝐶 from 𝐴𝐵𝐶 yields the (double) area of 𝐷𝐵𝐶. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0))    ⇒   ⊢ (𝜑 → (((𝐵 − 𝐶)𝐺(𝐴 − 𝐶)) − ((𝐷 − 𝐶)𝐺(𝐴 − 𝐶))) = ((𝐵 − 𝐶)𝐺(𝐷 − 𝐶)))
Theorem	cevathlem1 43848	Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ))    &   ⊢ (𝜑 → (𝐺 ∈ ℂ ∧ 𝐻 ∈ ℂ ∧ 𝐾 ∈ ℂ))    &   ⊢ (𝜑 → (𝐴 ≠ 0 ∧ 𝐸 ≠ 0 ∧ 𝐶 ≠ 0))    &   ⊢ (𝜑 → ((𝐴 · 𝐵) = (𝐶 · 𝐷) ∧ (𝐸 · 𝐹) = (𝐴 · 𝐺) ∧ (𝐶 · 𝐻) = (𝐸 · 𝐾)))    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐹) · 𝐻) = ((𝐷 · 𝐺) · 𝐾))
Theorem	cevathlem2 43849*	Ceva's theorem second lemma. Relate (doubled) areas of triangles 𝐶𝐴𝑂 and 𝐴𝐵𝑂 with of segments 𝐵𝐷 and 𝐷𝐶. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ))    &   ⊢ (𝜑 → 𝑂 ∈ ℂ)    &   ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0))    &   ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0))    &   ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0))    ⇒   ⊢ (𝜑 → (((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) · (𝐵 − 𝐷)) = (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) · (𝐷 − 𝐶)))
Theorem	cevath 43850*	Ceva's theorem. Let 𝐴𝐵𝐶 be a triangle and let points 𝐹, 𝐷 and 𝐸 lie on sides 𝐴𝐵, 𝐵𝐶, 𝐶𝐴 correspondingly. Suppose that cevians 𝐴𝐷, 𝐵𝐸 and 𝐶𝐹 intersect at one point 𝑂. Then triangle's sides are partitioned into segments and their lengths satisfy a certain identity. Here we obtain a bit stronger version by using complex numbers themselves instead of their absolute values. The proof goes by applying cevathlem2 43849 three times and then using cevathlem1 43848 to multiply obtained identities and prove the theorem. In the theorem statement we are using function 𝐺 as a collinearity indicator. For justification of that use, see sigarcol 43845. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ))    &   ⊢ (𝜑 → 𝑂 ∈ ℂ)    &   ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0))    &   ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0))    &   ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0))    ⇒   ⊢ (𝜑 → (((𝐴 − 𝐹) · (𝐶 − 𝐸)) · (𝐵 − 𝐷)) = (((𝐹 − 𝐵) · (𝐸 − 𝐴)) · (𝐷 − 𝐶)))
20.38.2  Simple groups
Theorem	simpcntrab 43851	The center of a simple group is trivial or the group is abelian. (Contributed by SS, 3-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntr‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → (𝑍 = { 0 } ∨ 𝐺 ∈ Abel))
20.39  Mathbox for Jarvin Udandy
Theorem	hirstL-ax3 43852	The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → ((¬ 𝜑 → 𝜓) → 𝜑))
Theorem	ax3h 43853	Recover ax-3 8 from hirstL-ax3 43852. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
Theorem	aibandbiaiffaiffb 43854	A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ (𝜑 ↔ 𝜓))
Theorem	aibandbiaiaiffb 43855	A closed form showing (a implies b and b implies a) implies (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))
Theorem	notatnand 43856	Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜑 ∧ 𝜓)
Theorem	aistia 43857	Given a is equivalent to ⊤, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    ⇒   ⊢ 𝜑
Theorem	aisfina 43858	Given a is equivalent to ⊥, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    ⇒   ⊢ ¬ 𝜑
Theorem	bothtbothsame 43859	Given both a, b are equivalent to ⊤, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	bothfbothsame 43860	Given both a, b are equivalent to ⊥, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	aiffbbtat 43861	Given a is equivalent to b, b is equivalent to ⊤ there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ↔ ⊤)
Theorem	aisbbisfaisf 43862	Given a is equivalent to b, b is equivalent to ⊥ there exists a proof for a is equivalent to F. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	axorbtnotaiffb 43863	Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1504 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜓)    ⇒   ⊢ ¬ (𝜑 ↔ 𝜓)
Theorem	aiffnbandciffatnotciffb 43864	Given a is equivalent to (not b), c is equivalent to a, there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ ¬ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    ⇒   ⊢ ¬ (𝜒 ↔ 𝜓)
Theorem	axorbciffatcxorb 43865	Given a is equivalent to (not b), c is equivalent to a. there exists a proof for ( c xor b ). (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    ⇒   ⊢ (𝜒 ⊻ 𝜓)
Theorem	aibnbna 43866	Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ ¬ 𝜑
Theorem	aibnbaif 43867	Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	aiffbtbat 43868	Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (⊤ ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ⊤)
Theorem	astbstanbst 43869	Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ ((𝜑 ∧ 𝜓) ↔ ⊤)
Theorem	aistbistaandb 43870	Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for (a and b). (Contributed by Jarvin Udandy, 9-Sep-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ∧ 𝜓)
Theorem	aisbnaxb 43871	Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ (𝜑 ⊻ 𝜓)
Theorem	atbiffatnnb 43872	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	bisaiaisb 43873	Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
Theorem	atbiffatnnbalt 43874	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	abnotbtaxb 43875	Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	abnotataxb 43876	Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ¬ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	conimpf 43877	Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	conimpfalt 43878	Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	aistbisfiaxb 43879	Given a is equivalent to T., Given b is equivalent to F. there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	aisfbistiaxb 43880	Given a is equivalent to F., Given b is equivalent to T., there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	aifftbifffaibif 43881	Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a implies b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ ((𝜑 → 𝜓) ↔ ⊥)
Theorem	aifftbifffaibifff 43882	Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a iff b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ ((𝜑 ↔ 𝜓) ↔ ⊥)
Theorem	atnaiana 43883	Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))
Theorem	ainaiaandna 43884	Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)))
Theorem	abcdta 43885	Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜑
Theorem	abcdtb 43886	Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜓
Theorem	abcdtc 43887	Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜒
Theorem	abcdtd 43888	Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜃
Theorem	abciffcbatnabciffncba 43889	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑))
Theorem	abciffcbatnabciffncbai 43890	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑))    ⇒   ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑))
Theorem	nabctnabc 43891	not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ ¬ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (¬ 𝜑 → (𝜓 ∧ 𝜒))
Theorem	jabtaib 43892	For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	onenotinotbothi 43893	From one negated implication it is not the case its nonnegated form and a random others are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.)
⊢ ¬ (𝜑 → 𝜓)    ⇒   ⊢ ¬ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜃))
Theorem	twonotinotbothi 43894	From these two negated implications it is not the case their nonnegated forms are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.)
⊢ ¬ (𝜑 → 𝜓)    &   ⊢ ¬ (𝜒 → 𝜃)    ⇒   ⊢ ¬ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜃))
Theorem	clifte 43895	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ (𝜑 ∧ ¬ 𝜒)    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	cliftet 43896	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ (𝜑 ∧ 𝜒)    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)))
Theorem	clifteta 43897	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	cliftetb 43898	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)))
Theorem	confun 43899	Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ 𝜑    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜑 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜒 → (𝜃 ↔ 𝜑))
Theorem	confun2 43900	Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ (𝜓 → 𝜑)    &   ⊢ (𝜓 → ¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)))    &   ⊢ ((𝜓 → 𝜑) → ((𝜓 → 𝜑) → 𝜑))    ⇒   ⊢ (𝜓 → (¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)) ↔ (𝜓 → 𝜑)))