Metamath Proof Explorer

Theorem mdsymlem4

Description: Lemma for mdsymi . This is the forward direction of Lemma 4(i) of Maeda p. 168. (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsymlem1.1 ⊢ A ∈ C ℋ
mdsymlem1.2 ⊢ B ∈ C ℋ
mdsymlem1.3 ⊢ C = A ∨ ℋ p
Assertion mdsymlem4 ⊢ p ∈ HAtoms → B 𝑀 ℋ * A ∧ A ≠ 0 ℋ ∧ B ≠ 0 ℋ ∧ 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 mdsymlem2 ⊢ p ∈ HAtoms ∧ B ∩ C ⊆ A ∧ B 𝑀 ℋ * A ∧ p ⊆ A ∨ ℋ B → B ≠ 0 ℋ → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
5 4 exp31 ⊢ p ∈ HAtoms → B ∩ C ⊆ A → B 𝑀 ℋ * A ∧ p ⊆ A ∨ ℋ B → B ≠ 0 ℋ → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
6 5 com4t ⊢ B 𝑀 ℋ * A ∧ p ⊆ A ∨ ℋ B → B ≠ 0 ℋ → p ∈ HAtoms → B ∩ C ⊆ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
7 6 ex ⊢ B 𝑀 ℋ * A → p ⊆ A ∨ ℋ B → B ≠ 0 ℋ → p ∈ HAtoms → B ∩ C ⊆ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
8 7 com23 ⊢ B 𝑀 ℋ * A → B ≠ 0 ℋ → p ⊆ A ∨ ℋ B → p ∈ HAtoms → B ∩ C ⊆ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
9 8 a1d ⊢ B 𝑀 ℋ * A → A ≠ 0 ℋ → B ≠ 0 ℋ → p ⊆ A ∨ ℋ B → p ∈ HAtoms → B ∩ C ⊆ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
10 9 imp44 ⊢ B 𝑀 ℋ * A ∧ A ≠ 0 ℋ ∧ B ≠ 0 ℋ ∧ p ⊆ A ∨ ℋ B → p ∈ HAtoms → B ∩ C ⊆ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
11 10 com3l ⊢ p ∈ HAtoms → B ∩ C ⊆ A → B 𝑀 ℋ * A ∧ A ≠ 0 ℋ ∧ B ≠ 0 ℋ ∧ p ⊆ A ∨ ℋ B → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
12 1 2 3 mdsymlem3 ⊢ p ∈ HAtoms ∧ ¬ B ∩ C ⊆ A ∧ p ⊆ A ∨ ℋ B ∧ A ≠ 0 ℋ → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
13 12 anasss ⊢ p ∈ HAtoms ∧ ¬ B ∩ C ⊆ A ∧ p ⊆ A ∨ ℋ B ∧ A ≠ 0 ℋ → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
14 13 exp31 ⊢ p ∈ HAtoms → ¬ B ∩ C ⊆ A → p ⊆ A ∨ ℋ B ∧ A ≠ 0 ℋ → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
15 14 com3r ⊢ p ⊆ A ∨ ℋ B ∧ A ≠ 0 ℋ → p ∈ HAtoms → ¬ B ∩ C ⊆ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
16 15 ancoms ⊢ A ≠ 0 ℋ ∧ p ⊆ A ∨ ℋ B → p ∈ HAtoms → ¬ B ∩ C ⊆ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
17 16 adantlr ⊢ A ≠ 0 ℋ ∧ B ≠ 0 ℋ ∧ p ⊆ A ∨ ℋ B → p ∈ HAtoms → ¬ B ∩ C ⊆ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
18 17 adantl ⊢ B 𝑀 ℋ * A ∧ A ≠ 0 ℋ ∧ B ≠ 0 ℋ ∧ p ⊆ A ∨ ℋ B → p ∈ HAtoms → ¬ B ∩ C ⊆ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
19 18 com3l ⊢ p ∈ HAtoms → ¬ B ∩ C ⊆ A → B 𝑀 ℋ * A ∧ A ≠ 0 ℋ ∧ B ≠ 0 ℋ ∧ p ⊆ A ∨ ℋ B → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
20 11 19 pm2.61d ⊢ p ∈ HAtoms → B 𝑀 ℋ * A ∧ A ≠ 0 ℋ ∧ B ≠ 0 ℋ ∧ p ⊆ A ∨ ℋ B → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
21 rexcom ⊢ ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B ↔ ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
22 20 21 imbitrdi ⊢ p ∈ HAtoms → B 𝑀 ℋ * A ∧ A ≠ 0 ℋ ∧ B ≠ 0 ℋ ∧ p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B