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 ˙ = K
paddasslem.j ˙ = join K
paddasslem.a A = Atoms K
paddasslem.p + ˙ = + 𝑃 K
Assertion paddasslem15 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r p X + ˙ Y + ˙ Z

Proof

Step Hyp Ref Expression
1 paddasslem.l ˙ = K
2 paddasslem.j ˙ = join K
3 paddasslem.a A = Atoms K
4 paddasslem.p + ˙ = + 𝑃 K
5 simpr2r K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r Y + ˙ Z
6 simpl1 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r K HL
7 6 hllatd K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r K Lat
8 simpl22 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r Y A
9 simpl23 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r Z A
10 simpl3 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r Y Z
11 1 2 3 4 elpaddn0 K Lat Y A Z A Y Z r Y + ˙ Z r A y Y z Z r ˙ y ˙ z
12 7 8 9 10 11 syl31anc K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r Y + ˙ Z r A y Y z Z r ˙ y ˙ z
13 5 12 mpbid K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z
14 simp11 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z K HL
15 simp12 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z X A Y A Z A
16 simp21 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z p A
17 simp31 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z r A
18 16 17 jca K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z p A r A
19 simp22l K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z x X
20 simp32l K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z y Y
21 simp32r K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z z Z
22 19 20 21 3jca K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z x X y Y z Z
23 simp23 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z p ˙ x ˙ r
24 simp33 K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z r ˙ y ˙ z
25 23 24 jca K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z p ˙ x ˙ r r ˙ y ˙ z
26 1 2 3 4 paddasslem14 K HL X A Y A Z A p A r A x X y Y z Z p ˙ x ˙ r r ˙ y ˙ z p X + ˙ Y + ˙ Z
27 14 15 18 22 25 26 syl32anc K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z p X + ˙ Y + ˙ Z
28 27 3expia K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z p X + ˙ Y + ˙ Z
29 28 3expd K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z p X + ˙ Y + ˙ Z
30 29 imp K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z p X + ˙ Y + ˙ Z
31 30 rexlimdvv K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z p X + ˙ Y + ˙ Z
32 31 expimpd K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r r A y Y z Z r ˙ y ˙ z p X + ˙ Y + ˙ Z
33 13 32 mpd K HL X A Y A Z A Y Z p A x X r Y + ˙ Z p ˙ x ˙ r p X + ˙ Y + ˙ Z