pmod2iN

Description: Dual of the modular law. (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmod.a	$⊢ A = Atoms (K)$
	pmod.s	$⊢ S = PSubSp (K)$
	pmod.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	pmod2iN	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to (Z \subseteq X \to (X \cap Y) \underset{˙}{+} Z = X \cap (Y \underset{˙}{+} Z))$

Proof

Step	Hyp	Ref	Expression
1		pmod.a	$⊢ A = Atoms (K)$
2		pmod.s	$⊢ S = PSubSp (K)$
3		pmod.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
4		incom	$⊢ X \cap Y = Y \cap X$
5	4	oveq1i	$⊢ (X \cap Y) \underset{˙}{+} Z = (Y \cap X) \underset{˙}{+} Z$
6		hllat	$⊢ K \in HL \to K \in Lat$
7	6	3ad2ant1	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to K \in Lat$
8		simp22	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to Y \subseteq A$
9		ssinss1	$⊢ Y \subseteq A \to Y \cap X \subseteq A$
10	8 9	syl	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to Y \cap X \subseteq A$
11		simp23	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to Z \subseteq A$
12	1 3	paddcom	$⊢ (K \in Lat \land Y \cap X \subseteq A \land Z \subseteq A) \to (Y \cap X) \underset{˙}{+} Z = Z \underset{˙}{+} (Y \cap X)$
13	7 10 11 12	syl3anc	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to (Y \cap X) \underset{˙}{+} Z = Z \underset{˙}{+} (Y \cap X)$
14	5 13	syl5eq	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to (X \cap Y) \underset{˙}{+} Z = Z \underset{˙}{+} (Y \cap X)$
15		simp21	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to X \in S$
16	11 8 15	3jca	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to (Z \subseteq A \land Y \subseteq A \land X \in S)$
17	1 2 3	pmod1i	$⊢ (K \in HL \land (Z \subseteq A \land Y \subseteq A \land X \in S)) \to (Z \subseteq X \to (Z \underset{˙}{+} Y) \cap X = Z \underset{˙}{+} (Y \cap X))$
18	17	3impia	$⊢ (K \in HL \land (Z \subseteq A \land Y \subseteq A \land X \in S) \land Z \subseteq X) \to (Z \underset{˙}{+} Y) \cap X = Z \underset{˙}{+} (Y \cap X)$
19	16 18	syld3an2	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to (Z \underset{˙}{+} Y) \cap X = Z \underset{˙}{+} (Y \cap X)$
20	1 3	paddcom	$⊢ (K \in Lat \land Z \subseteq A \land Y \subseteq A) \to Z \underset{˙}{+} Y = Y \underset{˙}{+} Z$
21	7 11 8 20	syl3anc	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to Z \underset{˙}{+} Y = Y \underset{˙}{+} Z$
22	21	ineq1d	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to (Z \underset{˙}{+} Y) \cap X = (Y \underset{˙}{+} Z) \cap X$
23	14 19 22	3eqtr2d	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to (X \cap Y) \underset{˙}{+} Z = (Y \underset{˙}{+} Z) \cap X$
24		incom	$⊢ (Y \underset{˙}{+} Z) \cap X = X \cap (Y \underset{˙}{+} Z)$
25	23 24	eqtrdi	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A) \land Z \subseteq X) \to (X \cap Y) \underset{˙}{+} Z = X \cap (Y \underset{˙}{+} Z)$
26	25	3expia	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to (Z \subseteq X \to (X \cap Y) \underset{˙}{+} Z = X \cap (Y \underset{˙}{+} Z))$

Metamath Proof Explorer

Theorem pmod2iN

Proof