atcvrj0

Description: Two atoms covering the zero subspace are equal. ( atcv1 analog.) (Contributed by NM, 29-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		atcvrj0.b	$⊢ B = {Base}_{K}$
2		atcvrj0.j	$⊢ \underset{˙}{\lor} = join (K)$
3		atcvrj0.z	$⊢ \underset{˙}{0} = 0. (K)$
4		atcvrj0.c	$⊢ C = ⋖_{K}$
5		atcvrj0.a	$⊢ A = Atoms (K)$
6		breq1	$⊢ X = \underset{˙}{0} \to (X C (P \underset{˙}{\lor} Q) \leftrightarrow \underset{˙}{0} C (P \underset{˙}{\lor} Q))$
7	6	biimpd	$⊢ X = \underset{˙}{0} \to (X C (P \underset{˙}{\lor} Q) \to \underset{˙}{0} C (P \underset{˙}{\lor} Q))$
8	7	adantl	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land X = \underset{˙}{0}) \to (X C (P \underset{˙}{\lor} Q) \to \underset{˙}{0} C (P \underset{˙}{\lor} Q))$
9	2 3 4 5	atcvr0eq	$⊢ (K \in HL \land P \in A \land Q \in A) \to (\underset{˙}{0} C (P \underset{˙}{\lor} Q) \leftrightarrow P = Q)$
10	9	3adant3r1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (\underset{˙}{0} C (P \underset{˙}{\lor} Q) \leftrightarrow P = Q)$
11	10	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land X = \underset{˙}{0}) \to (\underset{˙}{0} C (P \underset{˙}{\lor} Q) \leftrightarrow P = Q)$
12	8 11	sylibd	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land X = \underset{˙}{0}) \to (X C (P \underset{˙}{\lor} Q) \to P = Q)$
13	12	ex	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X = \underset{˙}{0} \to (X C (P \underset{˙}{\lor} Q) \to P = Q))$
14	13	com23	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X C (P \underset{˙}{\lor} Q) \to (X = \underset{˙}{0} \to P = Q))$
15	14	3impia	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land X C (P \underset{˙}{\lor} Q)) \to (X = \underset{˙}{0} \to P = Q)$
16		oveq1	$⊢ P = Q \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} Q$
17	16	breq2d	$⊢ P = Q \to (X C (P \underset{˙}{\lor} Q) \leftrightarrow X C (Q \underset{˙}{\lor} Q))$
18	17	biimpac	$⊢ (X C (P \underset{˙}{\lor} Q) \land P = Q) \to X C (Q \underset{˙}{\lor} Q)$
19		simpr3	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to Q \in A$
20	2 5	hlatjidm	$⊢ (K \in HL \land Q \in A) \to Q \underset{˙}{\lor} Q = Q$
21	19 20	syldan	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to Q \underset{˙}{\lor} Q = Q$
22	21	breq2d	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X C (Q \underset{˙}{\lor} Q) \leftrightarrow X C Q)$
23		hlatl	$⊢ K \in HL \to K \in AtLat$
24	23	adantr	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in AtLat$
25		simpr1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to X \in B$
26		eqid	$⊢ \leq_{K} = \leq_{K}$
27	1 26 3 4 5	atcvreq0	$⊢ (K \in AtLat \land X \in B \land Q \in A) \to (X C Q \leftrightarrow X = \underset{˙}{0})$
28	24 25 19 27	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X C Q \leftrightarrow X = \underset{˙}{0})$
29	28	biimpd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X C Q \to X = \underset{˙}{0})$
30	22 29	sylbid	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X C (Q \underset{˙}{\lor} Q) \to X = \underset{˙}{0})$
31	18 30	syl5	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((X C (P \underset{˙}{\lor} Q) \land P = Q) \to X = \underset{˙}{0})$
32	31	expd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X C (P \underset{˙}{\lor} Q) \to (P = Q \to X = \underset{˙}{0}))$
33	32	3impia	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land X C (P \underset{˙}{\lor} Q)) \to (P = Q \to X = \underset{˙}{0})$
34	15 33	impbid	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land X C (P \underset{˙}{\lor} Q)) \to (X = \underset{˙}{0} \leftrightarrow P = Q)$

Metamath Proof Explorer

Theorem atcvrj0

Proof