This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemn

Description: Lemma N of Crawley p. 121 line 27. (Contributed by NM, 27-Feb-2014)

Ref Expression
Hypotheses cdlemn11.b ⊢ B = Base K
cdlemn11.l ⊢ ≤ ˙ = ≤ K
cdlemn11.j ⊢ ∨ ˙ = join ⁡ K
cdlemn11.a ⊢ A = Atoms ⁡ K
cdlemn11.h ⊢ H = LHyp ⁡ K
cdlemn11.i ⊢ I = DIsoB ⁡ K ⁡ W
cdlemn11.J ⊢ J = DIsoC ⁡ K ⁡ W
cdlemn11.u ⊢ U = DVecH ⁡ K ⁡ W
cdlemn11.s ⊢ ⊕ ˙ = LSSum ⁡ U
Assertion cdlemn ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W ∧ X ∈ B ∧ X ≤ ˙ W → R ≤ ˙ Q ∨ ˙ X ↔ J ⁡ R ⊆ J ⁡ Q ⊕ ˙ I ⁡ X

Proof

Step Hyp Ref Expression
1 cdlemn11.b ⊢ B = Base K
2 cdlemn11.l ⊢ ≤ ˙ = ≤ K
3 cdlemn11.j ⊢ ∨ ˙ = join ⁡ K
4 cdlemn11.a ⊢ A = Atoms ⁡ K
5 cdlemn11.h ⊢ H = LHyp ⁡ K
6 cdlemn11.i ⊢ I = DIsoB ⁡ K ⁡ W
7 cdlemn11.J ⊢ J = DIsoC ⁡ K ⁡ W
8 cdlemn11.u ⊢ U = DVecH ⁡ K ⁡ W
9 cdlemn11.s ⊢ ⊕ ˙ = LSSum ⁡ U
10 1 2 3 4 5 8 9 6 7 cdlemn5 ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W ∧ X ∈ B ∧ X ≤ ˙ W ∧ R ≤ ˙ Q ∨ ˙ X → J ⁡ R ⊆ J ⁡ Q ⊕ ˙ I ⁡ X
11 10 3expia ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W ∧ X ∈ B ∧ X ≤ ˙ W → R ≤ ˙ Q ∨ ˙ X → J ⁡ R ⊆ J ⁡ Q ⊕ ˙ I ⁡ X
12 1 2 3 4 5 6 7 8 9 cdlemn11 ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W ∧ X ∈ B ∧ X ≤ ˙ W ∧ J ⁡ R ⊆ J ⁡ Q ⊕ ˙ I ⁡ X → R ≤ ˙ Q ∨ ˙ X
13 12 3expia ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W ∧ X ∈ B ∧ X ≤ ˙ W → J ⁡ R ⊆ J ⁡ Q ⊕ ˙ I ⁡ X → R ≤ ˙ Q ∨ ˙ X
14 11 13 impbid ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W ∧ X ∈ B ∧ X ≤ ˙ W → R ≤ ˙ Q ∨ ˙ X ↔ J ⁡ R ⊆ J ⁡ Q ⊕ ˙ I ⁡ X