Metamath Proof Explorer

Theorem mdsymlem8

Description: Lemma for mdsymi . Lemma 4(ii) of Maeda p. 168. (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 mdsymlem8 ⊢ A ≠ 0 ℋ ∧ B ≠ 0 ℋ → B 𝑀 ℋ * A ↔ A 𝑀 ℋ * 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 chjcomi ⊢ A ∨ ℋ B = B ∨ ℋ A
5 4 sseq2i ⊢ p ⊆ A ∨ ℋ B ↔ p ⊆ B ∨ ℋ A
6 atelch ⊢ q ∈ HAtoms → q ∈ C ℋ
7 atelch ⊢ r ∈ HAtoms → r ∈ C ℋ
8 chjcom ⊢ q ∈ C ℋ ∧ r ∈ C ℋ → q ∨ ℋ r = r ∨ ℋ q
9 6 7 8 syl2an ⊢ q ∈ HAtoms ∧ r ∈ HAtoms → q ∨ ℋ r = r ∨ ℋ q
10 9 sseq2d ⊢ q ∈ HAtoms ∧ r ∈ HAtoms → p ⊆ q ∨ ℋ r ↔ p ⊆ r ∨ ℋ q
11 ancom ⊢ q ⊆ A ∧ r ⊆ B ↔ r ⊆ B ∧ q ⊆ A
12 11 a1i ⊢ q ∈ HAtoms ∧ r ∈ HAtoms → q ⊆ A ∧ r ⊆ B ↔ r ⊆ B ∧ q ⊆ A
13 10 12 anbi12d ⊢ q ∈ HAtoms ∧ r ∈ HAtoms → p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B ↔ p ⊆ r ∨ ℋ q ∧ r ⊆ B ∧ q ⊆ A
14 13 2rexbiia ⊢ ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B ↔ ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ r ∨ ℋ q ∧ r ⊆ B ∧ q ⊆ A
15 rexcom ⊢ ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ r ∨ ℋ q ∧ r ⊆ B ∧ q ⊆ A ↔ ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ r ∨ ℋ q ∧ r ⊆ B ∧ q ⊆ A
16 14 15 bitri ⊢ ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B ↔ ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ r ∨ ℋ q ∧ r ⊆ B ∧ q ⊆ A
17 5 16 imbi12i ⊢ p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B ↔ p ⊆ B ∨ ℋ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ r ∨ ℋ q ∧ r ⊆ B ∧ q ⊆ A
18 17 ralbii ⊢ ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B ↔ ∀ p ∈ HAtoms p ⊆ B ∨ ℋ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ r ∨ ℋ q ∧ r ⊆ B ∧ q ⊆ A
19 18 a1i ⊢ A ≠ 0 ℋ ∧ B ≠ 0 ℋ → ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B ↔ ∀ p ∈ HAtoms p ⊆ B ∨ ℋ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ r ∨ ℋ q ∧ r ⊆ B ∧ q ⊆ A
20 1 2 3 mdsymlem7 ⊢ A ≠ 0 ℋ ∧ B ≠ 0 ℋ → B 𝑀 ℋ * A ↔ ∀ p ∈ HAtoms p ⊆ A ∨ ℋ B → ∃ q ∈ HAtoms ∃ r ∈ HAtoms p ⊆ q ∨ ℋ r ∧ q ⊆ A ∧ r ⊆ B
21 eqid ⊢ B ∨ ℋ p = B ∨ ℋ p
22 2 1 21 mdsymlem7 ⊢ B ≠ 0 ℋ ∧ A ≠ 0 ℋ → A 𝑀 ℋ * B ↔ ∀ p ∈ HAtoms p ⊆ B ∨ ℋ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ r ∨ ℋ q ∧ r ⊆ B ∧ q ⊆ A
23 22 ancoms ⊢ A ≠ 0 ℋ ∧ B ≠ 0 ℋ → A 𝑀 ℋ * B ↔ ∀ p ∈ HAtoms p ⊆ B ∨ ℋ A → ∃ r ∈ HAtoms ∃ q ∈ HAtoms p ⊆ r ∨ ℋ q ∧ r ⊆ B ∧ q ⊆ A
24 19 20 23 3bitr4d ⊢ A ≠ 0 ℋ ∧ B ≠ 0 ℋ → B 𝑀 ℋ * A ↔ A 𝑀 ℋ * B