4at

Description: Four atoms determine a lattice volume uniquely. Three-dimensional analogue of ps-1 and 3at . (Contributed by NM, 11-Jul-2012)

	Ref	Expression
Hypotheses	4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4at.j	$⊢ \underset{˙}{\lor} = join (K)$
	4at.a	$⊢ A = Atoms (K)$
Assertion	4at	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \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)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$

Proof

Step	Hyp	Ref	Expression
1		4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		4at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		4at.a	$⊢ A = Atoms (K)$
4	1 2 3	4atlem12	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \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)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
5		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to K \in HL$
6	5	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to K \in Lat$
7		simp23	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to T \in A$
8		simp31	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to U \in A$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 2 3	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
11	5 7 8 10	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to T \underset{˙}{\lor} U \in {Base}_{K}$
12		simp32	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to V \in A$
13		simp33	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to W \in A$
14	9 2 3	hlatjcl	$⊢ (K \in HL \land V \in A \land W \in A) \to V \underset{˙}{\lor} W \in {Base}_{K}$
15	5 12 13 14	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to V \underset{˙}{\lor} W \in {Base}_{K}$
16	9 2	latjcl	$⊢ (K \in Lat \land T \underset{˙}{\lor} U \in {Base}_{K} \land V \underset{˙}{\lor} W \in {Base}_{K}) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}$
17	6 11 15 16	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}$
18	9 1	latref	$⊢ (K \in Lat \land (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}) \to ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
19	6 17 18	syl2anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
20		breq1	$⊢ (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \leftrightarrow ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
21	19 20	syl5ibrcom	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
22	21	adantr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \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) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
23	4 22	impbid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \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)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$

Metamath Proof Explorer

Theorem 4at

Proof