Metamath Proof Explorer


Theorem paddasslem17

Description: Lemma for paddass . The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012)

Ref Expression
Hypotheses paddass.a A = Atoms K
paddass.p + ˙ = + 𝑃 K
Assertion paddasslem17 K HL X A Y A Z A ¬ X Y + ˙ Z Y Z X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z

Proof

Step Hyp Ref Expression
1 paddass.a A = Atoms K
2 paddass.p + ˙ = + 𝑃 K
3 ianor ¬ X Y + ˙ Z Y Z ¬ X Y + ˙ Z ¬ Y Z
4 ianor ¬ X Y + ˙ Z ¬ X ¬ Y + ˙ Z
5 nne ¬ X X =
6 nne ¬ Y + ˙ Z Y + ˙ Z =
7 5 6 orbi12i ¬ X ¬ Y + ˙ Z X = Y + ˙ Z =
8 4 7 bitri ¬ X Y + ˙ Z X = Y + ˙ Z =
9 ianor ¬ Y Z ¬ Y ¬ Z
10 nne ¬ Y Y =
11 nne ¬ Z Z =
12 10 11 orbi12i ¬ Y ¬ Z Y = Z =
13 9 12 bitri ¬ Y Z Y = Z =
14 8 13 orbi12i ¬ X Y + ˙ Z ¬ Y Z X = Y + ˙ Z = Y = Z =
15 3 14 bitri ¬ X Y + ˙ Z Y Z X = Y + ˙ Z = Y = Z =
16 1 2 paddssat K HL Y A Z A Y + ˙ Z A
17 16 3adant3r1 K HL X A Y A Z A Y + ˙ Z A
18 1 2 padd02 K HL Y + ˙ Z A + ˙ Y + ˙ Z = Y + ˙ Z
19 17 18 syldan K HL X A Y A Z A + ˙ Y + ˙ Z = Y + ˙ Z
20 1 2 padd02 K HL Y A + ˙ Y = Y
21 20 3ad2antr2 K HL X A Y A Z A + ˙ Y = Y
22 21 oveq1d K HL X A Y A Z A + ˙ Y + ˙ Z = Y + ˙ Z
23 19 22 eqtr4d K HL X A Y A Z A + ˙ Y + ˙ Z = + ˙ Y + ˙ Z
24 oveq1 X = X + ˙ Y + ˙ Z = + ˙ Y + ˙ Z
25 oveq1 X = X + ˙ Y = + ˙ Y
26 25 oveq1d X = X + ˙ Y + ˙ Z = + ˙ Y + ˙ Z
27 24 26 eqeq12d X = X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z + ˙ Y + ˙ Z = + ˙ Y + ˙ Z
28 23 27 syl5ibrcom K HL X A Y A Z A X = X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z
29 eqimss X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z
30 28 29 syl6 K HL X A Y A Z A X = X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z
31 1 2 padd01 K HL X A X + ˙ = X
32 31 3ad2antr1 K HL X A Y A Z A X + ˙ = X
33 1 2 sspadd1 K HL X A Y A X X + ˙ Y
34 33 3adant3r3 K HL X A Y A Z A X X + ˙ Y
35 simpl K HL X A Y A Z A K HL
36 1 2 paddssat K HL X A Y A X + ˙ Y A
37 36 3adant3r3 K HL X A Y A Z A X + ˙ Y A
38 simpr3 K HL X A Y A Z A Z A
39 1 2 sspadd1 K HL X + ˙ Y A Z A X + ˙ Y X + ˙ Y + ˙ Z
40 35 37 38 39 syl3anc K HL X A Y A Z A X + ˙ Y X + ˙ Y + ˙ Z
41 34 40 sstrd K HL X A Y A Z A X X + ˙ Y + ˙ Z
42 32 41 eqsstrd K HL X A Y A Z A X + ˙ X + ˙ Y + ˙ Z
43 oveq2 Y + ˙ Z = X + ˙ Y + ˙ Z = X + ˙
44 43 sseq1d Y + ˙ Z = X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z X + ˙ X + ˙ Y + ˙ Z
45 42 44 syl5ibrcom K HL X A Y A Z A Y + ˙ Z = X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z
46 30 45 jaod K HL X A Y A Z A X = Y + ˙ Z = X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z
47 1 2 padd02 K HL Z A + ˙ Z = Z
48 47 3ad2antr3 K HL X A Y A Z A + ˙ Z = Z
49 48 oveq2d K HL X A Y A Z A X + ˙ + ˙ Z = X + ˙ Z
50 32 oveq1d K HL X A Y A Z A X + ˙ + ˙ Z = X + ˙ Z
51 49 50 eqtr4d K HL X A Y A Z A X + ˙ + ˙ Z = X + ˙ + ˙ Z
52 oveq1 Y = Y + ˙ Z = + ˙ Z
53 52 oveq2d Y = X + ˙ Y + ˙ Z = X + ˙ + ˙ Z
54 oveq2 Y = X + ˙ Y = X + ˙
55 54 oveq1d Y = X + ˙ Y + ˙ Z = X + ˙ + ˙ Z
56 53 55 eqeq12d Y = X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z X + ˙ + ˙ Z = X + ˙ + ˙ Z
57 51 56 syl5ibrcom K HL X A Y A Z A Y = X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z
58 1 2 padd01 K HL Y A Y + ˙ = Y
59 58 3ad2antr2 K HL X A Y A Z A Y + ˙ = Y
60 59 oveq2d K HL X A Y A Z A X + ˙ Y + ˙ = X + ˙ Y
61 1 2 padd01 K HL X + ˙ Y A X + ˙ Y + ˙ = X + ˙ Y
62 37 61 syldan K HL X A Y A Z A X + ˙ Y + ˙ = X + ˙ Y
63 60 62 eqtr4d K HL X A Y A Z A X + ˙ Y + ˙ = X + ˙ Y + ˙
64 oveq2 Z = Y + ˙ Z = Y + ˙
65 64 oveq2d Z = X + ˙ Y + ˙ Z = X + ˙ Y + ˙
66 oveq2 Z = X + ˙ Y + ˙ Z = X + ˙ Y + ˙
67 65 66 eqeq12d Z = X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z X + ˙ Y + ˙ = X + ˙ Y + ˙
68 63 67 syl5ibrcom K HL X A Y A Z A Z = X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z
69 57 68 jaod K HL X A Y A Z A Y = Z = X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z
70 69 29 syl6 K HL X A Y A Z A Y = Z = X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z
71 46 70 jaod K HL X A Y A Z A X = Y + ˙ Z = Y = Z = X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z
72 15 71 syl5bi K HL X A Y A Z A ¬ X Y + ˙ Z Y Z X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z
73 72 3impia K HL X A Y A Z A ¬ X Y + ˙ Z Y Z X + ˙ Y + ˙ Z X + ˙ Y + ˙ Z