Metamath Proof Explorer

Theorem 4atlem10a

Description: Lemma for 4at . Substitute V for R . (Contributed by NM, 9-Jul-2012)

Ref Expression
Hypotheses 4at.l ⊢≤˙=≤K
4at.j ⊢∨˙=join⁡K
4at.a ⊢A=Atoms⁡K
Assertion 4atlem10a ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→R≤˙P∨˙Q∨˙V∨˙W↔P∨˙Q∨˙R∨˙W=P∨˙Q∨˙V∨˙W

Proof

Step Hyp Ref Expression
1 4at.l ⊢≤˙=≤K
2 4at.j ⊢∨˙=join⁡K
3 4at.a ⊢A=Atoms⁡K
4 simp11 ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→K∈HL
5 simp21 ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→R∈A
6 simp22 ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→V∈A
7 4 hllatd ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→K∈Lat
8 simp1 ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→K∈HL∧P∈A∧Q∈A
9 eqid ⊢BaseK=BaseK
10 9 2 3 hlatjcl ⊢K∈HL∧P∈A∧Q∈A→P∨˙Q∈BaseK
11 8 10 syl ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→P∨˙Q∈BaseK
12 simp23 ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→W∈A
13 9 3 atbase ⊢W∈A→W∈BaseK
14 12 13 syl ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→W∈BaseK
15 9 2 latjcl ⊢K∈Lat∧P∨˙Q∈BaseK∧W∈BaseK→P∨˙Q∨˙W∈BaseK
16 7 11 14 15 syl3anc ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→P∨˙Q∨˙W∈BaseK
17 simp3 ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→¬R≤˙P∨˙Q∨˙W
18 9 1 2 3 hlexchb2 ⊢K∈HL∧R∈A∧V∈A∧P∨˙Q∨˙W∈BaseK∧¬R≤˙P∨˙Q∨˙W→R≤˙V∨˙P∨˙Q∨˙W↔R∨˙P∨˙Q∨˙W=V∨˙P∨˙Q∨˙W
19 4 5 6 16 17 18 syl131anc ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→R≤˙V∨˙P∨˙Q∨˙W↔R∨˙P∨˙Q∨˙W=V∨˙P∨˙Q∨˙W
20 1 2 3 4atlem4c ⊢K∈HL∧P∈A∧Q∈A∧V∈A∧W∈A→P∨˙Q∨˙V∨˙W=V∨˙P∨˙Q∨˙W
21 8 6 12 20 syl12anc ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→P∨˙Q∨˙V∨˙W=V∨˙P∨˙Q∨˙W
22 21 breq2d ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→R≤˙P∨˙Q∨˙V∨˙W↔R≤˙V∨˙P∨˙Q∨˙W
23 1 2 3 4atlem4c ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧W∈A→P∨˙Q∨˙R∨˙W=R∨˙P∨˙Q∨˙W
24 8 5 12 23 syl12anc ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→P∨˙Q∨˙R∨˙W=R∨˙P∨˙Q∨˙W
25 24 21 eqeq12d ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→P∨˙Q∨˙R∨˙W=P∨˙Q∨˙V∨˙W↔R∨˙P∨˙Q∨˙W=V∨˙P∨˙Q∨˙W
26 19 22 25 3bitr4d ⊢K∈HL∧P∈A∧Q∈A∧R∈A∧V∈A∧W∈A∧¬R≤˙P∨˙Q∨˙W→R≤˙P∨˙Q∨˙V∨˙W↔P∨˙Q∨˙R∨˙W=P∨˙Q∨˙V∨˙W