dihmeetlem16N

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

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

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem14.b	$⊢ B = {Base}_{K}$
2		dihmeetlem14.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetlem14.h	$⊢ H = LHyp (K)$
4		dihmeetlem14.j	$⊢ \underset{˙}{\lor} = join (K)$
5		dihmeetlem14.m	$⊢ \underset{˙}{\land} = meet (K)$
6		dihmeetlem14.a	$⊢ A = Atoms (K)$
7		dihmeetlem14.u	$⊢ U = DVecH (K) (W)$
8		dihmeetlem14.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
9		dihmeetlem14.i	$⊢ I = DIsoH (K) (W)$
10		eqid	$⊢ 0_{U} = 0_{U}$
11	1 2 3 4 5 6 7 8 9 10	dihmeetlem15N	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (r) \cap I (p) = \{0_{U}\}$
12	11	oveq2d	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} p) \underset{˙}{\oplus} (I (r) \cap I (p)) = I (Y \underset{˙}{\land} p) \underset{˙}{\oplus} \{0_{U}\}$
13		simpl1	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
14		simpl2	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to Y \in B$
15		simpl3l	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to p \in A$
16	1 6	atbase	$⊢ p \in A \to p \in B$
17	15 16	syl	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to p \in B$
18		simpr1	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to (r \in A \land \neg r \underset{˙}{\leq} W)$
19		simpr2	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to r \underset{˙}{\leq} Y$
20		simpr3	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to (Y \underset{˙}{\land} p) \underset{˙}{\leq} W$
21	1 2 3 4 5 6 7 8 9	dihmeetlem14N	$⊢ (((K \in HL \land W \in H) \land Y \in B \land p \in B) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} p) \underset{˙}{\oplus} (I (r) \cap I (p)) = I (Y) \cap I (p)$
22	13 14 17 18 19 20 21	syl33anc	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} p) \underset{˙}{\oplus} (I (r) \cap I (p)) = I (Y) \cap I (p)$
23	3 7 13	dvhlmod	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to U \in LMod$
24		simpl1l	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to K \in HL$
25	24	hllatd	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to K \in Lat$
26	1 5	latmcl	$⊢ (K \in Lat \land Y \in B \land p \in B) \to Y \underset{˙}{\land} p \in B$
27	25 14 17 26	syl3anc	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to Y \underset{˙}{\land} p \in B$
28		eqid	$⊢ LSubSp (U) = LSubSp (U)$
29	1 3 9 7 28	dihlss	$⊢ ((K \in HL \land W \in H) \land Y \underset{˙}{\land} p \in B) \to I (Y \underset{˙}{\land} p) \in LSubSp (U)$
30	13 27 29	syl2anc	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} p) \in LSubSp (U)$
31	28	lsssubg	$⊢ (U \in LMod \land I (Y \underset{˙}{\land} p) \in LSubSp (U)) \to I (Y \underset{˙}{\land} p) \in SubGrp (U)$
32	23 30 31	syl2anc	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} p) \in SubGrp (U)$
33	10 8	lsm01	$⊢ I (Y \underset{˙}{\land} p) \in SubGrp (U) \to I (Y \underset{˙}{\land} p) \underset{˙}{\oplus} \{0_{U}\} = I (Y \underset{˙}{\land} p)$
34	32 33	syl	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} p) \underset{˙}{\oplus} \{0_{U}\} = I (Y \underset{˙}{\land} p)$
35	12 22 34	3eqtr3rd	$⊢ (((K \in HL \land W \in H) \land Y \in B \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} p) = I (Y) \cap I (p)$

Metamath Proof Explorer

Theorem dihmeetlem16N

Proof