Metamath Proof Explorer

Theorem cdlemg8

Description: TODO: FIX COMMENT. (Contributed by NM, 29-Apr-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 cdlemg8 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q → P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W = Q ∨ ˙ F ⁡ G ⁡ Q ∧ ˙ W

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 simpl1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P = P → K ∈ HL ∧ W ∈ H
8 simpl21 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P = P → P ∈ A ∧ ¬ P ≤ ˙ W
9 simpl22 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P = P → Q ∈ A ∧ ¬ Q ≤ ˙ W
10 simpl23 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P = P → F ∈ T
11 simpl3l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P = P → G ∈ T
12 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P = P → F ⁡ G ⁡ P = P
13 1 2 3 4 5 6 cdlemg8a ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P = P → P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W = Q ∨ ˙ F ⁡ G ⁡ Q ∧ ˙ W
14 7 8 9 10 11 12 13 syl123anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P = P → P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W = Q ∨ ˙ F ⁡ G ⁡ Q ∧ ˙ W
15 simpl1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → K ∈ HL ∧ W ∈ H
16 simpl2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T
17 simpl3l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → G ∈ T
18 simpl3r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q
19 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → F ⁡ G ⁡ P ≠ P
20 1 2 3 4 5 6 cdlemg8d ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W = Q ∨ ˙ F ⁡ G ⁡ Q ∧ ˙ W
21 15 16 17 18 19 20 syl113anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W = Q ∨ ˙ F ⁡ G ⁡ Q ∧ ˙ W
22 14 21 pm2.61dane ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q → P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W = Q ∨ ˙ F ⁡ G ⁡ Q ∧ ˙ W