dihmeetlem9N

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihmeetlem9.b	$⊢ B = {Base}_{K}$
	dihmeetlem9.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihmeetlem9.h	$⊢ H = LHyp (K)$
	dihmeetlem9.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihmeetlem9.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihmeetlem9.a	$⊢ A = Atoms (K)$
	dihmeetlem9.u	$⊢ U = DVecH (K) (W)$
	dihmeetlem9.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihmeetlem9.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihmeetlem9N	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to (I (p) \underset{˙}{\oplus} I (X \underset{˙}{\land} Y)) \cap I (Y) = I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} (I (p) \cap I (Y))$

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem9.b	$⊢ B = {Base}_{K}$
2		dihmeetlem9.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetlem9.h	$⊢ H = LHyp (K)$
4		dihmeetlem9.j	$⊢ \underset{˙}{\lor} = join (K)$
5		dihmeetlem9.m	$⊢ \underset{˙}{\land} = meet (K)$
6		dihmeetlem9.a	$⊢ A = Atoms (K)$
7		dihmeetlem9.u	$⊢ U = DVecH (K) (W)$
8		dihmeetlem9.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
9		dihmeetlem9.i	$⊢ I = DIsoH (K) (W)$
10		simp1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to (K \in HL \land W \in H)$
11	3 7 10	dvhlmod	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to U \in LMod$
12		eqid	$⊢ LSubSp (U) = LSubSp (U)$
13	12	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
14	11 13	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to LSubSp (U) \subseteq SubGrp (U)$
15		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to K \in HL$
16	15	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to K \in Lat$
17		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to X \in B$
18		simp2r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to Y \in B$
19	1 5	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
20	16 17 18 19	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to X \underset{˙}{\land} Y \in B$
21	1 3 9 7 12	dihlss	$⊢ ((K \in HL \land W \in H) \land X \underset{˙}{\land} Y \in B) \to I (X \underset{˙}{\land} Y) \in LSubSp (U)$
22	10 20 21	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to I (X \underset{˙}{\land} Y) \in LSubSp (U)$
23	14 22	sseldd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to I (X \underset{˙}{\land} Y) \in SubGrp (U)$
24	1 6	atbase	$⊢ p \in A \to p \in B$
25	24	3ad2ant3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to p \in B$
26	1 3 9 7 12	dihlss	$⊢ ((K \in HL \land W \in H) \land p \in B) \to I (p) \in LSubSp (U)$
27	10 25 26	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to I (p) \in LSubSp (U)$
28	14 27	sseldd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to I (p) \in SubGrp (U)$
29	1 3 9 7 12	dihlss	$⊢ ((K \in HL \land W \in H) \land Y \in B) \to I (Y) \in LSubSp (U)$
30	10 18 29	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to I (Y) \in LSubSp (U)$
31	14 30	sseldd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to I (Y) \in SubGrp (U)$
32	1 2 5	latmle2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
33	16 17 18 32	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
34	1 2 3 9	dihord	$⊢ ((K \in HL \land W \in H) \land X \underset{˙}{\land} Y \in B \land Y \in B) \to (I (X \underset{˙}{\land} Y) \subseteq I (Y) \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y)$
35	10 20 18 34	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to (I (X \underset{˙}{\land} Y) \subseteq I (Y) \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y)$
36	33 35	mpbird	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to I (X \underset{˙}{\land} Y) \subseteq I (Y)$
37	8	lsmmod	$⊢ ((I (X \underset{˙}{\land} Y) \in SubGrp (U) \land I (p) \in SubGrp (U) \land I (Y) \in SubGrp (U)) \land I (X \underset{˙}{\land} Y) \subseteq I (Y)) \to I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} (I (p) \cap I (Y)) = (I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} I (p)) \cap I (Y)$
38	23 28 31 36 37	syl31anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} (I (p) \cap I (Y)) = (I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} I (p)) \cap I (Y)$
39		lmodabl	$⊢ U \in LMod \to U \in Abel$
40	11 39	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to U \in Abel$
41	8	lsmcom	$⊢ (U \in Abel \land I (X \underset{˙}{\land} Y) \in SubGrp (U) \land I (p) \in SubGrp (U)) \to I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} I (p) = I (p) \underset{˙}{\oplus} I (X \underset{˙}{\land} Y)$
42	40 23 28 41	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} I (p) = I (p) \underset{˙}{\oplus} I (X \underset{˙}{\land} Y)$
43	42	ineq1d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to (I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} I (p)) \cap I (Y) = (I (p) \underset{˙}{\oplus} I (X \underset{˙}{\land} Y)) \cap I (Y)$
44	38 43	eqtr2d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land p \in A) \to (I (p) \underset{˙}{\oplus} I (X \underset{˙}{\land} Y)) \cap I (Y) = I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} (I (p) \cap I (Y))$

Metamath Proof Explorer

Theorem dihmeetlem9N

Proof