dihmeetALTN

Description: Isomorphism H of a lattice meet. This version does not depend on the atomisticity of the constructed vector space. TODO: Delete? (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihmeetALT.b	$⊢ B = {Base}_{K}$
	dihmeetALT.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihmeetALT.h	$⊢ H = LHyp (K)$
	dihmeetALT.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihmeetALTN	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Proof

Step	Hyp	Ref	Expression
1		dihmeetALT.b	$⊢ B = {Base}_{K}$
2		dihmeetALT.m	$⊢ \underset{˙}{\land} = meet (K)$
3		dihmeetALT.h	$⊢ H = LHyp (K)$
4		dihmeetALT.i	$⊢ I = DIsoH (K) (W)$
5		simpl1l	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to K \in HL$
6	5	hllatd	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to K \in Lat$
7		simpl2	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to X \in B$
8		simpl3	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to Y \in B$
9	1 2	latmcom	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
10	6 7 8 9	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
11	10	fveq2d	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to I (X \underset{˙}{\land} Y) = I (Y \underset{˙}{\land} X)$
12		simpl1	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to (K \in HL \land W \in H)$
13		simpr	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to X \leq_{K} W$
14		eqid	$⊢ \leq_{K} = \leq_{K}$
15	1 14 2 3 4	dihmeetbN	$⊢ ((K \in HL \land W \in H) \land Y \in B \land (X \in B \land X \leq_{K} W)) \to I (Y \underset{˙}{\land} X) = I (Y) \cap I (X)$
16	12 8 7 13 15	syl112anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to I (Y \underset{˙}{\land} X) = I (Y) \cap I (X)$
17		incom	$⊢ I (Y) \cap I (X) = I (X) \cap I (Y)$
18	16 17	eqtrdi	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to I (Y \underset{˙}{\land} X) = I (X) \cap I (Y)$
19	11 18	eqtrd	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land X \leq_{K} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
20		simpll1	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land Y \leq_{K} W) \to (K \in HL \land W \in H)$
21		simpll2	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land Y \leq_{K} W) \to X \in B$
22		simpll3	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land Y \leq_{K} W) \to Y \in B$
23		simpr	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land Y \leq_{K} W) \to Y \leq_{K} W$
24	1 14 2 3 4	dihmeetbN	$⊢ ((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \leq_{K} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
25	20 21 22 23 24	syl112anc	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land Y \leq_{K} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
26	25	adantlr	$⊢ (((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W) \land Y \leq_{K} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
27		simp1l1	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W \land \neg Y \leq_{K} W) \to (K \in HL \land W \in H)$
28		simp1l2	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W \land \neg Y \leq_{K} W) \to X \in B$
29		simp1r	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W \land \neg Y \leq_{K} W) \to \neg X \leq_{K} W$
30		simp1l3	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W \land \neg Y \leq_{K} W) \to Y \in B$
31		simp3	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W \land \neg Y \leq_{K} W) \to \neg Y \leq_{K} W$
32	30 31	jca	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W \land \neg Y \leq_{K} W) \to (Y \in B \land \neg Y \leq_{K} W)$
33		simp2	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W \land \neg Y \leq_{K} W) \to (X \underset{˙}{\land} Y) \leq_{K} W$
34		eqid	$⊢ join (K) = join (K)$
35		eqid	$⊢ Atoms (K) = Atoms (K)$
36		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
37		eqid	$⊢ LSSum (DVecH (K) (W)) = LSSum (DVecH (K) (W))$
38	1 14 3 34 2 35 36 37 4	dihmeetlem20N	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \leq_{K} W) \land ((Y \in B \land \neg Y \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
39	27 28 29 32 33 38	syl122anc	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W \land \neg Y \leq_{K} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
40	39	3expa	$⊢ (((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W) \land \neg Y \leq_{K} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
41	26 40	pm2.61dan	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land (X \underset{˙}{\land} Y) \leq_{K} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
42		simpll1	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land \neg (X \underset{˙}{\land} Y) \leq_{K} W) \to (K \in HL \land W \in H)$
43		simpll2	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land \neg (X \underset{˙}{\land} Y) \leq_{K} W) \to X \in B$
44		simpll3	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land \neg (X \underset{˙}{\land} Y) \leq_{K} W) \to Y \in B$
45		simpr	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land \neg (X \underset{˙}{\land} Y) \leq_{K} W) \to \neg (X \underset{˙}{\land} Y) \leq_{K} W$
46	1 14 2 3 4	dihmeetcN	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \leq_{K} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
47	42 43 44 45 46	syl121anc	$⊢ ((((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \land \neg (X \underset{˙}{\land} Y) \leq_{K} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
48	41 47	pm2.61dan	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land \neg X \leq_{K} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
49	19 48	pm2.61dan	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Metamath Proof Explorer

Theorem dihmeetALTN

Proof