Metamath Proof Explorer

Theorem mdsymlem7

Description: Lemma for mdsymi . 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.)

Ref Expression
Hypotheses mdsymlem1.1 ⊢ A ∈ C ℋ
mdsymlem1.2 ⊢ B ∈ C ℋ
mdsymlem1.3 ⊢ C = A ∨ ℋ p
Assertion mdsymlem7 ⊢ A ≠ 0 ℋ ∧ B ≠ 0 ℋ → B 𝑀 ℋ * A ↔ ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B

Proof

Step Hyp Ref Expression
1 mdsymlem1.1 ⊢ A ∈ C ℋ
2 mdsymlem1.2 ⊢ B ∈ C ℋ
3 mdsymlem1.3 ⊢ C = A ∨ ℋ p
4 1 2 3 mdsymlem4 ⊢ p ∈ HAtoms → B 𝑀 ℋ * A ∧ A ≠ 0 ℋ ∧ B ≠ 0 ℋ ∧ p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
5 4 exp4d ⊢ p ∈ HAtoms → B 𝑀 ℋ * A → A ≠ 0 ℋ ∧ B ≠ 0 ℋ → p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
6 5 com13 ⊢ A ≠ 0 ℋ ∧ B ≠ 0 ℋ → B 𝑀 ℋ * A → p ∈ HAtoms → p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
7 6 ralrimdv ⊢ A ≠ 0 ℋ ∧ B ≠ 0 ℋ → B 𝑀 ℋ * A → ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
8 1 2 3 mdsymlem6 ⊢ ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B → B 𝑀 ℋ * A
9 7 8 impbid1 ⊢ A ≠ 0 ℋ ∧ B ≠ 0 ℋ → B 𝑀 ℋ * A ↔ ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B