Metamath Proof Explorer


Theorem paddasslem15

Description: Lemma for paddass . Use elpaddn0 to eliminate y and z from paddasslem14 . (Contributed by NM, 11-Jan-2012)

Ref Expression
Hypotheses paddasslem.l = ( le ‘ 𝐾 )
paddasslem.j = ( join ‘ 𝐾 )
paddasslem.a 𝐴 = ( Atoms ‘ 𝐾 )
paddasslem.p + = ( +𝑃𝐾 )
Assertion paddasslem15 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )

Proof

Step Hyp Ref Expression
1 paddasslem.l = ( le ‘ 𝐾 )
2 paddasslem.j = ( join ‘ 𝐾 )
3 paddasslem.a 𝐴 = ( Atoms ‘ 𝐾 )
4 paddasslem.p + = ( +𝑃𝐾 )
5 simpr2r ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → 𝑟 ∈ ( 𝑌 + 𝑍 ) )
6 simpl1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → 𝐾 ∈ HL )
7 6 hllatd ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → 𝐾 ∈ Lat )
8 simpl22 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → 𝑌𝐴 )
9 simpl23 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → 𝑍𝐴 )
10 simpl3 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) )
11 1 2 3 4 elpaddn0 ( ( ( 𝐾 ∈ Lat ∧ 𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) → ( 𝑟 ∈ ( 𝑌 + 𝑍 ) ↔ ( 𝑟𝐴 ∧ ∃ 𝑦𝑌𝑧𝑍 𝑟 ( 𝑦 𝑧 ) ) ) )
12 7 8 9 10 11 syl31anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → ( 𝑟 ∈ ( 𝑌 + 𝑍 ) ↔ ( 𝑟𝐴 ∧ ∃ 𝑦𝑌𝑧𝑍 𝑟 ( 𝑦 𝑧 ) ) ) )
13 5 12 mpbid ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → ( 𝑟𝐴 ∧ ∃ 𝑦𝑌𝑧𝑍 𝑟 ( 𝑦 𝑧 ) ) )
14 simp11 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝐾 ∈ HL )
15 simp12 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) )
16 simp21 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝𝐴 )
17 simp31 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑟𝐴 )
18 16 17 jca ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → ( 𝑝𝐴𝑟𝐴 ) )
19 simp22l ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑥𝑋 )
20 simp32l ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑦𝑌 )
21 simp32r ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑧𝑍 )
22 19 20 21 3jca ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) )
23 simp23 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ( 𝑥 𝑟 ) )
24 simp33 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑟 ( 𝑦 𝑧 ) )
25 23 24 jca ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) )
26 1 2 3 4 paddasslem14 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
27 14 15 18 22 25 26 syl32anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ∧ ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
28 27 3expia ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → ( ( 𝑟𝐴 ∧ ( 𝑦𝑌𝑧𝑍 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
29 28 3expd ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → ( 𝑟𝐴 → ( ( 𝑦𝑌𝑧𝑍 ) → ( 𝑟 ( 𝑦 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
30 29 imp ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) ∧ 𝑟𝐴 ) → ( ( 𝑦𝑌𝑧𝑍 ) → ( 𝑟 ( 𝑦 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) )
31 30 rexlimdvv ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) ∧ 𝑟𝐴 ) → ( ∃ 𝑦𝑌𝑧𝑍 𝑟 ( 𝑦 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
32 31 expimpd ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → ( ( 𝑟𝐴 ∧ ∃ 𝑦𝑌𝑧𝑍 𝑟 ( 𝑦 𝑧 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
33 13 32 mpd ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ( 𝑥𝑋𝑟 ∈ ( 𝑌 + 𝑍 ) ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )