4atexlemswapqr

Description: Lemma for 4atexlem7 . Swap Q and R , so that theorems involving C can be reused for D . Note that U must be expanded because it involves Q . (Contributed by NM, 25-Nov-2012)

	Ref	Expression
Hypotheses	4thatlem.ph	$⊢ φ \leftrightarrow (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (T \in A \land U \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
	4thatlemslps.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4thatlemslps.j	$⊢ \underset{˙}{\lor} = join (K)$
	4thatlemslps.a	$⊢ A = Atoms (K)$
	4thatlemsw.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	4atexlemswapqr	$⊢ φ \to (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (S \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} Q) \land (T \in A \land ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq R \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} R)))$

Proof

Step	Hyp	Ref	Expression
1		4thatlem.ph	$⊢ φ \leftrightarrow (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (T \in A \land U \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
2		4thatlemslps.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		4thatlemslps.j	$⊢ \underset{˙}{\lor} = join (K)$
4		4thatlemslps.a	$⊢ A = Atoms (K)$
5		4thatlemsw.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
6		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (T \in A \land U \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (K \in HL \land W \in H)$
7	1 6	sylbi	$⊢ φ \to (K \in HL \land W \in H)$
8	1	4atexlempw	$⊢ φ \to (P \in A \land \neg P \underset{˙}{\leq} W)$
9		simp22	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (T \in A \land U \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
10		3simpa	$⊢ (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
11	9 10	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (T \in A \land U \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
12	1 11	sylbi	$⊢ φ \to (R \in A \land \neg R \underset{˙}{\leq} W)$
13	7 8 12	3jca	$⊢ φ \to ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W))$
14	1	4atexlems	$⊢ φ \to S \in A$
15	1	4atexlemq	$⊢ φ \to Q \in A$
16		simp13r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (T \in A \land U \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg Q \underset{˙}{\leq} W$
17	1 16	sylbi	$⊢ φ \to \neg Q \underset{˙}{\leq} W$
18	1	4atexlemkc	$⊢ φ \to K \in CvLat$
19	1	4atexlemp	$⊢ φ \to P \in A$
20	12	simpld	$⊢ φ \to R \in A$
21	1	4atexlempnq	$⊢ φ \to P \neq Q$
22		simp223	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (T \in A \land U \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
23	1 22	sylbi	$⊢ φ \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
24	4 3	cvlsupr7	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} Q = R \underset{˙}{\lor} Q$
25	18 19 15 20 21 23 24	syl132anc	$⊢ φ \to P \underset{˙}{\lor} Q = R \underset{˙}{\lor} Q$
26	15 17 25	3jca	$⊢ φ \to (Q \in A \land \neg Q \underset{˙}{\leq} W \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} Q)$
27	1	4atexlemt	$⊢ φ \to T \in A$
28	4 3	cvlsupr8	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R$
29	18 19 15 20 21 23 28	syl132anc	$⊢ φ \to P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R$
30	29	oveq1d	$⊢ φ \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
31	5 30	syl5eq	$⊢ φ \to U = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
32	31	oveq1d	$⊢ φ \to U \underset{˙}{\lor} T = ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\lor} T$
33	1	4atexlemutvt	$⊢ φ \to U \underset{˙}{\lor} T = V \underset{˙}{\lor} T$
34	32 33	eqtr3d	$⊢ φ \to ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\lor} T = V \underset{˙}{\lor} T$
35	27 34	jca	$⊢ φ \to (T \in A \land ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\lor} T = V \underset{˙}{\lor} T)$
36	14 26 35	3jca	$⊢ φ \to (S \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} Q) \land (T \in A \land ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\lor} T = V \underset{˙}{\lor} T))$
37	4 3	cvlsupr5	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to R \neq P$
38	37	necomd	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \neq R$
39	18 19 15 20 21 23 38	syl132anc	$⊢ φ \to P \neq R$
40	1	4atexlemnslpq	$⊢ φ \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
41	29	eqcomd	$⊢ φ \to P \underset{˙}{\lor} R = P \underset{˙}{\lor} Q$
42	41	breq2d	$⊢ φ \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} R) \leftrightarrow S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
43	40 42	mtbird	$⊢ φ \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
44	39 43	jca	$⊢ φ \to (P \neq R \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
45	13 36 44	3jca	$⊢ φ \to (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (S \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W \land P \underset{˙}{\lor} Q = R \underset{˙}{\lor} Q) \land (T \in A \land ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq R \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} R)))$

Metamath Proof Explorer

Theorem 4atexlemswapqr

Proof