P. 328 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32701-32800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	atoml2i 32701	An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition P8(ii) of [BeltramettiCassinelli1] p. 400. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((𝐵 ∈ HAtoms ∧ ¬ 𝐵 ⊆ 𝐴) → ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms)
Theorem	atordi 32702	An ordering law for a Hilbert lattice atom and a commuting subspace. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((𝐵 ∈ HAtoms ∧ 𝐴 𝐶ℋ 𝐵) → (𝐵 ⊆ 𝐴 ∨ 𝐵 ⊆ (⊥‘𝐴)))
Theorem	atcvatlem 32703	Lemma for atcvati 32704. (Contributed by NM, 27-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms))
Theorem	atcvati 32704	A nonzero Hilbert lattice element less than the join of two atoms is an atom. (Contributed by NM, 28-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶)) → 𝐴 ∈ HAtoms))
Theorem	atcvat2i 32705	A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ (𝐵 ∨ℋ 𝐶)) → 𝐴 ∈ HAtoms))
Theorem	atord 32706	An ordering law for a Hilbert lattice atom and a commuting subspace. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐴 𝐶ℋ 𝐵) → (𝐵 ⊆ 𝐴 ∨ 𝐵 ⊆ (⊥‘𝐴)))
Theorem	atcvat2 32707	A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 29-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ (𝐵 ∨ℋ 𝐶)) → 𝐴 ∈ HAtoms))
20.8.5  Irreducibility
Theorem	chirredlem1 32708*	Lemma for chirredi 32712. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (((𝑝 ∈ HAtoms ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑝 ∩ (⊥‘𝑟)) = 0ℋ)
Theorem	chirredlem2 32709*	Lemma for chirredi 32712. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞)) = 𝑞)
Theorem	chirredlem3 32710*	Lemma for chirredi 32712. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥)    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝))
Theorem	chirredlem4 32711*	Lemma for chirredi 32712. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥)    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 = 𝑝 ∨ 𝑟 = 𝑞))
Theorem	chirredi 32712*	The Hilbert lattice is irreducible: any element that commutes with all elements must be zero or one. Theorem 14.8.4 of [BeltramettiCassinelli] p. 166. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥)    ⇒   ⊢ (𝐴 = 0ℋ ∨ 𝐴 = ℋ)
Theorem	chirred 32713*	The Hilbert lattice is irreducible: any element that commutes with all elements must be zero or one. Theorem 14.8.4 of [BeltramettiCassinelli] p. 166. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ ∀𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥) → (𝐴 = 0ℋ ∨ 𝐴 = ℋ))
20.8.6  Atoms (cont.)
Theorem	atcvat3i 32714	A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (((¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ HAtoms))
Theorem	atcvat4i 32715*	A condition implying existence of an atom with the properties shown. Lemma 3.2.20 of [PtakPulmannova] p. 68. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))))
Theorem	atdmd 32716	Two Hilbert lattice elements have the dual modular pair property if the first is an atom. Theorem 7.6(c) of [MaedaMaeda] p. 31. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → 𝐴 𝑀ℋ* 𝐵)
Theorem	atmd 32717	Two Hilbert lattice elements have the modular pair property if the first is an atom. Theorem 7.6(b) of [MaedaMaeda] p. 31. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → 𝐴 𝑀ℋ 𝐵)
Theorem	atmd2 32718	Two Hilbert lattice elements have the dual modular pair property if the second is an atom. Part of Exercise 6 of [Kalmbach] p. 103. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → 𝐴 𝑀ℋ 𝐵)
Theorem	atabsi 32719	Absorption of an incomparable atom. Similar to Exercise 7.1 of [MaedaMaeda] p. 34. (Contributed by NM, 15-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐶 ∈ HAtoms → (¬ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ 𝐵) = (𝐴 ∩ 𝐵)))
Theorem	atabs2i 32720	Absorption of an incomparable atom. (Contributed by NM, 18-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐶 ∈ HAtoms → (¬ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴))
20.8.7  Modular symmetry
Theorem	mdsymlem1 32721*	Lemma for mdsymi 32729. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ (((𝑝 ∈ Cℋ ∧ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝑝 ⊆ 𝐴)
Theorem	mdsymlem2 32722*	Lemma for mdsymi 32729. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ (((𝑝 ∈ HAtoms ∧ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐵 ≠ 0ℋ → ∃𝑟 ∈ HAtoms ∃𝑞 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))))
Theorem	mdsymlem3 32723*	Lemma for mdsymi 32729. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ ¬ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ 𝐴 ≠ 0ℋ) → ∃𝑟 ∈ HAtoms ∃𝑞 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)))
Theorem	mdsymlem4 32724*	Lemma for mdsymi 32729. This is the forward direction of Lemma 4(i) of [Maeda] p. 168. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ (𝑝 ∈ HAtoms → ((𝐵 𝑀ℋ* 𝐴 ∧ ((𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ) ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵))) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))))
Theorem	mdsymlem5 32725*	Lemma for mdsymi 32729. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (¬ 𝑞 = 𝑝 → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (((𝑐 ∈ Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))))))
Theorem	mdsymlem6 32726*	Lemma for mdsymi 32729. This is the converse direction of Lemma 4(i) of [Maeda] p. 168, and is based on the proof of Theorem 1(d) to (e) of [Maeda] p. 167. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ (∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → 𝐵 𝑀ℋ* 𝐴)
Theorem	mdsymlem7 32727*	Lemma for mdsymi 32729. Lemma 4(i) of [Maeda] p. 168. Note that Maeda's 1965 definition of dual modular pair has reversed arguments compared to the later (1970) definition given in Remark 29.6 of [MaedaMaeda] p. 130, which is the one that we use. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ ((𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ) → (𝐵 𝑀ℋ* 𝐴 ↔ ∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)))))
Theorem	mdsymlem8 32728*	Lemma for mdsymi 32729. Lemma 4(ii) of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ ((𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ) → (𝐵 𝑀ℋ* 𝐴 ↔ 𝐴 𝑀ℋ* 𝐵))
Theorem	mdsymi 32729	M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴)
Theorem	mdsym 32730	M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴))
Theorem	dmdsym 32731	Dual M-symmetry of the Hilbert lattice. (Contributed by NM, 25-Jul-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ 𝐵 𝑀ℋ* 𝐴))
Theorem	atdmd2 32732	Two Hilbert lattice elements have the dual modular pair property if the second is an atom. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → 𝐴 𝑀ℋ* 𝐵)
Theorem	sumdmdii 32733	If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark in [MaedaMaeda] p. 139. (Contributed by NM, 12-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) → 𝐴 𝑀ℋ* 𝐵)
Theorem	cmmdi 32734	Commuting subspaces form a modular pair. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵)
Theorem	cmdmdi 32735	Commuting subspaces form a dual modular pair. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐴 𝑀ℋ* 𝐵)
Theorem	sumdmdlem 32736	Lemma for sumdmdi 32738. The span of vector 𝐶 not in the subspace sum is "trimmed off." (Contributed by NM, 18-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐶 ∈ ℋ ∧ ¬ 𝐶 ∈ (𝐴 +ℋ 𝐵)) → ((𝐵 +ℋ (span‘{𝐶})) ∩ 𝐴) = (𝐵 ∩ 𝐴))
Theorem	sumdmdlem2 32737*	Lemma for sumdmdi 32738. (Contributed by NM, 23-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	sumdmdi 32738	The subspace sum of two Hilbert lattice elements is closed iff the elements are a dual modular pair. Theorem 2 of [Holland] p. 1519. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ↔ 𝐴 𝑀ℋ* 𝐵)
Theorem	dmdbr4ati 32739*	Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))
Theorem	dmdbr5ati 32740*	Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))
Theorem	dmdbr6ati 32741*	Dual modular pair property in terms of atoms. The modular law takes the form of the shearing identity. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝐴 ∨ℋ 𝐵) ∩ 𝑥) = ((((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ∩ 𝑥))
Theorem	dmdbr7ati 32742*	Dual modular pair property in terms of atoms. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝐴 ∨ℋ 𝐵) ∩ 𝑥) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))
Theorem	mdoc1i 32743	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝑀ℋ (⊥‘𝐴)
Theorem	mdoc2i 32744	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) 𝑀ℋ 𝐴
Theorem	dmdoc1i 32745	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝑀ℋ* (⊥‘𝐴)
Theorem	dmdoc2i 32746	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) 𝑀ℋ* 𝐴
Theorem	mdcompli 32747	A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of [MaedaMaeda] p. 4. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ 𝐵 ↔ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐵))) 𝑀ℋ (𝐵 ∩ (⊥‘(𝐴 ∩ 𝐵))))
Theorem	dmdcompli 32748	A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐵))) 𝑀ℋ* (𝐵 ∩ (⊥‘(𝐴 ∩ 𝐵))))
Theorem	mddmdin0i 32749*	If dual modular implies modular whenever meet is zero, then dual modular implies modular for arbitrary lattice elements. This theorem is needed for the remark after Lemma 7 of [Holland] p. 1524 to hold. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ ((𝑥 𝑀ℋ* 𝑦 ∧ (𝑥 ∩ 𝑦) = 0ℋ) → 𝑥 𝑀ℋ 𝑦)    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 → 𝐴 𝑀ℋ 𝐵)
Theorem	cdjreui 32750*	A member of the sum of disjoint subspaces has a unique decomposition. Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 20-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦))
Theorem	cdj1i 32751*	Two ways to express "𝐴 and 𝐵 are completely disjoint subspaces." (1) => (2) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 21-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (∃𝑤 ∈ ℝ (0 < 𝑤 ∧ ∀𝑦 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ((normℎ‘𝑦) + (normℎ‘𝑣)) ≤ (𝑤 · (normℎ‘(𝑦 +ℎ 𝑣)))) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) = 1 → 𝑥 ≤ (normℎ‘(𝑦 −ℎ 𝑧)))))
Theorem	cdj3lem1 32752*	A property of "𝐴 and 𝐵 are completely disjoint subspaces." Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) + (normℎ‘𝑧)) ≤ (𝑥 · (normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) = 0ℋ)
Theorem	cdj3lem2 32753*	Lemma for cdj3i 32759. Value of the first-component function 𝑆. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘(𝐶 +ℎ 𝐷)) = 𝐶)
Theorem	cdj3lem2a 32754*	Lemma for cdj3i 32759. Closure of the first-component function 𝑆. (Contributed by NM, 25-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘𝐶) ∈ 𝐴)
Theorem	cdj3lem2b 32755*	Lemma for cdj3i 32759. The first-component function 𝑆 is bounded if the subspaces are completely disjoint. (Contributed by NM, 26-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 · (normℎ‘(𝑥 +ℎ 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑆‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢))))
Theorem	cdj3lem3 32756*	Lemma for cdj3i 32759. Value of the second-component function 𝑇. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘(𝐶 +ℎ 𝐷)) = 𝐷)
Theorem	cdj3lem3a 32757*	Lemma for cdj3i 32759. Closure of the second-component function 𝑇. (Contributed by NM, 26-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘𝐶) ∈ 𝐵)
Theorem	cdj3lem3b 32758*	Lemma for cdj3i 32759. The second-component function 𝑇 is bounded if the subspaces are completely disjoint. (Contributed by NM, 31-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 · (normℎ‘(𝑥 +ℎ 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢))))
Theorem	cdj3i 32759*	Two ways to express "𝐴 and 𝐵 are completely disjoint subspaces." (1) <=> (3) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 1-Jun-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    &   ⊢ (𝜑 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑆‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢))))    &   ⊢ (𝜓 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢))))    ⇒   ⊢ (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 · (normℎ‘(𝑥 +ℎ 𝑦)))) ↔ ((𝐴 ∩ 𝐵) = 0ℋ ∧ 𝜑 ∧ 𝜓))
PART 21  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
21.1  Mathboxes for user contributions
21.1.1  Mathbox guidelines
Theorem	mathbox 32760	(This theorem is a dummy placeholder for these guidelines. The label of this theorem, "mathbox", is hard-coded into the Metamath program to identify the start of the mathbox section for web page generation.) A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm. Mathboxes are provided to help keep your work synchronized with changes in set.mm while allowing you to work independently without affecting other contributors. Even though in a sense your mathbox belongs to you, it is still part of the shared body of knowledge contained in set.mm, and occasionally other people may make maintenance edits to your mathbox for things like keeping it synchronized with the rest of set.mm, reducing proof lengths, moving your theorems to the main part of set.mm when needed, and fixing typos or other errors. If you want to preserve it the way you left it, you can keep a local copy or keep track of the GitHub commit number. Guidelines: 1. See conventions 30717 for our general style guidelines. For contributing via GitHub, see https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md 30717. The Metamath program command "verify markup *" will check that you have followed many of the conventions we use. 2. If at all possible, please use only nullary class constants for new definitions, for example as in df-div 11871. 3. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The Metamath program "MM> WRITE SOURCE set.mm / REWRAP" command will take care of indentation conventions and line wrapping. 4. All mathbox content will be on public display and should hopefully reflect the overall quality of the website. 5. Mathboxes must be independent from one another (checked by "verify markup *"). If you need a theorem from another mathbox, typically it is moved to the main part of set.mm. New users should consult with more experienced users before doing this. 6. If a contributor is no longer active, we will continue the usual maintenance edits. As time goes on, often theorems will be moved to main or removed in favor of similar replacements. But we are also willing to maintain mathboxes in place, as work by others from years ago may form the foundation of future work; you could even argue that all of mathematics is like that. 7. For theorems of importance (for example, a Metamath 100 theorem or a dependency of one), we prefer to eventually move them out of mathboxes (although a mathbox is perfectly appropriate as proofs are being developed and refined). (Contributed by NM, 20-Feb-2007.) (Revised by the Metamath team, 9-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ 𝜑
21.2  Mathbox for Stefan Allan
Theorem	sa-abvi 32761	A theorem about the universal class. Inference associated with bj-abv 37507 (which is proved from fewer axioms). (Contributed by Stefan Allan, 9-Dec-2008.)
⊢ 𝜑    ⇒   ⊢ V = {𝑥 ∣ 𝜑}
Theorem	xfree 32762	A partial converse to 19.9t 2238. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(∃𝑥𝜑 → 𝜑))
Theorem	xfree2 32763	A partial converse to 19.9t 2238. (Contributed by Stefan Allan, 21-Dec-2008.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
Theorem	addltmulALT 32764	A proof readability experiment for addltmul 12479. (Contributed by Stefan Allan, 30-Oct-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (2 < 𝐴 ∧ 2 < 𝐵)) → (𝐴 + 𝐵) < (𝐴 · 𝐵))
21.3  Mathbox for Thierry Arnoux
21.3.1  Propositional Calculus - misc additions
Theorem	ad11antr 32765	Deduction adding 11 conjuncts to antecedent. (Contributed by Thierry Arnoux, 27-Sep-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜓)
Theorem	simp-12l 32766	Simplification of a conjunction. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜑)
Theorem	simp-12r 32767	Simplification of a conjunction. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜓)
Theorem	an52ds 32768	Inference exchanging the last antecedent with the second. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜒) ∧ 𝜃) ∧ 𝜓) → 𝜂)
Theorem	an62ds 32769	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((((((𝜑 ∧ 𝜂) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜁)
Theorem	an72ds 32770	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (((((((𝜑 ∧ 𝜁) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜎)
Theorem	an82ds 32771	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜌)    ⇒   ⊢ ((((((((𝜑 ∧ 𝜎) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜓) → 𝜌)
Theorem	syl22anbrc 32772	Syllogism inference. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜂 ↔ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)))    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	or3di 32773	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
⊢ ((𝜑 ∨ (𝜓 ∧ 𝜒 ∧ 𝜏)) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)))
Theorem	or3dir 32774	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∨ 𝜏) ↔ ((𝜑 ∨ 𝜏) ∧ (𝜓 ∨ 𝜏) ∧ (𝜒 ∨ 𝜏)))
Theorem	3o1cs 32775	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	3o2cs 32776	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	3o3cs 32777	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
21.3.2  Predicate Calculus
21.3.2.1  Predicate Calculus - misc additions
Theorem	sbc2iedf 32778*	Conversion of implicit substitution to explicit class substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ↔ 𝜒))
Theorem	rspc2daf 32779*	Double restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
21.3.2.2  Restricted quantification - misc additions
Theorem	ralcom4f 32780*	Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexcom4f 32781*	Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
Theorem	19.9d2rf 32782	A deduction version of one direction of 19.9 2239 with two variables. (Contributed by Thierry Arnoux, 20-Mar-2017.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.9d2r 32783*	A deduction version of one direction of 19.9 2239 with two variables. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	r19.29ffa 32784*	A commonly used pattern based on r19.29 3126, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → 𝜒)
Theorem	reu6dv 32785*	A condition which implies existential uniqueness. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)
21.3.2.3  Equality
Theorem	eqtrb 32786	A transposition of equality. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))
Theorem	eqelbid 32787*	A variable elimination law for equality within a given set 𝐴. See equvel 2486. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝑥 = 𝐵 ↔ 𝑥 = 𝐶) ↔ 𝐵 = 𝐶))
21.3.2.4  Double restricted existential uniqueness quantification
Theorem	opsbc2ie 32788*	Conversion of implicit substitution to explicit class substitution for ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒))
Theorem	opreu2reuALT 32789*	Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex 6295 instead. (Contributed by Thierry Arnoux, 4-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((∃!𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃!𝑏 ∈ 𝐵 ∃𝑎 ∈ 𝐴 𝜒) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
21.3.2.5  Double restricted existential uniqueness quantification syntax
Syntax	w2reu 32790	Syntax for double restricted existential uniqueness quantification.
wff ∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑
Definition	df-2reu 32791	Define the double restricted existential uniqueness quantifier. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))
Theorem	2reucom 32792	Double restricted existential uniqueness commutes. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴𝜑)
Theorem	2reu2rex1 32793	Double restricted existential uniqueness implies double restricted existence. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	2reureurex 32794	Double restricted existential uniqueness implies restricted existential uniqueness with restricted existence. (Contributed by AV, 5-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	2reu2reu2 32795*	Double restricted existential uniqueness implies two nested restricted existential uniqueness. (Contributed by AV, 5-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑)
Theorem	opreu2reu1 32796*	Equivalent definition of the double restricted existential uniqueness quantifier, using uniqueness of ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜒 ↔ 𝜑))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑝 ∈ (𝐴 × 𝐵)𝜒)
Theorem	sq2reunnltb 32797*	There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. Double restricted existential uniqueness variant of 2sqreunnltb 27601. (Contributed by AV, 5-Jul-2023.)
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑎 ∈ ℕ , 𝑏 ∈ ℕ(𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
Theorem	addsqnot2reu 32798*	For each complex number 𝐶, there does not uniquely exist two complex numbers 𝑎 and 𝑏, with 𝑏 squared and added to 𝑎 resulting in the given complex number 𝐶. Double restricted existential uniqueness variant of addsqn2reurex2 27585. (Contributed by AV, 5-Jul-2023.)
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑎 ∈ ℂ , 𝑏 ∈ ℂ(𝑎 + (𝑏↑2)) = 𝐶)
21.3.2.6  Substitution (without distinct variables) - misc additions
Theorem	sbceqbidf 32799	Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒))
Theorem	sbcies 32800*	A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝐴 = (𝐸‘𝑊)    &   ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎]𝜓 ↔ 𝜑))