cdlemg12c

Description: The triples <. P , ( FP ) , ( F( GP ) ) >. and <. Q , ( FQ ) , ( F( GQ ) ) >. are axially perspective by dalaw . TODO: FIX COMMENT. (Contributed by NM, 5-May-2013)

	Ref	Expression
Hypotheses	cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg12.a	$⊢ A = Atoms (K)$
	cdlemg12.h	$⊢ H = LHyp (K)$
	cdlemg12.t	$⊢ T = LTrn (K) (W)$
	cdlemg12b.r	$⊢ R = trL (K) (W)$
Assertion	cdlemg12c	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} G (Q))) \underset{˙}{\leq} (((G (P) \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (G (Q) \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\lor} ((F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q)))$

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg12.a	$⊢ A = Atoms (K)$
5		cdlemg12.h	$⊢ H = LHyp (K)$
6		cdlemg12.t	$⊢ T = LTrn (K) (W)$
7		cdlemg12b.r	$⊢ R = trL (K) (W)$
8	1 2 3 4 5 6 7	cdlemg12b	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (G (P) \underset{˙}{\lor} G (Q))) \underset{˙}{\leq} (F (G (P)) \underset{˙}{\lor} F (G (Q)))$
9		simp1l	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
10		simp21l	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
11		simp1	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (K \in HL \land W \in H)$
12		simp31	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to G \in T$
13	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in A) \to G (P) \in A$
14	11 12 10 13	syl3anc	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to G (P) \in A$
15		simp23	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in T$
16	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land G (P) \in A) \to F (G (P)) \in A$
17	11 15 14 16	syl3anc	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F (G (P)) \in A$
18		simp22l	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
19	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land Q \in A) \to G (Q) \in A$
20	11 12 18 19	syl3anc	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to G (Q) \in A$
21	1 4 5 6	ltrncoat	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land Q \in A) \to F (G (Q)) \in A$
22	11 15 12 18 21	syl121anc	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F (G (Q)) \in A$
23	1 2 3 4	dalaw	$⊢ (K \in HL \land (P \in A \land G (P) \in A \land F (G (P)) \in A) \land (Q \in A \land G (Q) \in A \land F (G (Q)) \in A)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\land} (G (P) \underset{˙}{\lor} G (Q))) \underset{˙}{\leq} (F (G (P)) \underset{˙}{\lor} F (G (Q))) \to ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} G (Q))) \underset{˙}{\leq} (((G (P) \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (G (Q) \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\lor} ((F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q))))$
24	9 10 14 17 18 20 22 23	syl133anc	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\land} (G (P) \underset{˙}{\lor} G (Q))) \underset{˙}{\leq} (F (G (P)) \underset{˙}{\lor} F (G (Q))) \to ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} G (Q))) \underset{˙}{\leq} (((G (P) \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (G (Q) \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\lor} ((F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q))))$
25	8 24	mpd	$⊢ ((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 F \in T) \land (G \in T \land P \neq Q \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} G (Q))) \underset{˙}{\leq} (((G (P) \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} (G (Q) \underset{˙}{\lor} F (G (Q)))) \underset{˙}{\lor} ((F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q)))$

Metamath Proof Explorer

Theorem cdlemg12c

Proof