Metamath Proof Explorer

Theorem cdlemg2idN

Description: Version of cdleme31id with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 21-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemg2id.l ⊢ ≤ ˙ = ≤ K
cdlemg2id.a ⊢ A = Atoms ⁡ K
cdlemg2id.h ⊢ H = LHyp ⁡ K
cdlemg2id.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemg2id.b ⊢ B = Base K
Assertion cdlemg2idN ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → F ⁡ X = X

Proof

Step Hyp Ref Expression
1 cdlemg2id.l ⊢ ≤ ˙ = ≤ K
2 cdlemg2id.a ⊢ A = Atoms ⁡ K
3 cdlemg2id.h ⊢ H = LHyp ⁡ K
4 cdlemg2id.t ⊢ T = LTrn ⁡ K ⁡ W
5 cdlemg2id.b ⊢ B = Base K
6 simp111 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → K ∈ HL
7 simp112 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → W ∈ H
8 simp12 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → P ∈ A ∧ ¬ P ≤ ˙ W
9 simp13 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → Q ∈ A ∧ ¬ Q ≤ ˙ W
10 simp113 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → F ∈ T
11 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → F ⁡ P = Q
12 eqid ⊢ join ⁡ K = join ⁡ K
13 eqid ⊢ meet ⁡ K = meet ⁡ K
14 eqid ⊢ P join ⁡ K Q meet ⁡ K W = P join ⁡ K Q meet ⁡ K W
15 eqid ⊢ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W = t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W
16 eqid ⊢ P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W
17 eqid ⊢ x ∈ B ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ B | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ B | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x = x ∈ B ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ B | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ B | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x
18 5 1 12 13 2 3 4 14 15 16 17 cdlemg2dN ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ F ⁡ P = Q → F = x ∈ B ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ B | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ B | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x
19 6 7 8 9 10 11 18 syl222anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → F = x ∈ B ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ B | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ B | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x
20 19 fveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → F ⁡ X = x ∈ B ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ B | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ B | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x ⁡ X
21 simp2r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → X ∈ B
22 simp3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → P = Q
23 17 cdleme31id ⊢ X ∈ B ∧ P = Q → x ∈ B ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ B | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ B | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x ⁡ X = X
24 21 22 23 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → x ∈ B ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ B | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ B | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x ⁡ X = X
25 20 24 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ⁡ P = Q ∧ X ∈ B ∧ P = Q → F ⁡ X = X