Metamath Proof Explorer


Theorem pl42lem4N

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 pl42lem4N 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 ˙ X ˙ W ˙ Y ˙ 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 1 2 3 4 5 6 7 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
9 8 3impia 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
10 1 2 3 4 5 6 7 pl42lem3N K HL X B Y B Z B W B V B F X + ˙ F Y F Z + ˙ F W F V F X + ˙ F Y + ˙ F W F X + ˙ F Y + ˙ F V
11 simpl1 K HL X B Y B Z B W B V B K HL
12 11 hllatd K HL X B Y B Z B W B V B K Lat
13 simpl2 K HL X B Y B Z B W B V B X B
14 eqid PSubSp K = PSubSp K
15 1 14 6 pmapsub K Lat X B F X PSubSp K
16 12 13 15 syl2anc K HL X B Y B Z B W B V B F X PSubSp K
17 simpl3 K HL X B Y B Z B W B V B Y B
18 1 14 6 pmapsub K Lat Y B F Y PSubSp K
19 12 17 18 syl2anc K HL X B Y B Z B W B V B F Y PSubSp K
20 simpr2 K HL X B Y B Z B W B V B W B
21 1 14 6 pmapsub K Lat W B F W PSubSp K
22 12 20 21 syl2anc K HL X B Y B Z B W B V B F W PSubSp K
23 simpr3 K HL X B Y B Z B W B V B V B
24 1 14 6 pmapsub K Lat V B F V PSubSp K
25 12 23 24 syl2anc K HL X B Y B Z B W B V B F V PSubSp K
26 14 7 pmodl42N K HL F X PSubSp K F Y PSubSp K F W PSubSp K F V PSubSp K F X + ˙ F Y + ˙ F W F X + ˙ F Y + ˙ F V = F X + ˙ F Y + ˙ F X + ˙ F W F Y + ˙ F V
27 11 16 19 22 25 26 syl32anc K HL X B Y B Z B W B V B F X + ˙ F Y + ˙ F W F X + ˙ F Y + ˙ F V = F X + ˙ F Y + ˙ F X + ˙ F W F Y + ˙ F V
28 1 2 3 4 5 6 7 pl42lem2N K HL X B Y B Z B W B V B F X + ˙ F Y + ˙ F X + ˙ F W F Y + ˙ F V F X ˙ Y ˙ X ˙ W ˙ Y ˙ V
29 27 28 eqsstrd K HL X B Y B Z B W B V B F X + ˙ F Y + ˙ F W F X + ˙ F Y + ˙ F V F X ˙ Y ˙ X ˙ W ˙ Y ˙ V
30 10 29 sstrd K HL X B Y B Z B W B V B F X + ˙ F Y F Z + ˙ F W F V F X ˙ Y ˙ X ˙ W ˙ Y ˙ V
31 30 3adant3 K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W F X + ˙ F Y F Z + ˙ F W F V F X ˙ Y ˙ X ˙ W ˙ Y ˙ V
32 9 31 eqsstrd 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 ˙ X ˙ W ˙ Y ˙ V
33 32 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 ˙ Y ˙ X ˙ W ˙ Y ˙ V