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 𝐴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 ( 𝑝 ⊆ ( 𝑞 𝑟 ) ∧ ( 𝑞𝐴𝑟𝐵 ) ) ) ) )