Metamath Proof Explorer

Theorem cvlsupr8

Description: Consequence of superposition condition ( P .\/ R ) = ( Q .\/ R ) . (Contributed by NM, 24-Nov-2012)

Ref Expression
Hypotheses cvlsupr5.a ⊢ A = Atoms ⁡ K
cvlsupr5.j ⊢ ∨ ˙ = join ⁡ K
Assertion cvlsupr8 ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ P ∨ ˙ R = Q ∨ ˙ R → P ∨ ˙ Q = P ∨ ˙ R

Proof

Step Hyp Ref Expression
1 cvlsupr5.a ⊢ A = Atoms ⁡ K
2 cvlsupr5.j ⊢ ∨ ˙ = join ⁡ K
3 cvllat ⊢ K ∈ CvLat → K ∈ Lat
4 3 3ad2ant1 ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ P ∨ ˙ R = Q ∨ ˙ R → K ∈ Lat
5 simp22 ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ P ∨ ˙ R = Q ∨ ˙ R → Q ∈ A
6 eqid ⊢ Base K = Base K
7 6 1 atbase ⊢ Q ∈ A → Q ∈ Base K
8 5 7 syl ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ P ∨ ˙ R = Q ∨ ˙ R → Q ∈ Base K
9 simp23 ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ P ∨ ˙ R = Q ∨ ˙ R → R ∈ A
10 6 1 atbase ⊢ R ∈ A → R ∈ Base K
11 9 10 syl ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ P ∨ ˙ R = Q ∨ ˙ R → R ∈ Base K
12 6 2 latjcom ⊢ K ∈ Lat ∧ Q ∈ Base K ∧ R ∈ Base K → Q ∨ ˙ R = R ∨ ˙ Q
13 4 8 11 12 syl3anc ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ P ∨ ˙ R = Q ∨ ˙ R → Q ∨ ˙ R = R ∨ ˙ Q
14 simp3r ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ P ∨ ˙ R = Q ∨ ˙ R → P ∨ ˙ R = Q ∨ ˙ R
15 1 2 cvlsupr7 ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ P ∨ ˙ R = Q ∨ ˙ R → P ∨ ˙ Q = R ∨ ˙ Q
16 13 14 15 3eqtr4rd ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ P ∨ ˙ R = Q ∨ ˙ R → P ∨ ˙ Q = P ∨ ˙ R