Metamath Proof Explorer


Theorem paddasslem9

Description: Lemma for paddass . Combine paddasslem7 and paddasslem8 . (Contributed by NM, 9-Jan-2012)

Ref Expression
Hypotheses paddasslem.l = ( le ‘ 𝐾 )
paddasslem.j = ( join ‘ 𝐾 )
paddasslem.a 𝐴 = ( Atoms ‘ 𝐾 )
paddasslem.p + = ( +𝑃𝐾 )
Assertion paddasslem9 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )

Proof

Step Hyp Ref Expression
1 paddasslem.l = ( le ‘ 𝐾 )
2 paddasslem.j = ( join ‘ 𝐾 )
3 paddasslem.a 𝐴 = ( Atoms ‘ 𝐾 )
4 paddasslem.p + = ( +𝑃𝐾 )
5 simpl1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → 𝐾 ∈ HL )
6 simpl2 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) )
7 simpl3l ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → 𝑝𝐴 )
8 simpr31 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → 𝑠𝐴 )
9 7 8 jca ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → ( 𝑝𝐴𝑠𝐴 ) )
10 simpr1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) )
11 simpr32 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → 𝑠 ( 𝑥 𝑦 ) )
12 simpl3r ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → 𝑟𝐴 )
13 7 12 8 3jca ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → ( 𝑝𝐴𝑟𝐴𝑠𝐴 ) )
14 an6 ( ( ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ) ↔ ( ( 𝑋𝐴𝑥𝑋 ) ∧ ( 𝑌𝐴𝑦𝑌 ) ∧ ( 𝑍𝐴𝑧𝑍 ) ) )
15 ssel2 ( ( 𝑋𝐴𝑥𝑋 ) → 𝑥𝐴 )
16 ssel2 ( ( 𝑌𝐴𝑦𝑌 ) → 𝑦𝐴 )
17 ssel2 ( ( 𝑍𝐴𝑧𝑍 ) → 𝑧𝐴 )
18 15 16 17 3anim123i ( ( ( 𝑋𝐴𝑥𝑋 ) ∧ ( 𝑌𝐴𝑦𝑌 ) ∧ ( 𝑍𝐴𝑧𝑍 ) ) → ( 𝑥𝐴𝑦𝐴𝑧𝐴 ) )
19 14 18 sylbi ( ( ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ) → ( 𝑥𝐴𝑦𝐴𝑧𝐴 ) )
20 19 3ad2antl2 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ) → ( 𝑥𝐴𝑦𝐴𝑧𝐴 ) )
21 20 3ad2antr1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → ( 𝑥𝐴𝑦𝐴𝑧𝐴 ) )
22 simpr2l ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → ¬ 𝑟 ( 𝑥 𝑦 ) )
23 simpr2r ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → 𝑟 ( 𝑦 𝑧 ) )
24 22 23 11 3jca ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ∧ 𝑠 ( 𝑥 𝑦 ) ) )
25 simpr33 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → 𝑠 ( 𝑝 𝑧 ) )
26 1 2 3 paddasslem7 ( ( ( 𝐾 ∈ HL ∧ ( 𝑝𝐴𝑟𝐴𝑠𝐴 ) ∧ ( 𝑥𝐴𝑦𝐴𝑧𝐴 ) ) ∧ ( ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ∧ 𝑠 ( 𝑥 𝑦 ) ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) → 𝑝 ( 𝑠 𝑧 ) )
27 5 13 21 24 25 26 syl32anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → 𝑝 ( 𝑠 𝑧 ) )
28 1 2 3 4 paddasslem8 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑠𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ 𝑠 ( 𝑥 𝑦 ) ∧ 𝑝 ( 𝑠 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
29 5 6 9 10 11 27 28 syl33anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ∧ ( 𝑠𝐴𝑠 ( 𝑥 𝑦 ) ∧ 𝑠 ( 𝑝 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )