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	⊢ 𝐴 ∈ Cℋ
	mdsymlem1.2	⊢ 𝐵 ∈ Cℋ
	mdsymlem1.3	⊢ 𝐶 = ( 𝐴 ∨ℋ 𝑝 )
Assertion	mdsymlem7	⊢ ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ ) → ( 𝐵 𝑀ℋ* 𝐴 ↔ ∀ 𝑝 ∈ HAtoms ( 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ∃ 𝑞 ∈ HAtoms ∃ 𝑟 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdsymlem1.1	⊢ 𝐴 ∈ Cℋ
2		mdsymlem1.2	⊢ 𝐵 ∈ Cℋ
3		mdsymlem1.3	⊢ 𝐶 = ( 𝐴 ∨ℋ 𝑝 )
4	1 2 3	mdsymlem4	⊢ ( 𝑝 ∈ HAtoms → ( ( 𝐵 𝑀ℋ* 𝐴 ∧ ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ ) ∧ 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ∃ 𝑞 ∈ HAtoms ∃ 𝑟 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) )
5	4	exp4d	⊢ ( 𝑝 ∈ HAtoms → ( 𝐵 𝑀ℋ* 𝐴 → ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ ) → ( 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ∃ 𝑞 ∈ HAtoms ∃ 𝑟 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) ) ) )
6	5	com13	⊢ ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ ) → ( 𝐵 𝑀ℋ* 𝐴 → ( 𝑝 ∈ HAtoms → ( 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ∃ 𝑞 ∈ HAtoms ∃ 𝑟 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) ) ) )
7	6	ralrimdv	⊢ ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ ) → ( 𝐵 𝑀ℋ* 𝐴 → ∀ 𝑝 ∈ HAtoms ( 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ∃ 𝑞 ∈ HAtoms ∃ 𝑟 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) ) )
8	1 2 3	mdsymlem6	⊢ ( ∀ 𝑝 ∈ HAtoms ( 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ∃ 𝑞 ∈ HAtoms ∃ 𝑟 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) → 𝐵 𝑀ℋ* 𝐴 )
9	7 8	impbid1	⊢ ( ( 𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ ) → ( 𝐵 𝑀ℋ* 𝐴 ↔ ∀ 𝑝 ∈ HAtoms ( 𝑝 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ∃ 𝑞 ∈ HAtoms ∃ 𝑟 ∈ HAtoms ( 𝑝 ⊆ ( 𝑞 ∨ℋ 𝑟 ) ∧ ( 𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵 ) ) ) ) )