4at2

Description: Four atoms determine a lattice volume uniquely. (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	4at2	$⊢ (((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	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))$
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		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
9	8	3ad2ant1	$⊢ ((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 \in {Base}_{K}$
10		simp21	$⊢ ((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 R \in A$
11	7 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
12	10 11	syl	$⊢ ((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 R \in {Base}_{K}$
13		simp22	$⊢ ((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 S \in A$
14	7 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
15	13 14	syl	$⊢ ((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 S \in {Base}_{K}$
16	7 2	latjass	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in {Base}_{K} \land S \in {Base}_{K})) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
17	6 9 12 15 16	syl13anc	$⊢ ((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 = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
18		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$
19		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$
20	7 2 3	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
21	5 18 19 20	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}$
22		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$
23	7 3	atbase	$⊢ V \in A \to V \in {Base}_{K}$
24	22 23	syl	$⊢ ((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 {Base}_{K}$
25		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$
26	7 3	atbase	$⊢ W \in A \to W \in {Base}_{K}$
27	25 26	syl	$⊢ ((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 {Base}_{K}$
28	7 2	latjass	$⊢ (K \in Lat \land (T \underset{˙}{\lor} U \in {Base}_{K} \land V \in {Base}_{K} \land W \in {Base}_{K})) \to ((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \underset{˙}{\lor} W = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
29	6 21 24 27 28	syl13anc	$⊢ ((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 = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
30	17 29	breq12d	$⊢ ((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) \underset{˙}{\leq} (((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \underset{˙}{\lor} W) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
31	30	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) \underset{˙}{\leq} (((T \underset{˙}{\lor} U) \underset{˙}{\lor} V) \underset{˙}{\lor} W) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
32	17 29	eqeq12d	$⊢ ((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 \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
33	32	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 \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
34	4 31 33	3bitr4d	$⊢ (((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 4at2

Proof