Metamath Proof Explorer


Theorem pl42lem1N

Description: Lemma for pl42N . (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pl42lem.b B = Base K
pl42lem.l ˙ = K
pl42lem.j ˙ = join K
pl42lem.m ˙ = meet K
pl42lem.o ˙ = oc K
pl42lem.f F = pmap K
pl42lem.p + ˙ = + 𝑃 K
Assertion pl42lem1N K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y ˙ Z ˙ W ˙ V = F X + ˙ F Y F Z + ˙ F W F V

Proof

Step Hyp Ref Expression
1 pl42lem.b B = Base K
2 pl42lem.l ˙ = K
3 pl42lem.j ˙ = join K
4 pl42lem.m ˙ = meet K
5 pl42lem.o ˙ = oc K
6 pl42lem.f F = pmap K
7 pl42lem.p + ˙ = + 𝑃 K
8 simp11 K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W K HL
9 8 hllatd K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W K Lat
10 simp12 K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W X B
11 simp13 K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W Y B
12 1 3 latjcl K Lat X B Y B X ˙ Y B
13 9 10 11 12 syl3anc K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W X ˙ Y B
14 simp21 K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W Z B
15 1 4 latmcl K Lat X ˙ Y B Z B X ˙ Y ˙ Z B
16 9 13 14 15 syl3anc K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W X ˙ Y ˙ Z B
17 simp22 K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W W B
18 1 3 latjcl K Lat X ˙ Y ˙ Z B W B X ˙ Y ˙ Z ˙ W B
19 9 16 17 18 syl3anc K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W X ˙ Y ˙ Z ˙ W B
20 simp23 K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W V B
21 eqid Atoms K = Atoms K
22 1 4 21 6 pmapmeet K HL X ˙ Y ˙ Z ˙ W B V B F X ˙ Y ˙ Z ˙ W ˙ V = F X ˙ Y ˙ Z ˙ W F V
23 8 19 20 22 syl3anc K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y ˙ Z ˙ W ˙ V = F X ˙ Y ˙ Z ˙ W F V
24 hlop K HL K OP
25 8 24 syl K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W K OP
26 1 5 opoccl K OP W B ˙ W B
27 25 17 26 syl2anc K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W ˙ W B
28 1 2 4 latmle2 K Lat X ˙ Y B Z B X ˙ Y ˙ Z ˙ Z
29 9 13 14 28 syl3anc K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W X ˙ Y ˙ Z ˙ Z
30 simp3r K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W Z ˙ ˙ W
31 1 2 9 16 14 27 29 30 lattrd K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W X ˙ Y ˙ Z ˙ ˙ W
32 1 2 3 6 5 7 pmapojoinN K HL X ˙ Y ˙ Z B W B X ˙ Y ˙ Z ˙ ˙ W F X ˙ Y ˙ Z ˙ W = F X ˙ Y ˙ Z + ˙ F W
33 8 16 17 31 32 syl31anc K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y ˙ Z ˙ W = F X ˙ Y ˙ Z + ˙ F W
34 1 4 21 6 pmapmeet K HL X ˙ Y B Z B F X ˙ Y ˙ Z = F X ˙ Y F Z
35 8 13 14 34 syl3anc K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y ˙ Z = F X ˙ Y F Z
36 simp3l K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W X ˙ ˙ Y
37 1 2 3 6 5 7 pmapojoinN K HL X B Y B X ˙ ˙ Y F X ˙ Y = F X + ˙ F Y
38 8 10 11 36 37 syl31anc K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y = F X + ˙ F Y
39 38 ineq1d K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y F Z = F X + ˙ F Y F Z
40 35 39 eqtrd K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y ˙ Z = F X + ˙ F Y F Z
41 40 oveq1d K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y ˙ Z + ˙ F W = F X + ˙ F Y F Z + ˙ F W
42 33 41 eqtrd K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y ˙ Z ˙ W = F X + ˙ F Y F Z + ˙ F W
43 42 ineq1d K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y ˙ Z ˙ W F V = F X + ˙ F Y F Z + ˙ F W F V
44 23 43 eqtrd K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y ˙ Z ˙ W ˙ V = F X + ˙ F Y F Z + ˙ F W F V
45 44 3expia K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X ˙ Y ˙ Z ˙ W ˙ V = F X + ˙ F Y F Z + ˙ F W F V