4atlem12a

Description: Lemma for 4at . Substitute T for P . (Contributed by NM, 9-Jul-2012)

	Ref	Expression
Hypotheses	4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4at.j	$⊢ \underset{˙}{\lor} = join (K)$
	4at.a	$⊢ A = Atoms (K)$
Assertion	4atlem12a	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \leftrightarrow (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) = (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		simp11	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to K \in HL$
5		simp12	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to P \in A$
6		simp13	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to T \in A$
7	4	hllatd	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to K \in Lat$
8		simp21	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to U \in A$
9		simp22	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to V \in A$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 2 3	hlatjcl	$⊢ (K \in HL \land U \in A \land V \in A) \to U \underset{˙}{\lor} V \in {Base}_{K}$
12	4 8 9 11	syl3anc	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to U \underset{˙}{\lor} V \in {Base}_{K}$
13		simp23	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to W \in A$
14	10 3	atbase	$⊢ W \in A \to W \in {Base}_{K}$
15	13 14	syl	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to W \in {Base}_{K}$
16	10 2	latjcl	$⊢ (K \in Lat \land U \underset{˙}{\lor} V \in {Base}_{K} \land W \in {Base}_{K}) \to (U \underset{˙}{\lor} V) \underset{˙}{\lor} W \in {Base}_{K}$
17	7 12 15 16	syl3anc	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (U \underset{˙}{\lor} V) \underset{˙}{\lor} W \in {Base}_{K}$
18		simp3	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
19	10 1 2 3	hlexchb2	$⊢ (K \in HL \land (P \in A \land T \in A \land (U \underset{˙}{\lor} V) \underset{˙}{\lor} W \in {Base}_{K}) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (P \underset{˙}{\leq} (T \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \leftrightarrow P \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) = T \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W))$
20	4 5 6 17 18 19	syl131anc	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (P \underset{˙}{\leq} (T \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \leftrightarrow P \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) = T \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W))$
21	1 2 3	4atlem4a	$⊢ ((K \in HL \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)$
22	4 6 8 9 13 21	syl32anc	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) = T \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
23	22	breq2d	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \leftrightarrow P \underset{˙}{\leq} (T \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)))$
24	1 2 3	4atlem4a	$⊢ ((K \in HL \land P \in A \land U \in A) \land (V \in A \land W \in A)) \to (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) = P \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
25	4 5 8 9 13 24	syl32anc	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) = P \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
26	25 22	eqeq12d	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to ((P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \leftrightarrow P \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) = T \underset{˙}{\lor} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W))$
27	20 23 26	3bitr4d	$⊢ ((K \in HL \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \leftrightarrow (P \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$

Metamath Proof Explorer

Theorem 4atlem12a

Proof