Metamath Proof Explorer


Theorem pl42lem3N

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 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

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 simpl1 K HL X B Y B Z B W B V B K HL
9 simpl2 K HL X B Y B Z B W B V B X B
10 eqid Atoms K = Atoms K
11 1 10 6 pmapssat K HL X B F X Atoms K
12 8 9 11 syl2anc K HL X B Y B Z B W B V B F X Atoms K
13 simpl3 K HL X B Y B Z B W B V B Y B
14 1 10 6 pmapssat K HL Y B F Y Atoms K
15 8 13 14 syl2anc K HL X B Y B Z B W B V B F Y Atoms K
16 10 7 paddssat K HL F X Atoms K F Y Atoms K F X + ˙ F Y Atoms K
17 8 12 15 16 syl3anc K HL X B Y B Z B W B V B F X + ˙ F Y Atoms K
18 simpr2 K HL X B Y B Z B W B V B W B
19 1 10 6 pmapssat K HL W B F W Atoms K
20 8 18 19 syl2anc K HL X B Y B Z B W B V B F W Atoms K
21 inss1 F X + ˙ F Y F Z F X + ˙ F Y
22 10 7 paddss1 K HL F X + ˙ F Y Atoms K F W Atoms K F X + ˙ F Y F Z F X + ˙ F Y F X + ˙ F Y F Z + ˙ F W F X + ˙ F Y + ˙ F W
23 21 22 mpi K HL F X + ˙ F Y Atoms K F W Atoms K F X + ˙ F Y F Z + ˙ F W F X + ˙ F Y + ˙ F W
24 8 17 20 23 syl3anc K HL X B Y B Z B W B V B F X + ˙ F Y F Z + ˙ F W F X + ˙ F Y + ˙ F W
25 simpr3 K HL X B Y B Z B W B V B V B
26 1 10 6 pmapssat K HL V B F V Atoms K
27 8 25 26 syl2anc K HL X B Y B Z B W B V B F V Atoms K
28 10 7 sspadd2 K HL F V Atoms K F X + ˙ F Y Atoms K F V F X + ˙ F Y + ˙ F V
29 8 27 17 28 syl3anc K HL X B Y B Z B W B V B F V F X + ˙ F Y + ˙ F V
30 ss2in F X + ˙ F Y F Z + ˙ F W F X + ˙ F Y + ˙ F W F V F X + ˙ F Y + ˙ F V F X + ˙ F Y F Z + ˙ F W F V F X + ˙ F Y + ˙ F W F X + ˙ F Y + ˙ F V
31 24 29 30 syl2anc 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