islpln2a

Description: The predicate "is a lattice plane" for join of atoms. (Contributed by NM, 16-Jul-2012)

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

Proof

Step	Hyp	Ref	Expression
1		islpln2a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		islpln2a.j	$⊢ \underset{˙}{\lor} = join (K)$
3		islpln2a.a	$⊢ A = Atoms (K)$
4		islpln2a.p	$⊢ P = LPlanes (K)$
5		oveq1	$⊢ Q = R \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} R$
6	2 3	hlatjidm	$⊢ (K \in HL \land R \in A) \to R \underset{˙}{\lor} R = R$
7	6	3ad2antr2	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to R \underset{˙}{\lor} R = R$
8	5 7	sylan9eqr	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A)) \land Q = R) \to Q \underset{˙}{\lor} R = R$
9	8	oveq1d	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A)) \land Q = R) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = R \underset{˙}{\lor} S$
10		simpll	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A)) \land Q = R) \to K \in HL$
11		simplr2	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A)) \land Q = R) \to R \in A$
12		simplr3	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A)) \land Q = R) \to S \in A$
13	2 3 4	2atnelpln	$⊢ (K \in HL \land R \in A \land S \in A) \to \neg R \underset{˙}{\lor} S \in P$
14	10 11 12 13	syl3anc	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A)) \land Q = R) \to \neg R \underset{˙}{\lor} S \in P$
15	9 14	eqneltrd	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A)) \land Q = R) \to \neg (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P$
16	15	ex	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to (Q = R \to \neg (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P)$
17	16	necon2ad	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P \to Q \neq R)$
18		hllat	$⊢ K \in HL \to K \in Lat$
19	18	adantr	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to K \in Lat$
20		simpr3	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to S \in A$
21		eqid	$⊢ {Base}_{K} = {Base}_{K}$
22	21 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
23	20 22	syl	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to S \in {Base}_{K}$
24	21 2 3	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
25	24	3adant3r3	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
26	21 1 2	latleeqj2	$⊢ (K \in Lat \land S \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K}) \to (S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = Q \underset{˙}{\lor} R)$
27	19 23 25 26	syl3anc	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to (S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = Q \underset{˙}{\lor} R)$
28	2 3 4	2atnelpln	$⊢ (K \in HL \land Q \in A \land R \in A) \to \neg Q \underset{˙}{\lor} R \in P$
29	28	3adant3r3	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to \neg Q \underset{˙}{\lor} R \in P$
30		eleq1	$⊢ (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = Q \underset{˙}{\lor} R \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P \leftrightarrow Q \underset{˙}{\lor} R \in P)$
31	30	notbid	$⊢ (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = Q \underset{˙}{\lor} R \to (\neg (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P \leftrightarrow \neg Q \underset{˙}{\lor} R \in P)$
32	29 31	syl5ibrcom	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = Q \underset{˙}{\lor} R \to \neg (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P)$
33	27 32	sylbid	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to (S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to \neg (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P)$
34	33	con2d	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P \to \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
35	17 34	jcad	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P \to (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
36	1 2 3 4	lplni2	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P$
37	36	3expia	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to ((Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P)$
38	35 37	impbid	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P \leftrightarrow (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$

Metamath Proof Explorer

Theorem islpln2a

Proof