Metamath Proof Explorer

Theorem cdlemg9b

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

Ref Expression
Hypotheses cdlemg8.l ⊢ ≤ ˙ = ≤ K
cdlemg8.j ⊢ ∨ ˙ = join ⁡ K
cdlemg8.m ⊢ ∧ ˙ = meet ⁡ K
cdlemg8.a ⊢ A = Atoms ⁡ K
cdlemg8.h ⊢ H = LHyp ⁡ K
cdlemg8.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion cdlemg9b ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → P ∨ ˙ Q ∧ ˙ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≤ ˙ G ⁡ P ∨ ˙ G ⁡ Q

Proof

Step Hyp Ref Expression
1 cdlemg8.l ⊢ ≤ ˙ = ≤ K
2 cdlemg8.j ⊢ ∨ ˙ = join ⁡ K
3 cdlemg8.m ⊢ ∧ ˙ = meet ⁡ K
4 cdlemg8.a ⊢ A = Atoms ⁡ K
5 cdlemg8.h ⊢ H = LHyp ⁡ K
6 cdlemg8.t ⊢ T = LTrn ⁡ K ⁡ W
7 eqid ⊢ P ∨ ˙ Q ∧ ˙ W = P ∨ ˙ Q ∧ ˙ W
8 1 2 3 4 5 6 7 cdlemg9a ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → P ∨ ˙ P ∨ ˙ Q ∧ ˙ W ∧ ˙ F ⁡ G ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W ≤ ˙ G ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
9 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → K ∈ HL
10 simp1r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → W ∈ H
11 simp21 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → P ∈ A ∧ ¬ P ≤ ˙ W
12 simp22l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → Q ∈ A
13 1 2 3 4 5 7 cdlemg3a ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ Q = P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
14 9 10 11 12 13 syl211anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → P ∨ ˙ Q = P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
15 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → K ∈ HL ∧ W ∈ H
16 simp22 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → Q ∈ A ∧ ¬ Q ≤ ˙ W
17 simp23 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → F ∈ T
18 simp31 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → G ∈ T
19 5 6 1 2 4 3 7 cdlemg2l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T → F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = F ⁡ G ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
20 15 11 16 17 18 19 syl122anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = F ⁡ G ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
21 14 20 oveq12d ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → P ∨ ˙ Q ∧ ˙ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ P ∨ ˙ Q ∧ ˙ W ∧ ˙ F ⁡ G ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
22 5 6 1 2 4 3 7 cdlemg2k ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T → G ⁡ P ∨ ˙ G ⁡ Q = G ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
23 15 11 16 18 22 syl121anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → G ⁡ P ∨ ˙ G ⁡ Q = G ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
24 8 21 23 3brtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ P ≠ Q ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≠ P ∨ ˙ Q → P ∨ ˙ Q ∧ ˙ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q ≤ ˙ G ⁡ P ∨ ˙ G ⁡ Q