P. 325 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32401-32500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	atomli 32401	An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition 3.2.17 of [PtakPulmannova] p. 66. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝐵 ∈ HAtoms → ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ (HAtoms ∪ {0ℋ}))
Theorem	atoml2i 32402	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 32403	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 32404	Lemma for atcvati 32405. (Contributed by NM, 27-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms))
Theorem	atcvati 32405	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 32406	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 32407	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 32408	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 32409*	Lemma for chirredi 32413. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (((𝑝 ∈ HAtoms ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑝 ∩ (⊥‘𝑟)) = 0ℋ)
Theorem	chirredlem2 32410*	Lemma for chirredi 32413. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞)) = 𝑞)
Theorem	chirredlem3 32411*	Lemma for chirredi 32413. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥)    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝))
Theorem	chirredlem4 32412*	Lemma for chirredi 32413. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥)    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 = 𝑝 ∨ 𝑟 = 𝑞))
Theorem	chirredi 32413*	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 32414*	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 32415	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 32416*	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 32417	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 32418	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 32419	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 32420	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 32421	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 32422*	Lemma for mdsymi 32430. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ (((𝑝 ∈ Cℋ ∧ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝑝 ⊆ 𝐴)
Theorem	mdsymlem2 32423*	Lemma for mdsymi 32430. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ (((𝑝 ∈ HAtoms ∧ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐵 ≠ 0ℋ → ∃𝑟 ∈ HAtoms ∃𝑞 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))))
Theorem	mdsymlem3 32424*	Lemma for mdsymi 32430. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ ¬ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ 𝐴 ≠ 0ℋ) → ∃𝑟 ∈ HAtoms ∃𝑞 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)))
Theorem	mdsymlem4 32425*	Lemma for mdsymi 32430. 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 32426*	Lemma for mdsymi 32430. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (¬ 𝑞 = 𝑝 → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (((𝑐 ∈ Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))))))
Theorem	mdsymlem6 32427*	Lemma for mdsymi 32430. 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 32428*	Lemma for mdsymi 32430. 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 32429*	Lemma for mdsymi 32430. Lemma 4(ii) of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ ((𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ) → (𝐵 𝑀ℋ* 𝐴 ↔ 𝐴 𝑀ℋ* 𝐵))
Theorem	mdsymi 32430	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 32431	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 32432	Dual M-symmetry of the Hilbert lattice. (Contributed by NM, 25-Jul-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ 𝐵 𝑀ℋ* 𝐴))
Theorem	atdmd2 32433	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 32434	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 32435	Commuting subspaces form a modular pair. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵)
Theorem	cmdmdi 32436	Commuting subspaces form a dual modular pair. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐴 𝑀ℋ* 𝐵)
Theorem	sumdmdlem 32437	Lemma for sumdmdi 32439. 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 32438*	Lemma for sumdmdi 32439. (Contributed by NM, 23-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	sumdmdi 32439	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 32440*	Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))
Theorem	dmdbr5ati 32441*	Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))
Theorem	dmdbr6ati 32442*	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 32443*	Dual modular pair property in terms of atoms. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝐴 ∨ℋ 𝐵) ∩ 𝑥) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))
Theorem	mdoc1i 32444	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝑀ℋ (⊥‘𝐴)
Theorem	mdoc2i 32445	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) 𝑀ℋ 𝐴
Theorem	dmdoc1i 32446	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝑀ℋ* (⊥‘𝐴)
Theorem	dmdoc2i 32447	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) 𝑀ℋ* 𝐴
Theorem	mdcompli 32448	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 32449	A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐵))) 𝑀ℋ* (𝐵 ∩ (⊥‘(𝐴 ∩ 𝐵))))
Theorem	mddmdin0i 32450*	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 32451*	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 32452*	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 32453*	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 32454*	Lemma for cdj3i 32460. Value of the first-component function 𝑆. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘(𝐶 +ℎ 𝐷)) = 𝐶)
Theorem	cdj3lem2a 32455*	Lemma for cdj3i 32460. Closure of the first-component function 𝑆. (Contributed by NM, 25-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘𝐶) ∈ 𝐴)
Theorem	cdj3lem2b 32456*	Lemma for cdj3i 32460. 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 32457*	Lemma for cdj3i 32460. Value of the second-component function 𝑇. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘(𝐶 +ℎ 𝐷)) = 𝐷)
Theorem	cdj3lem3a 32458*	Lemma for cdj3i 32460. Closure of the second-component function 𝑇. (Contributed by NM, 26-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘𝐶) ∈ 𝐵)
Theorem	cdj3lem3b 32459*	Lemma for cdj3i 32460. 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 32460*	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 32461	(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 30419 for our general style guidelines. For contributing via GitHub, see https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md 30419. 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 11921. 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 32462	A theorem about the universal class. Inference associated with bj-abv 36907 (which is proved from fewer axioms). (Contributed by Stefan Allan, 9-Dec-2008.)
⊢ 𝜑    ⇒   ⊢ V = {𝑥 ∣ 𝜑}
Theorem	xfree 32463	A partial converse to 19.9t 2204. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(∃𝑥𝜑 → 𝜑))
Theorem	xfree2 32464	A partial converse to 19.9t 2204. (Contributed by Stefan Allan, 21-Dec-2008.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
Theorem	addltmulALT 32465	A proof readability experiment for addltmul 12502. (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 32466	Deduction adding 11 conjuncts to antecedent. (Contributed by Thierry Arnoux, 27-Sep-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜓)
Theorem	simp-12l 32467	Simplification of a conjunction. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜑)
Theorem	simp-12r 32468	Simplification of a conjunction. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜓)
Theorem	an42ds 32469	Inference exchanging the last antecedent with the second one. See also an32s 652. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜒) ∧ 𝜓) → 𝜏)
Theorem	an52ds 32470	Inference exchanging the last antecedent with the second. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜒) ∧ 𝜃) ∧ 𝜓) → 𝜂)
Theorem	an62ds 32471	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((((((𝜑 ∧ 𝜂) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜁)
Theorem	an72ds 32472	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (((((((𝜑 ∧ 𝜁) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜎)
Theorem	an82ds 32473	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜌)    ⇒   ⊢ ((((((((𝜑 ∧ 𝜎) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜓) → 𝜌)
Theorem	syl22anbrc 32474	Syllogism inference. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜂 ↔ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)))    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	bian1d 32475	Adding a superfluous conjunct in a biconditional. (Contributed by Thierry Arnoux, 26-Feb-2017.) (Proof shortened by Hongxiu Chen, 29-Jun-2025.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃)))
Theorem	bian1dOLD 32476	Obsolete version of bian1d 32475 as of 29-Jun-2025. (Contributed by Thierry Arnoux, 26-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃)))
Theorem	orim12da 32477	Deduce a disjunction from another one. Variation on orim12d 967. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜏)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → (𝜃 ∨ 𝜏))
Theorem	or3di 32478	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
⊢ ((𝜑 ∨ (𝜓 ∧ 𝜒 ∧ 𝜏)) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)))
Theorem	or3dir 32479	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∨ 𝜏) ↔ ((𝜑 ∨ 𝜏) ∧ (𝜓 ∨ 𝜏) ∧ (𝜒 ∨ 𝜏)))
Theorem	3o1cs 32480	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	3o2cs 32481	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	3o3cs 32482	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	13an22anass 32483	Associative law for four conjunctions with a triple conjunction. (Contributed by Thierry Arnoux, 21-Jan-2025.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
21.3.2  Predicate Calculus
21.3.2.1  Predicate Calculus - misc additions
Theorem	sbc2iedf 32484*	Conversion of implicit substitution to explicit class substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ↔ 𝜒))
Theorem	rspc2daf 32485*	Double restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
21.3.2.2  Restricted quantification - misc additions
Theorem	ralcom4f 32486*	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 32487*	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 32488	A deduction version of one direction of 19.9 2205 with two variables. (Contributed by Thierry Arnoux, 20-Mar-2017.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.9d2r 32489*	A deduction version of one direction of 19.9 2205 with two variables. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	r19.29ffa 32490*	A commonly used pattern based on r19.29 3114, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → 𝜒)
Theorem	n0limd 32491*	Deduction rule for nonempty classes. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	reu6dv 32492*	A condition which implies existential uniqueness. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)
21.3.2.3  Equality
Theorem	eqtrb 32493	A transposition of equality. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))
Theorem	eqelbid 32494*	A variable elimination law for equality within a given set 𝐴. See equvel 2461. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝑥 = 𝐵 ↔ 𝑥 = 𝐶) ↔ 𝐵 = 𝐶))
21.3.2.4  Double restricted existential uniqueness quantification
Theorem	opsbc2ie 32495*	Conversion of implicit substitution to explicit class substitution for ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒))
Theorem	opreu2reuALT 32496*	Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex 6314 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 32497	Syntax for double restricted existential uniqueness quantification.
wff ∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑
Definition	df-2reu 32498	Define the double restricted existential uniqueness quantifier. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))
Theorem	2reucom 32499	Double restricted existential uniqueness commutes. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴𝜑)
Theorem	2reu2rex1 32500	Double restricted existential uniqueness implies double restricted existence. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)