pl42N

Description: Law holding in a Hilbert lattice that fails in orthomodular lattice L42 (Figure 7 in MegPav2000 p. 2366). (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pl42.b	$⊢ B = {Base}_{K}$
	pl42.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pl42.j	$⊢ \underset{˙}{\lor} = join (K)$
	pl42.m	$⊢ \underset{˙}{\land} = meet (K)$
	pl42.o	$⊢ \underset{˙}{⊥} = oc (K)$
Assertion	pl42N	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to ((X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W)) \to ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))))$

Proof

Step	Hyp	Ref	Expression
1		pl42.b	$⊢ B = {Base}_{K}$
2		pl42.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		pl42.j	$⊢ \underset{˙}{\lor} = join (K)$
4		pl42.m	$⊢ \underset{˙}{\land} = meet (K)$
5		pl42.o	$⊢ \underset{˙}{⊥} = oc (K)$
6		eqid	$⊢ pmap (K) = pmap (K)$
7		eqid	$⊢ +_{𝑃} (K) = +_{𝑃} (K)$
8	1 2 3 4 5 6 7	pl42lem4N	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to ((X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W)) \to pmap (K) ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) \subseteq pmap (K) ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))))$
9		simpl1	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to K \in HL$
10	9	hllatd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to K \in Lat$
11		simpl2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to X \in B$
12		simpl3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to Y \in B$
13	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
14	10 11 12 13	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to X \underset{˙}{\lor} Y \in B$
15		simpr1	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to Z \in B$
16	1 4	latmcl	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B$
17	10 14 15 16	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B$
18		simpr2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to W \in B$
19	1 3	latjcl	$⊢ (K \in Lat \land (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B \land W \in B) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W \in B$
20	10 17 18 19	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W \in B$
21		simpr3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to V \in B$
22	1 4	latmcl	$⊢ (K \in Lat \land ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W \in B \land V \in B) \to (((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V \in B$
23	10 20 21 22	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V \in B$
24	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\lor} W \in B$
25	10 11 18 24	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to X \underset{˙}{\lor} W \in B$
26	1 3	latjcl	$⊢ (K \in Lat \land Y \in B \land V \in B) \to Y \underset{˙}{\lor} V \in B$
27	10 12 21 26	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to Y \underset{˙}{\lor} V \in B$
28	1 4	latmcl	$⊢ (K \in Lat \land X \underset{˙}{\lor} W \in B \land Y \underset{˙}{\lor} V \in B) \to (X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V) \in B$
29	10 25 27 28	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V) \in B$
30	1 3	latjcl	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land (X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V) \in B) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) \in B$
31	10 14 29 30	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) \in B$
32	1 2 6	pmaple	$⊢ (K \in HL \land (((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V \in B \land (X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) \in B) \to (((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))) \leftrightarrow pmap (K) ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) \subseteq pmap (K) ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))))$
33	9 23 31 32	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))) \leftrightarrow pmap (K) ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) \subseteq pmap (K) ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))))$
34	8 33	sylibrd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to ((X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W)) \to ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))))$

Metamath Proof Explorer

Theorem pl42N

Proof