atcvr0eq

Description: The covers relation is not transitive. ( atcv0eq analog.) (Contributed by NM, 29-Nov-2011)

	Ref	Expression
Hypotheses	atcvr0eq.j	$⊢ \underset{˙}{\lor} = join (K)$
	atcvr0eq.z	$⊢ \underset{˙}{0} = 0. (K)$
	atcvr0eq.c	$⊢ C = ⋖_{K}$
	atcvr0eq.a	$⊢ A = Atoms (K)$
Assertion	atcvr0eq	$⊢ (K \in HL \land P \in A \land Q \in A) \to (\underset{˙}{0} C (P \underset{˙}{\lor} Q) \leftrightarrow P = Q)$

Proof

Step	Hyp	Ref	Expression
1		atcvr0eq.j	$⊢ \underset{˙}{\lor} = join (K)$
2		atcvr0eq.z	$⊢ \underset{˙}{0} = 0. (K)$
3		atcvr0eq.c	$⊢ C = ⋖_{K}$
4		atcvr0eq.a	$⊢ A = Atoms (K)$
5	1 3 4	atcvr1	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P C (P \underset{˙}{\lor} Q))$
6	2 3 4	atcvr0	$⊢ (K \in HL \land P \in A) \to \underset{˙}{0} C P$
7	6	3adant3	$⊢ (K \in HL \land P \in A \land Q \in A) \to \underset{˙}{0} C P$
8	7	biantrurd	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P C (P \underset{˙}{\lor} Q) \leftrightarrow (\underset{˙}{0} C P \land P C (P \underset{˙}{\lor} Q)))$
9	5 8	bitrd	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow (\underset{˙}{0} C P \land P C (P \underset{˙}{\lor} Q)))$
10		simp1	$⊢ (K \in HL \land P \in A \land Q \in A) \to K \in HL$
11		hlop	$⊢ K \in HL \to K \in OP$
12	11	3ad2ant1	$⊢ (K \in HL \land P \in A \land Q \in A) \to K \in OP$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 2	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in {Base}_{K}$
15	12 14	syl	$⊢ (K \in HL \land P \in A \land Q \in A) \to \underset{˙}{0} \in {Base}_{K}$
16	13 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
17	16	3ad2ant2	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \in {Base}_{K}$
18	13 1 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
19	13 3	cvrntr	$⊢ (K \in HL \land (\underset{˙}{0} \in {Base}_{K} \land P \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((\underset{˙}{0} C P \land P C (P \underset{˙}{\lor} Q)) \to \neg \underset{˙}{0} C (P \underset{˙}{\lor} Q))$
20	10 15 17 18 19	syl13anc	$⊢ (K \in HL \land P \in A \land Q \in A) \to ((\underset{˙}{0} C P \land P C (P \underset{˙}{\lor} Q)) \to \neg \underset{˙}{0} C (P \underset{˙}{\lor} Q))$
21	9 20	sylbid	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \neq Q \to \neg \underset{˙}{0} C (P \underset{˙}{\lor} Q))$
22	21	necon4ad	$⊢ (K \in HL \land P \in A \land Q \in A) \to (\underset{˙}{0} C (P \underset{˙}{\lor} Q) \to P = Q)$
23	1 4	hlatjidm	$⊢ (K \in HL \land P \in A) \to P \underset{˙}{\lor} P = P$
24	23	3adant3	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} P = P$
25	7 24	breqtrrd	$⊢ (K \in HL \land P \in A \land Q \in A) \to \underset{˙}{0} C (P \underset{˙}{\lor} P)$
26		oveq2	$⊢ P = Q \to P \underset{˙}{\lor} P = P \underset{˙}{\lor} Q$
27	26	breq2d	$⊢ P = Q \to (\underset{˙}{0} C (P \underset{˙}{\lor} P) \leftrightarrow \underset{˙}{0} C (P \underset{˙}{\lor} Q))$
28	25 27	syl5ibcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P = Q \to \underset{˙}{0} C (P \underset{˙}{\lor} Q))$
29	22 28	impbid	$⊢ (K \in HL \land P \in A \land Q \in A) \to (\underset{˙}{0} C (P \underset{˙}{\lor} Q) \leftrightarrow P = Q)$

Metamath Proof Explorer

Theorem atcvr0eq

Proof