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	chrelat4i 32401*	A consequence of relative atomicity. Extensionality principle: two lattice elements are equal iff they majorize the same atoms. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵))
Theorem	cvexch 32402	The Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ((𝐴 ∩ 𝐵) ⋖ℋ 𝐵 ↔ 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵)))
Theorem	cvp 32403	The Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → ((𝐴 ∩ 𝐵) = 0ℋ ↔ 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵)))
Theorem	atnssm0 32404	The meet of a Hilbert lattice element and an incomparable atom is the zero subspace. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → (¬ 𝐵 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐵) = 0ℋ))
Theorem	atnemeq0 32405	The meet of distinct atoms is the zero subspace. (Contributed by NM, 25-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (𝐴 ≠ 𝐵 ↔ (𝐴 ∩ 𝐵) = 0ℋ))
Theorem	atssma 32406	The meet with an atom's superset is the atom. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) ∈ HAtoms))
Theorem	atcv0eq 32407	Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (0ℋ ⋖ℋ (𝐴 ∨ℋ 𝐵) ↔ 𝐴 = 𝐵))
Theorem	atcv1 32408	Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝐴 ⋖ℋ (𝐵 ∨ℋ 𝐶)) → (𝐴 = 0ℋ ↔ 𝐵 = 𝐶))
Theorem	atexch 32409	The Hilbert lattice satisfies the atom exchange property. Proposition 1(i) of [Kalmbach] p. 140. A version of this theorem related to vector analysis was originally proved by Hermann Grassmann in 1862. Also Definition 3.4-3(b) in [MegPav2000] p. 2345 (PDF p. 8) (use atnemeq0 32405 to obtain atom inequality). (Contributed by NM, 27-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐵 ⊆ (𝐴 ∨ℋ 𝐶) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → 𝐶 ⊆ (𝐴 ∨ℋ 𝐵)))
Theorem	atomli 32410	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 32411	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 32412	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 32413	Lemma for atcvati 32414. (Contributed by NM, 27-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms))
Theorem	atcvati 32414	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 32415	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 32416	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 32417	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 32418*	Lemma for chirredi 32422. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (((𝑝 ∈ HAtoms ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑝 ∩ (⊥‘𝑟)) = 0ℋ)
Theorem	chirredlem2 32419*	Lemma for chirredi 32422. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞)) = 𝑞)
Theorem	chirredlem3 32420*	Lemma for chirredi 32422. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥)    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝))
Theorem	chirredlem4 32421*	Lemma for chirredi 32422. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥)    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 = 𝑝 ∨ 𝑟 = 𝑞))
Theorem	chirredi 32422*	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 32423*	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 32424	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 32425*	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 32426	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 32427	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 32428	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 32429	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 32430	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 32431*	Lemma for mdsymi 32439. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ (((𝑝 ∈ Cℋ ∧ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝑝 ⊆ 𝐴)
Theorem	mdsymlem2 32432*	Lemma for mdsymi 32439. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ (((𝑝 ∈ HAtoms ∧ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐵 ≠ 0ℋ → ∃𝑟 ∈ HAtoms ∃𝑞 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))))
Theorem	mdsymlem3 32433*	Lemma for mdsymi 32439. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ ((((𝑝 ∈ HAtoms ∧ ¬ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ 𝐴 ≠ 0ℋ) → ∃𝑟 ∈ HAtoms ∃𝑞 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)))
Theorem	mdsymlem4 32434*	Lemma for mdsymi 32439. 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 32435*	Lemma for mdsymi 32439. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (¬ 𝑞 = 𝑝 → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (((𝑐 ∈ Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))))))
Theorem	mdsymlem6 32436*	Lemma for mdsymi 32439. 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 32437*	Lemma for mdsymi 32439. 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 32438*	Lemma for mdsymi 32439. Lemma 4(ii) of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝)    ⇒   ⊢ ((𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ) → (𝐵 𝑀ℋ* 𝐴 ↔ 𝐴 𝑀ℋ* 𝐵))
Theorem	mdsymi 32439	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 32440	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 32441	Dual M-symmetry of the Hilbert lattice. (Contributed by NM, 25-Jul-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ 𝐵 𝑀ℋ* 𝐴))
Theorem	atdmd2 32442	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 32443	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 32444	Commuting subspaces form a modular pair. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵)
Theorem	cmdmdi 32445	Commuting subspaces form a dual modular pair. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐴 𝑀ℋ* 𝐵)
Theorem	sumdmdlem 32446	Lemma for sumdmdi 32448. 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 32447*	Lemma for sumdmdi 32448. (Contributed by NM, 23-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	sumdmdi 32448	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 32449*	Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))
Theorem	dmdbr5ati 32450*	Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))
Theorem	dmdbr6ati 32451*	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 32452*	Dual modular pair property in terms of atoms. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝐴 ∨ℋ 𝐵) ∩ 𝑥) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))
Theorem	mdoc1i 32453	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝑀ℋ (⊥‘𝐴)
Theorem	mdoc2i 32454	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) 𝑀ℋ 𝐴
Theorem	dmdoc1i 32455	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝑀ℋ* (⊥‘𝐴)
Theorem	dmdoc2i 32456	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) 𝑀ℋ* 𝐴
Theorem	mdcompli 32457	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 32458	A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐵))) 𝑀ℋ* (𝐵 ∩ (⊥‘(𝐴 ∩ 𝐵))))
Theorem	mddmdin0i 32459*	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 32460*	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 32461*	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 32462*	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 32463*	Lemma for cdj3i 32469. Value of the first-component function 𝑆. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘(𝐶 +ℎ 𝐷)) = 𝐶)
Theorem	cdj3lem2a 32464*	Lemma for cdj3i 32469. Closure of the first-component function 𝑆. (Contributed by NM, 25-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘𝐶) ∈ 𝐴)
Theorem	cdj3lem2b 32465*	Lemma for cdj3i 32469. 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 32466*	Lemma for cdj3i 32469. Value of the second-component function 𝑇. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘(𝐶 +ℎ 𝐷)) = 𝐷)
Theorem	cdj3lem3a 32467*	Lemma for cdj3i 32469. Closure of the second-component function 𝑇. (Contributed by NM, 26-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘𝐶) ∈ 𝐵)
Theorem	cdj3lem3b 32468*	Lemma for cdj3i 32469. 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 32469*	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 32470	(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 30428 for our general style guidelines. For contributing via GitHub, see https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md 30428. 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 11918. 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 32471	A theorem about the universal class. Inference associated with bj-abv 36888 (which is proved from fewer axioms). (Contributed by Stefan Allan, 9-Dec-2008.)
⊢ 𝜑    ⇒   ⊢ V = {𝑥 ∣ 𝜑}
Theorem	xfree 32472	A partial converse to 19.9t 2201. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(∃𝑥𝜑 → 𝜑))
Theorem	xfree2 32473	A partial converse to 19.9t 2201. (Contributed by Stefan Allan, 21-Dec-2008.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
Theorem	addltmulALT 32474	A proof readability experiment for addltmul 12499. (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 32475	Deduction adding 11 conjuncts to antecedent. (Contributed by Thierry Arnoux, 27-Sep-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜓)
Theorem	simp-12l 32476	Simplification of a conjunction. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜑)
Theorem	simp-12r 32477	Simplification of a conjunction. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜓)
Theorem	an42ds 32478	Inference exchanging the last antecedent with the second one. See also an32s 652. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜒) ∧ 𝜓) → 𝜏)
Theorem	an52ds 32479	Inference exchanging the last antecedent with the second. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜒) ∧ 𝜃) ∧ 𝜓) → 𝜂)
Theorem	an62ds 32480	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((((((𝜑 ∧ 𝜂) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜁)
Theorem	an72ds 32481	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (((((((𝜑 ∧ 𝜁) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜎)
Theorem	an82ds 32482	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜌)    ⇒   ⊢ ((((((((𝜑 ∧ 𝜎) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜓) → 𝜌)
Theorem	bian1d 32483	Adding a superfluous conjunct in a biconditional. (Contributed by Thierry Arnoux, 26-Feb-2017.) (Proof shortened by Hongxiu Chen, 29-Jun-2025.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃)))
Theorem	bian1dOLD 32484	Obsolete version of bian1d 32483 as of 29-Jun-2025. (Contributed by Thierry Arnoux, 26-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃)))
Theorem	bibiad 32485	Eliminate an hypothesis 𝜃 in a biconditional. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	orim12da 32486	Deduce a disjunction from another one. Variation on orim12d 966. (Contributed by Thierry Arnoux, 18-May-2025.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜏)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → (𝜃 ∨ 𝜏))
Theorem	or3di 32487	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
⊢ ((𝜑 ∨ (𝜓 ∧ 𝜒 ∧ 𝜏)) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)))
Theorem	or3dir 32488	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∨ 𝜏) ↔ ((𝜑 ∨ 𝜏) ∧ (𝜓 ∨ 𝜏) ∧ (𝜒 ∨ 𝜏)))
Theorem	3o1cs 32489	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	3o2cs 32490	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	3o3cs 32491	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	13an22anass 32492	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 32493*	Conversion of implicit substitution to explicit class substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ↔ 𝜒))
Theorem	rspc2daf 32494*	Double restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
21.3.2.2  Restricted quantification - misc additions
Theorem	ralcom4f 32495*	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 32496*	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 32497	A deduction version of one direction of 19.9 2202 with two variables. (Contributed by Thierry Arnoux, 20-Mar-2017.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.9d2r 32498*	A deduction version of one direction of 19.9 2202 with two variables. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	r19.29ffa 32499*	A commonly used pattern based on r19.29 3111, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → 𝜒)
Theorem	n0limd 32500*	Deduction rule for nonempty classes. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)