islvol2aN

Description: The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	islvol2a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	islvol2a.j	$⊢ \underset{˙}{\lor} = join (K)$
	islvol2a.a	$⊢ A = Atoms (K)$
	islvol2a.v	$⊢ V = LVols (K)$
Assertion	islvol2aN	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V \leftrightarrow (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)))$

Proof

Step	Hyp	Ref	Expression
1		islvol2a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		islvol2a.j	$⊢ \underset{˙}{\lor} = join (K)$
3		islvol2a.a	$⊢ A = Atoms (K)$
4		islvol2a.v	$⊢ V = LVols (K)$
5		oveq1	$⊢ P = Q \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} Q$
6		simpl1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to K \in HL$
7		simpl3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to Q \in A$
8	2 3	hlatjidm	$⊢ (K \in HL \land Q \in A) \to Q \underset{˙}{\lor} Q = Q$
9	6 7 8	syl2anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to Q \underset{˙}{\lor} Q = Q$
10	5 9	sylan9eqr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \land P = Q) \to P \underset{˙}{\lor} Q = Q$
11	10	oveq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \land P = Q) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
12	11	oveq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \land P = Q) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S$
13		simprl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to R \in A$
14		simprr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to S \in A$
15	2 3 4	3atnelvolN	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to \neg (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V$
16	6 7 13 14 15	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to \neg (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V$
17	16	adantr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \land P = Q) \to \neg (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V$
18	12 17	eqneltrd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \land P = Q) \to \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V$
19	18	ex	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (P = Q \to \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V)$
20	19	necon2ad	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V \to P \neq Q)$
21	6	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to K \in Lat$
22		eqid	$⊢ {Base}_{K} = {Base}_{K}$
23	22 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
24	23	ad2antrl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to R \in {Base}_{K}$
25	22 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
26	25	adantr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
27	22 1 2	latleeqj2	$⊢ (K \in Lat \land R \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} Q)$
28	21 24 26 27	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} Q)$
29		simpl2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to P \in A$
30	2 3 4	3atnelvolN	$⊢ (K \in HL \land (P \in A \land Q \in A \land S \in A)) \to \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S \in V$
31	6 29 7 14 30	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S \in V$
32		oveq1	$⊢ (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} Q \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S$
33	32	eleq1d	$⊢ (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} Q \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S \in V)$
34	33	notbid	$⊢ (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} Q \to (\neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V \leftrightarrow \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S \in V)$
35	31 34	syl5ibrcom	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} Q \to \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V)$
36	28 35	sylbid	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V)$
37	36	con2d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
38	22 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
39	38	ad2antll	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to S \in {Base}_{K}$
40	22 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}$
41	21 26 24 40	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}$
42	22 1 2	latleeqj2	$⊢ (K \in Lat \land S \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
43	21 39 41 42	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
44	2 3 4	3atnelvolN	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in V$
45	6 29 7 13 44	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in V$
46		eleq1	$⊢ ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in V)$
47	46	notbid	$⊢ ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \to (\neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V \leftrightarrow \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in V)$
48	45 47	syl5ibrcom	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \to \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V)$
49	43 48	sylbid	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \to \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V)$
50	49	con2d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V \to \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
51	20 37 50	3jcad	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)))$
52	1 2 3 4	lvoli2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V$
53	52	3expia	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V)$
54	51 53	impbid	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S \in V \leftrightarrow (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)))$

Metamath Proof Explorer

Theorem islvol2aN

Proof