2at0mat0

Description: Special case of 2atmat0 where one atom could be zero. (Contributed by NM, 30-May-2013)

	Ref	Expression
Hypotheses	2atmatz.j	$⊢ \underset{˙}{\lor} = join (K)$
	2atmatz.m	$⊢ \underset{˙}{\land} = meet (K)$
	2atmatz.z	$⊢ \underset{˙}{0} = 0. (K)$
	2atmatz.a	$⊢ A = Atoms (K)$
Assertion	2at0mat0	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		2atmatz.j	$⊢ \underset{˙}{\lor} = join (K)$
2		2atmatz.m	$⊢ \underset{˙}{\land} = meet (K)$
3		2atmatz.z	$⊢ \underset{˙}{0} = 0. (K)$
4		2atmatz.a	$⊢ A = Atoms (K)$
5		simpll	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S \in A) \to (K \in HL \land P \in A \land Q \in A)$
6		simplr1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S \in A) \to R \in A$
7		simpr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S \in A) \to S \in A$
8		simplr3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S \in A) \to P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S$
9		simpl1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to K \in HL$
10		hlol	$⊢ K \in HL \to K \in OL$
11	9 10	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to K \in OL$
12		simpr1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to R \in A$
13		simpr2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to S \in A$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15	14 1 4	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
16	9 12 13 15	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to R \underset{˙}{\lor} S \in {Base}_{K}$
17		simpl3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to Q \in A$
18	14 2 3 4	meetat2	$⊢ (K \in OL \land R \underset{˙}{\lor} S \in {Base}_{K} \land Q \in A) \to ((R \underset{˙}{\lor} S) \underset{˙}{\land} Q \in A \lor (R \underset{˙}{\lor} S) \underset{˙}{\land} Q = \underset{˙}{0})$
19	11 16 17 18	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((R \underset{˙}{\lor} S) \underset{˙}{\land} Q \in A \lor (R \underset{˙}{\lor} S) \underset{˙}{\land} Q = \underset{˙}{0})$
20	19	adantr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P = Q) \to ((R \underset{˙}{\lor} S) \underset{˙}{\land} Q \in A \lor (R \underset{˙}{\lor} S) \underset{˙}{\land} Q = \underset{˙}{0})$
21		oveq1	$⊢ P = Q \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} Q$
22	1 4	hlatjidm	$⊢ (K \in HL \land Q \in A) \to Q \underset{˙}{\lor} Q = Q$
23	9 17 22	syl2anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to Q \underset{˙}{\lor} Q = Q$
24	21 23	sylan9eqr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P = Q) \to P \underset{˙}{\lor} Q = Q$
25	24	oveq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P = Q) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = Q \underset{˙}{\land} (R \underset{˙}{\lor} S)$
26	9	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to K \in Lat$
27	14 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
28	17 27	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to Q \in {Base}_{K}$
29	14 2	latmcom	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \underset{˙}{\lor} S \in {Base}_{K}) \to Q \underset{˙}{\land} (R \underset{˙}{\lor} S) = (R \underset{˙}{\lor} S) \underset{˙}{\land} Q$
30	26 28 16 29	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to Q \underset{˙}{\land} (R \underset{˙}{\lor} S) = (R \underset{˙}{\lor} S) \underset{˙}{\land} Q$
31	30	adantr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P = Q) \to Q \underset{˙}{\land} (R \underset{˙}{\lor} S) = (R \underset{˙}{\lor} S) \underset{˙}{\land} Q$
32	25 31	eqtrd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P = Q) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = (R \underset{˙}{\lor} S) \underset{˙}{\land} Q$
33	32	eleq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P = Q) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\land} Q \in A)$
34	32	eqeq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P = Q) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0} \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\land} Q = \underset{˙}{0})$
35	33 34	orbi12d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P = Q) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0}) \leftrightarrow ((R \underset{˙}{\lor} S) \underset{˙}{\land} Q \in A \lor (R \underset{˙}{\lor} S) \underset{˙}{\land} Q = \underset{˙}{0}))$
36	20 35	mpbird	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P = Q) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$
37	14 1 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
38	37	adantr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
39	14 2 3 4	meetat2	$⊢ (K \in OL \land P \underset{˙}{\lor} Q \in {Base}_{K} \land S \in A) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} S \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} S = \underset{˙}{0})$
40	11 38 13 39	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} S \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} S = \underset{˙}{0})$
41	40	adantr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land R = S) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} S \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} S = \underset{˙}{0})$
42		oveq1	$⊢ R = S \to R \underset{˙}{\lor} S = S \underset{˙}{\lor} S$
43	1 4	hlatjidm	$⊢ (K \in HL \land S \in A) \to S \underset{˙}{\lor} S = S$
44	9 13 43	syl2anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to S \underset{˙}{\lor} S = S$
45	42 44	sylan9eqr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land R = S) \to R \underset{˙}{\lor} S = S$
46	45	oveq2d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land R = S) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} S$
47	46	eleq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land R = S) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\land} S \in A)$
48	46	eqeq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land R = S) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0} \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\land} S = \underset{˙}{0})$
49	47 48	orbi12d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land R = S) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0}) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\land} S \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} S = \underset{˙}{0}))$
50	41 49	mpbird	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land R = S) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$
51	50	adantlr	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P \neq Q) \land R = S) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$
52		df-ne	$⊢ (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0} \leftrightarrow \neg (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0}$
53		simpll1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to K \in HL$
54		simpll2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to P \in A$
55		simpll3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to Q \in A$
56		simpr1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to P \neq Q$
57		eqid	$⊢ LLines (K) = LLines (K)$
58	1 4 57	llni2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to P \underset{˙}{\lor} Q \in LLines (K)$
59	53 54 55 56 58	syl31anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to P \underset{˙}{\lor} Q \in LLines (K)$
60		simplr1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to R \in A$
61		simplr2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to S \in A$
62		simpr2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to R \neq S$
63	1 4 57	llni2	$⊢ ((K \in HL \land R \in A \land S \in A) \land R \neq S) \to R \underset{˙}{\lor} S \in LLines (K)$
64	53 60 61 62 63	syl31anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to R \underset{˙}{\lor} S \in LLines (K)$
65		simplr3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S$
66		simpr3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0}$
67	2 3 4 57	2llnmat	$⊢ ((K \in HL \land P \underset{˙}{\lor} Q \in LLines (K) \land R \underset{˙}{\lor} S \in LLines (K)) \land (P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A$
68	53 59 64 65 66 67	syl32anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land (P \neq Q \land R \neq S \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0})) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A$
69	68	3exp2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to (P \neq Q \to (R \neq S \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0} \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A)))$
70	69	imp31	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P \neq Q) \land R \neq S) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \neq \underset{˙}{0} \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A)$
71	52 70	biimtrrid	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P \neq Q) \land R \neq S) \to (\neg (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0} \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A)$
72	71	orrd	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P \neq Q) \land R \neq S) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0} \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A)$
73	72	orcomd	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P \neq Q) \land R \neq S) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$
74	51 73	pm2.61dane	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land P \neq Q) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$
75	36 74	pm2.61dane	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$
76	5 6 7 8 75	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S \in A) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$
77		simpl1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to K \in HL$
78	77 10	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to K \in OL$
79	37	adantr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
80		simpr1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to R \in A$
81	14 2 3 4	meetat2	$⊢ (K \in OL \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in A) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} R \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} R = \underset{˙}{0})$
82	78 79 80 81	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} R \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} R = \underset{˙}{0})$
83	82	adantr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S = \underset{˙}{0}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} R \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} R = \underset{˙}{0})$
84		oveq2	$⊢ S = \underset{˙}{0} \to R \underset{˙}{\lor} S = R \underset{˙}{\lor} \underset{˙}{0}$
85	14 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
86	80 85	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to R \in {Base}_{K}$
87	14 1 3	olj01	$⊢ (K \in OL \land R \in {Base}_{K}) \to R \underset{˙}{\lor} \underset{˙}{0} = R$
88	78 86 87	syl2anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to R \underset{˙}{\lor} \underset{˙}{0} = R$
89	84 88	sylan9eqr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S = \underset{˙}{0}) \to R \underset{˙}{\lor} S = R$
90	89	oveq2d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S = \underset{˙}{0}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} R$
91	90	eleq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S = \underset{˙}{0}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\land} R \in A)$
92	90	eqeq1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S = \underset{˙}{0}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0} \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\land} R = \underset{˙}{0})$
93	91 92	orbi12d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S = \underset{˙}{0}) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0}) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\land} R \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} R = \underset{˙}{0}))$
94	83 93	mpbird	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \land S = \underset{˙}{0}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$
95		simpr2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to (S \in A \lor S = \underset{˙}{0})$
96	76 94 95	mpjaodan	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$

Metamath Proof Explorer

Theorem 2at0mat0

Proof