Metamath Proof Explorer


Theorem paddasslem14

Description: Lemma for paddass . Remove p =/= z , x =/= y , and -. r .<_ ( x .\/ y ) from antecedent of paddasslem10 , using paddasslem11 , paddasslem12 , and paddasslem13 . (Contributed by NM, 11-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 paddasslem.l = ( le ‘ 𝐾 )
2 paddasslem.j = ( join ‘ 𝐾 )
3 paddasslem.a 𝐴 = ( Atoms ‘ 𝐾 )
4 paddasslem.p + = ( +𝑃𝐾 )
5 1 2 3 4 paddasslem11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ) ∧ 𝑧𝑍 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
6 5 3ad2antr3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ) ∧ ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
7 6 ex ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ) → ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
8 7 adantrd ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
9 8 a1d ( ( ( 𝐾 ∈ HL ∧ 𝑝 = 𝑧 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ) → ( ( 𝑝𝐴𝑟𝐴 ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) )
10 9 exp31 ( 𝐾 ∈ HL → ( 𝑝 = 𝑧 → ( ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) → ( ( 𝑝𝐴𝑟𝐴 ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) ) )
11 3simpb ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥 = 𝑦 ) → ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) )
12 11 3anim1i ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥 = 𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) )
13 3simpc ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) → ( 𝑦𝑌𝑧𝑍 ) )
14 13 anim1i ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → ( ( 𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) )
15 1 2 3 4 paddasslem12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑥 = 𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
16 12 14 15 syl2an ( ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥 = 𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
17 16 3exp1 ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥 = 𝑦 ) → ( ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) → ( ( 𝑝𝐴𝑟𝐴 ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
18 17 3expia ( ( 𝐾 ∈ HL ∧ 𝑝𝑧 ) → ( 𝑥 = 𝑦 → ( ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) → ( ( 𝑝𝐴𝑟𝐴 ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) ) )
19 3simpa ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) → ( 𝐾 ∈ HL ∧ 𝑝𝑧 ) )
20 19 3anim1i ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑝𝑧 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) )
21 3simpa ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) → ( 𝑥𝑋𝑦𝑌 ) )
22 3simpa ( ( 𝑟 ( 𝑥 𝑦 ) ∧ 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) → ( 𝑟 ( 𝑥 𝑦 ) ∧ 𝑝 ( 𝑥 𝑟 ) ) )
23 21 22 anim12i ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑟 ( 𝑥 𝑦 ) ∧ 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → ( ( 𝑥𝑋𝑦𝑌 ) ∧ ( 𝑟 ( 𝑥 𝑦 ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) )
24 1 2 3 4 paddasslem13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌 ) ∧ ( 𝑟 ( 𝑥 𝑦 ) ∧ 𝑝 ( 𝑥 𝑟 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
25 20 23 24 syl2an ( ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑟 ( 𝑥 𝑦 ) ∧ 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
26 25 expr ( ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ) → ( ( 𝑟 ( 𝑥 𝑦 ) ∧ 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
27 26 3expd ( ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ) → ( 𝑟 ( 𝑥 𝑦 ) → ( 𝑝 ( 𝑥 𝑟 ) → ( 𝑟 ( 𝑦 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
28 1 2 3 4 paddasslem10 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
29 28 expr ( ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ) → ( ( ¬ 𝑟 ( 𝑥 𝑦 ) ∧ 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
30 29 3expd ( ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ) → ( ¬ 𝑟 ( 𝑥 𝑦 ) → ( 𝑝 ( 𝑥 𝑟 ) → ( 𝑟 ( 𝑦 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
31 27 30 pm2.61d ( ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ) → ( 𝑝 ( 𝑥 𝑟 ) → ( 𝑟 ( 𝑦 𝑧 ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) )
32 31 impd ( ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ) → ( ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
33 32 expimpd ( ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
34 33 3exp ( ( 𝐾 ∈ HL ∧ 𝑝𝑧𝑥𝑦 ) → ( ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) → ( ( 𝑝𝐴𝑟𝐴 ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
35 34 3expia ( ( 𝐾 ∈ HL ∧ 𝑝𝑧 ) → ( 𝑥𝑦 → ( ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) → ( ( 𝑝𝐴𝑟𝐴 ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) ) )
36 18 35 pm2.61dne ( ( 𝐾 ∈ HL ∧ 𝑝𝑧 ) → ( ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) → ( ( 𝑝𝐴𝑟𝐴 ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
37 36 ex ( 𝐾 ∈ HL → ( 𝑝𝑧 → ( ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) → ( ( 𝑝𝐴𝑟𝐴 ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) ) )
38 10 37 pm2.61dne ( 𝐾 ∈ HL → ( ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) → ( ( 𝑝𝐴𝑟𝐴 ) → ( ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) ) ) )
39 38 3imp1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( 𝑝𝐴𝑟𝐴 ) ) ∧ ( ( 𝑥𝑋𝑦𝑌𝑧𝑍 ) ∧ ( 𝑝 ( 𝑥 𝑟 ) ∧ 𝑟 ( 𝑦 𝑧 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )