Metamath Proof Explorer


Theorem 3atlem5

Description: Lemma for 3at . (Contributed by NM, 23-Jun-2012)

Ref Expression
Hypotheses 3at.l ˙=K
3at.j ˙=joinK
3at.a A=AtomsK
Assertion 3atlem5 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UP˙Q˙R˙S˙T˙UP˙Q˙R=S˙T˙U

Proof

Step Hyp Ref Expression
1 3at.l ˙=K
2 3at.j ˙=joinK
3 3at.a A=AtomsK
4 oveq2 U=PS˙T˙U=S˙T˙P
5 4 eqcoms P=US˙T˙U=S˙T˙P
6 5 breq2d P=UP˙Q˙R˙S˙T˙UP˙Q˙R˙S˙T˙P
7 5 eqeq2d P=UP˙Q˙R=S˙T˙UP˙Q˙R=S˙T˙P
8 6 7 imbi12d P=UP˙Q˙R˙S˙T˙UP˙Q˙R=S˙T˙UP˙Q˙R˙S˙T˙PP˙Q˙R=S˙T˙P
9 simp1l KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UPUP˙Q˙R˙S˙T˙UKHLPAQARASATAUA
10 simp1r1 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UPUP˙Q˙R˙S˙T˙U¬R˙P˙Q
11 simp2 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UPUP˙Q˙R˙S˙T˙UPU
12 simp1r3 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UPUP˙Q˙R˙S˙T˙U¬Q˙P˙U
13 simp3 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UPUP˙Q˙R˙S˙T˙UP˙Q˙R˙S˙T˙U
14 1 2 3 3atlem3 KHLPAQARASATAUA¬R˙P˙QPU¬Q˙P˙UP˙Q˙R˙S˙T˙UP˙Q˙R=S˙T˙U
15 9 10 11 12 13 14 syl131anc KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UPUP˙Q˙R˙S˙T˙UP˙Q˙R=S˙T˙U
16 15 3expia KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UPUP˙Q˙R˙S˙T˙UP˙Q˙R=S˙T˙U
17 simp11 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PKHL
18 simp123 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PRA
19 simp122 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PQA
20 simp121 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PPA
21 18 19 20 3jca KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PRAQAPA
22 simp131 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PSA
23 simp132 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PTA
24 22 23 jca KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PSATA
25 simp21 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙P¬R˙P˙Q
26 simp22 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PPQ
27 1 2 3 hlatexch2 KHLPARAQAPQP˙R˙QR˙P˙Q
28 17 20 18 19 26 27 syl131anc KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PP˙R˙QR˙P˙Q
29 25 28 mtod KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙P¬P˙R˙Q
30 17 hllatd KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PKLat
31 eqid BaseK=BaseK
32 31 3 atbase RARBaseK
33 18 32 syl KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PRBaseK
34 31 3 atbase PAPBaseK
35 20 34 syl KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PPBaseK
36 31 3 atbase QAQBaseK
37 19 36 syl KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PQBaseK
38 31 1 2 latnlej1r KLatRBaseKPBaseKQBaseK¬R˙P˙QRQ
39 30 33 35 37 25 38 syl131anc KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PRQ
40 simp3 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PR˙Q˙P˙S˙T˙P
41 1 2 3 3atlem4 KHLRAQAPASATA¬P˙R˙QRQR˙Q˙P˙S˙T˙PR˙Q˙P=S˙T˙P
42 17 21 24 29 39 40 41 syl321anc KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PR˙Q˙P=S˙T˙P
43 42 3expia KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UR˙Q˙P˙S˙T˙PR˙Q˙P=S˙T˙P
44 simpl1 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UKHL
45 44 hllatd KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UKLat
46 simpl21 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UPA
47 46 34 syl KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UPBaseK
48 simpl22 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UQA
49 48 36 syl KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UQBaseK
50 simpl23 KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙URA
51 50 32 syl KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙URBaseK
52 31 2 latj31 KLatPBaseKQBaseKRBaseKP˙Q˙R=R˙Q˙P
53 45 47 49 51 52 syl13anc KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UP˙Q˙R=R˙Q˙P
54 53 breq1d KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UP˙Q˙R˙S˙T˙PR˙Q˙P˙S˙T˙P
55 53 eqeq1d KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UP˙Q˙R=S˙T˙PR˙Q˙P=S˙T˙P
56 43 54 55 3imtr4d KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UP˙Q˙R˙S˙T˙PP˙Q˙R=S˙T˙P
57 8 16 56 pm2.61ne KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UP˙Q˙R˙S˙T˙UP˙Q˙R=S˙T˙U
58 57 3impia KHLPAQARASATAUA¬R˙P˙QPQ¬Q˙P˙UP˙Q˙R˙S˙T˙UP˙Q˙R=S˙T˙U