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		simpl1	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to K \in HL$
4		simpl3	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Y \in S$
5		eqid	$⊢ Atoms (K) = Atoms (K)$
6	5 1	psubssat	$⊢ (K \in HL \land Y \in S) \to Y \subseteq Atoms (K)$
7	3 4 6	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)$
8		simpl2	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to X \in S$
9	5 1	psubssat	$⊢ (K \in HL \land X \in S) \to X \subseteq Atoms (K)$
10	3 8 9	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)$
11		simprl	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to Z \in S$
12	5 1	psubssat	$⊢ (K \in HL \land Z \in S) \to Z \subseteq Atoms (K)$
13	3 11 12	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)$
14	5 2	paddssat	$⊢ (K \in HL \land X \subseteq Atoms (K) \land Z \subseteq Atoms (K)) \to X \underset{˙}{+} Z \subseteq Atoms (K)$
15	3 10 13 14	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)$
16		simprr	$⊢ ((K \in HL \land X \in S \land Y \in S) \land (Z \in S \land W \in S)) \to W \in S$
17	1 2	paddclN	$⊢ (K \in HL \land Y \in S \land W \in S) \to Y \underset{˙}{+} W \in S$
18	3 4 16 17	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$
19	5 1	psubssat	$⊢ (K \in HL \land W \in S) \to W \subseteq Atoms (K)$
20	3 16 19	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)$
21	5 2	sspadd1	$⊢ (K \in HL \land Y \subseteq Atoms (K) \land W \subseteq Atoms (K)) \to Y \subseteq Y \underset{˙}{+} W$
22	3 7 20 21	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$
23	5 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)))$
24	23	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))$
25	3 7 15 18 22 24	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))$
26		incom	$⊢ (Y \underset{˙}{+} (X \underset{˙}{+} Z)) \cap (Y \underset{˙}{+} W) = (Y \underset{˙}{+} W) \cap (Y \underset{˙}{+} (X \underset{˙}{+} Z))$
27	25 26	eqtr3di	$⊢ ((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	15 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	5 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	3 10 7 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	5 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	3 10 7 13 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	5 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	3 10 7 13 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	5 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	3 10 7 20 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	5 1	psubssat	$⊢ (K \in HL \land Y \underset{˙}{+} W \in S) \to Y \underset{˙}{+} W \subseteq Atoms (K)$
44	3 18 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	3 8 11 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	3 4 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	5 2	sspadd1	$⊢ (K \in HL \land X \subseteq Atoms (K) \land Z \subseteq Atoms (K)) \to X \subseteq X \underset{˙}{+} Z$
50	3 10 13 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	5 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	3 15 7 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	5 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	3 10 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