dihmeetlem19N

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	dihmeetlem19N	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

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		incom	$⊢ I (p) \cap I (Y) = I (Y) \cap I (p)$
11		eqid	$⊢ 0_{U} = 0_{U}$
12	1 2 3 4 5 6 7 8 9 11	dihmeetlem18N	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (Y) \cap I (p) = \{0_{U}\}$
13	10 12	syl5eq	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (p) \cap I (Y) = \{0_{U}\}$
14	13	oveq2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} (I (p) \cap I (Y)) = I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} \{0_{U}\}$
15		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
16		simpl2l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to X \in B$
17		simpl3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to Y \in B$
18		simpr1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to (p \in A \land \neg p \underset{˙}{\leq} W)$
19		simpr31	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to p \underset{˙}{\leq} X$
20		simpr33	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
21	1 2 3 4 5 6 7 8 9	dihmeetlem12N	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land ((p \in A \land \neg p \underset{˙}{\leq} W) \land p \underset{˙}{\leq} X \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} (I (p) \cap I (Y)) = I (X) \cap I (Y)$
22	15 16 17 18 19 20 21	syl33anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} (I (p) \cap I (Y)) = I (X) \cap I (Y)$
23	3 7 15	dvhlmod	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to U \in LMod$
24		simpl1l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to K \in HL$
25	24	hllatd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to K \in Lat$
26	1 5	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
27	25 16 17 26	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to X \underset{˙}{\land} Y \in B$
28		eqid	$⊢ LSubSp (U) = LSubSp (U)$
29	1 3 9 7 28	dihlss	$⊢ ((K \in HL \land W \in H) \land X \underset{˙}{\land} Y \in B) \to I (X \underset{˙}{\land} Y) \in LSubSp (U)$
30	15 27 29	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (X \underset{˙}{\land} Y) \in LSubSp (U)$
31	28	lsssubg	$⊢ (U \in LMod \land I (X \underset{˙}{\land} Y) \in LSubSp (U)) \to I (X \underset{˙}{\land} Y) \in SubGrp (U)$
32	23 30 31	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (X \underset{˙}{\land} Y) \in SubGrp (U)$
33	11 8	lsm01	$⊢ I (X \underset{˙}{\land} Y) \in SubGrp (U) \to I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} \{0_{U}\} = I (X \underset{˙}{\land} Y)$
34	32 33	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (X \underset{˙}{\land} Y) \underset{˙}{\oplus} \{0_{U}\} = I (X \underset{˙}{\land} Y)$
35	14 22 34	3eqtr3rd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \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 (p \underset{˙}{\leq} X \land r \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W))) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Metamath Proof Explorer

Theorem dihmeetlem19N

Proof