pmodl42N

Description: Lemma derived from modular law. (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmodl42.s	$⊢ S = PSubSp (K)$
	pmodl42.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	pmodl42N	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to ((X \underset{˙}{+} Y) \underset{˙}{+} Z) \cap ((X \underset{˙}{+} Y) \underset{˙}{+} W) = (X \underset{˙}{+} Y) \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W))$

Proof

Step	Hyp	Ref	Expression
1		pmodl42.s	$⊢ S = PSubSp (K)$
2		pmodl42.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		incom	$⊢ (Y \underset{˙}{+} (X \underset{˙}{+} Z)) \cap (Y \underset{˙}{+} W) = (Y \underset{˙}{+} W) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z))$
4		simpl1	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to K \in HL$
5		simpl3	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Y \in S$
6		eqid	$⊢ Atoms (K) = Atoms (K)$
7	6 1	psubssat	$⊢ (K \in HL \land Y \in S) \to Y \subseteq Atoms (K)$
8	4 5 7	syl2anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Y \subseteq Atoms (K)$
9		simpl2	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to X \in S$
10	6 1	psubssat	$⊢ (K \in HL \land X \in S) \to X \subseteq Atoms (K)$
11	4 9 10	syl2anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to X \subseteq Atoms (K)$
12		simprl	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Z \in S$
13	6 1	psubssat	$⊢ (K \in HL \land Z \in S) \to Z \subseteq Atoms (K)$
14	4 12 13	syl2anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Z \subseteq Atoms (K)$
15	6 2	paddssat	$⊢ (K \in HL \land X \subseteq Atoms (K) \land Z \subseteq Atoms (K)) \to X \underset{˙}{+} Z \subseteq Atoms (K)$
16	4 11 14 15	syl3anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to X \underset{˙}{+} Z \subseteq Atoms (K)$
17		simprr	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to W \in S$
18	1 2	paddclN	$⊢ (K \in HL \land Y \in S \land W \in S) \to Y \underset{˙}{+} W \in S$
19	4 5 17 18	syl3anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Y \underset{˙}{+} W \in S$
20	6 1	psubssat	$⊢ (K \in HL \land W \in S) \to W \subseteq Atoms (K)$
21	4 17 20	syl2anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to W \subseteq Atoms (K)$
22	6 2	sspadd1	$⊢ (K \in HL \land Y \subseteq Atoms (K) \land W \subseteq Atoms (K)) \to Y \subseteq Y \underset{˙}{+} W$
23	4 8 21 22	syl3anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Y \subseteq Y \underset{˙}{+} W$
24	6 1 2	pmod1i	$⊢ (K \in HL \land (Y \subseteq Atoms (K) \land X \underset{˙}{+} Z \subseteq Atoms (K) \land Y \underset{˙}{+} W \in S)) \to (Y \subseteq Y \underset{˙}{+} W \to (Y \underset{˙}{+} (X \underset{˙}{+} Z)) \cap (Y \underset{˙}{+} W) = Y \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W)))$
25	24	3impia	$⊢ (K \in HL \land (Y \subseteq Atoms (K) \land X \underset{˙}{+} Z \subseteq Atoms (K) \land Y \underset{˙}{+} W \in S) \land Y \subseteq Y \underset{˙}{+} W) \to (Y \underset{˙}{+} (X \underset{˙}{+} Z)) \cap (Y \underset{˙}{+} W) = Y \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W))$
26	4 8 16 19 23 25	syl131anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to (Y \underset{˙}{+} (X \underset{˙}{+} Z)) \cap (Y \underset{˙}{+} W) = Y \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W))$
27	3 26	syl5reqr	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Y \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W)) = (Y \underset{˙}{+} W) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z))$
28	27	oveq2d	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to X \underset{˙}{+} (Y \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W))) = X \underset{˙}{+} ((Y \underset{˙}{+} W) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z)))$
29		ssinss1	$⊢ X \underset{˙}{+} Z \subseteq Atoms (K) \to (X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W) \subseteq Atoms (K)$
30	16 29	syl	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to (X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W) \subseteq Atoms (K)$
31	6 2	paddass	$⊢ (K \in HL \land (X \subseteq Atoms (K) \land Y \subseteq Atoms (K) \land (X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W) \subseteq Atoms (K))) \to (X \underset{˙}{+} Y) \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W)) = X \underset{˙}{+} (Y \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W)))$
32	4 11 8 30 31	syl13anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to (X \underset{˙}{+} Y) \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W)) = X \underset{˙}{+} (Y \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W)))$
33	6 2	paddass	$⊢ (K \in HL \land (X \subseteq Atoms (K) \land Y \subseteq Atoms (K) \land Z \subseteq Atoms (K))) \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = X \underset{˙}{+} (Y \underset{˙}{+} Z)$
34	4 11 8 14 33	syl13anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = X \underset{˙}{+} (Y \underset{˙}{+} Z)$
35	6 2	padd12N	$⊢ (K \in HL \land (X \subseteq Atoms (K) \land Y \subseteq Atoms (K) \land Z \subseteq Atoms (K))) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) = Y \underset{˙}{+} (X \underset{˙}{+} Z)$
36	4 11 8 14 35	syl13anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) = Y \underset{˙}{+} (X \underset{˙}{+} Z)$
37	34 36	eqtrd	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = Y \underset{˙}{+} (X \underset{˙}{+} Z)$
38	6 2	paddass	$⊢ (K \in HL \land (X \subseteq Atoms (K) \land Y \subseteq Atoms (K) \land W \subseteq Atoms (K))) \to (X \underset{˙}{+} Y) \underset{˙}{+} W = X \underset{˙}{+} (Y \underset{˙}{+} W)$
39	4 11 8 21 38	syl13anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to (X \underset{˙}{+} Y) \underset{˙}{+} W = X \underset{˙}{+} (Y \underset{˙}{+} W)$
40	37 39	ineq12d	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to ((X \underset{˙}{+} Y) \underset{˙}{+} Z) \cap ((X \underset{˙}{+} Y) \underset{˙}{+} W) = (Y \underset{˙}{+} (X \underset{˙}{+} Z)) \cap (X \underset{˙}{+} (Y \underset{˙}{+} W))$
41		incom	$⊢ (Y \underset{˙}{+} (X \underset{˙}{+} Z)) \cap (X \underset{˙}{+} (Y \underset{˙}{+} W)) = (X \underset{˙}{+} (Y \underset{˙}{+} W)) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z))$
42	40 41	eqtrdi	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to ((X \underset{˙}{+} Y) \underset{˙}{+} Z) \cap ((X \underset{˙}{+} Y) \underset{˙}{+} W) = (X \underset{˙}{+} (Y \underset{˙}{+} W)) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z))$
43	6 1	psubssat	$⊢ (K \in HL \land Y \underset{˙}{+} W \in S) \to Y \underset{˙}{+} W \subseteq Atoms (K)$
44	4 19 43	syl2anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Y \underset{˙}{+} W \subseteq Atoms (K)$
45	1 2	paddclN	$⊢ (K \in HL \land X \in S \land Z \in S) \to X \underset{˙}{+} Z \in S$
46	4 9 12 45	syl3anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to X \underset{˙}{+} Z \in S$
47	1 2	paddclN	$⊢ (K \in HL \land Y \in S \land X \underset{˙}{+} Z \in S) \to Y \underset{˙}{+} (X \underset{˙}{+} Z) \in S$
48	4 5 46 47	syl3anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Y \underset{˙}{+} (X \underset{˙}{+} Z) \in S$
49	6 2	sspadd1	$⊢ (K \in HL \land X \subseteq Atoms (K) \land Z \subseteq Atoms (K)) \to X \subseteq X \underset{˙}{+} Z$
50	4 11 14 49	syl3anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to X \subseteq X \underset{˙}{+} Z$
51	6 2	sspadd2	$⊢ (K \in HL \land X \underset{˙}{+} Z \subseteq Atoms (K) \land Y \subseteq Atoms (K)) \to X \underset{˙}{+} Z \subseteq Y \underset{˙}{+} (X \underset{˙}{+} Z)$
52	4 16 8 51	syl3anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to X \underset{˙}{+} Z \subseteq Y \underset{˙}{+} (X \underset{˙}{+} Z)$
53	50 52	sstrd	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to X \subseteq Y \underset{˙}{+} (X \underset{˙}{+} Z)$
54	6 1 2	pmod1i	$⊢ (K \in HL \land (X \subseteq Atoms (K) \land Y \underset{˙}{+} W \subseteq Atoms (K) \land Y \underset{˙}{+} (X \underset{˙}{+} Z) \in S)) \to (X \subseteq Y \underset{˙}{+} (X \underset{˙}{+} Z) \to (X \underset{˙}{+} (Y \underset{˙}{+} W)) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z)) = X \underset{˙}{+} ((Y \underset{˙}{+} W) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z))))$
55	54	3impia	$⊢ (K \in HL \land (X \subseteq Atoms (K) \land Y \underset{˙}{+} W \subseteq Atoms (K) \land Y \underset{˙}{+} (X \underset{˙}{+} Z) \in S) \land X \subseteq Y \underset{˙}{+} (X \underset{˙}{+} Z)) \to (X \underset{˙}{+} (Y \underset{˙}{+} W)) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z)) = X \underset{˙}{+} ((Y \underset{˙}{+} W) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z)))$
56	4 11 44 48 53 55	syl131anc	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to (X \underset{˙}{+} (Y \underset{˙}{+} W)) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z)) = X \underset{˙}{+} ((Y \underset{˙}{+} W) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z)))$
57	42 56	eqtrd	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to ((X \underset{˙}{+} Y) \underset{˙}{+} Z) \cap ((X \underset{˙}{+} Y) \underset{˙}{+} W) = X \underset{˙}{+} ((Y \underset{˙}{+} W) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z)))$
58	28 32 57	3eqtr4rd	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to ((X \underset{˙}{+} Y) \underset{˙}{+} Z) \cap ((X \underset{˙}{+} Y) \underset{˙}{+} W) = (X \underset{˙}{+} Y) \underset{˙}{+} ((X \underset{˙}{+} Z) \cap (Y \underset{˙}{+} W))$

Metamath Proof Explorer

Theorem pmodl42N

Proof