Metamath Proof Explorer

Theorem latj4

Description: Rearrangement of lattice join of 4 classes. ( chj4 analog.) (Contributed by NM, 14-Jun-2012)

Ref Expression
Hypotheses latjass.b ⊢B=BaseK
latjass.j ⊢∨˙=join⁡K
Assertion latj4 ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X∨˙Y∨˙Z∨˙W=X∨˙Z∨˙Y∨˙W

Proof

Step Hyp Ref Expression
1 latjass.b ⊢B=BaseK
2 latjass.j ⊢∨˙=join⁡K
3 simp1 ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→K∈Lat
4 simp2r ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→Y∈B
5 simp3l ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→Z∈B
6 simp3r ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→W∈B
7 1 2 latj12 ⊢K∈Lat∧Y∈B∧Z∈B∧W∈B→Y∨˙Z∨˙W=Z∨˙Y∨˙W
8 3 4 5 6 7 syl13anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→Y∨˙Z∨˙W=Z∨˙Y∨˙W
9 8 oveq2d ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X∨˙Y∨˙Z∨˙W=X∨˙Z∨˙Y∨˙W
10 simp2l ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X∈B
11 1 2 latjcl ⊢K∈Lat∧Z∈B∧W∈B→Z∨˙W∈B
12 3 5 6 11 syl3anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→Z∨˙W∈B
13 1 2 latjass ⊢K∈Lat∧X∈B∧Y∈B∧Z∨˙W∈B→X∨˙Y∨˙Z∨˙W=X∨˙Y∨˙Z∨˙W
14 3 10 4 12 13 syl13anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X∨˙Y∨˙Z∨˙W=X∨˙Y∨˙Z∨˙W
15 1 2 latjcl ⊢K∈Lat∧Y∈B∧W∈B→Y∨˙W∈B
16 3 4 6 15 syl3anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→Y∨˙W∈B
17 1 2 latjass ⊢K∈Lat∧X∈B∧Z∈B∧Y∨˙W∈B→X∨˙Z∨˙Y∨˙W=X∨˙Z∨˙Y∨˙W
18 3 10 5 16 17 syl13anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X∨˙Z∨˙Y∨˙W=X∨˙Z∨˙Y∨˙W
19 9 14 18 3eqtr4d ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X∨˙Y∨˙Z∨˙W=X∨˙Z∨˙Y∨˙W