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	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	paddasslem17	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land \neg ((X \neq \emptyset \land Y \underset{˙}{+} Z \neq \emptyset) \land (Y \neq \emptyset \land Z \neq \emptyset))) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$

Proof

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

Metamath Proof Explorer

Theorem paddasslem17

Proof