Proof of Theorem pmodlem1
Step | Hyp | Ref
| Expression |
1 | | simpl11 1136 |
. . . 4
|
2 | | simpl12 1137 |
. . . 4
|
3 | | simpl13 1138 |
. . . . 5
|
4 | | ssinss1 3841 |
. . . . 5
|
5 | 3, 4 | syl 17 |
. . . 4
|
6 | | pmodlem.a |
. . . . 5
|
7 | | pmodlem.p |
. . . . 5
|
8 | 6, 7 | sspadd1 35101 |
. . . 4
|
9 | 1, 2, 5, 8 | syl3anc 1326 |
. . 3
|
10 | | simpr 477 |
. . . 4
|
11 | | simpl31 1142 |
. . . 4
|
12 | 10, 11 | eqeltrd 2701 |
. . 3
|
13 | 9, 12 | sseldd 3604 |
. 2
|
14 | | simpl11 1136 |
. . . 4
|
15 | | hllat 34650 |
. . . 4
|
16 | 14, 15 | syl 17 |
. . 3
|
17 | | simpl12 1137 |
. . 3
|
18 | | simpl13 1138 |
. . . 4
|
19 | 18, 4 | syl 17 |
. . 3
|
20 | | simpl31 1142 |
. . 3
|
21 | | simpl32 1143 |
. . . 4
|
22 | | simpl21 1139 |
. . . . 5
|
23 | | simpl22 1140 |
. . . . 5
|
24 | | simpl23 1141 |
. . . . 5
|
25 | | pmodlem.s |
. . . . . . . . . 10
|
26 | 6, 25 | psubssat 35040 |
. . . . . . . . 9
|
27 | 14, 22, 26 | syl2anc 693 |
. . . . . . . 8
|
28 | 27, 24 | sseldd 3604 |
. . . . . . 7
|
29 | 18, 21 | sseldd 3604 |
. . . . . . 7
|
30 | 17, 20 | sseldd 3604 |
. . . . . . 7
|
31 | 28, 29, 30 | 3jca 1242 |
. . . . . 6
|
32 | | simpr 477 |
. . . . . 6
|
33 | | simpl33 1144 |
. . . . . 6
|
34 | | pmodlem.l |
. . . . . . . 8
|
35 | | pmodlem.j |
. . . . . . . 8
|
36 | 34, 35, 6 | hlatexch1 34681 |
. . . . . . 7
|
37 | 36 | imp 445 |
. . . . . 6
|
38 | 14, 31, 32, 33, 37 | syl31anc 1329 |
. . . . 5
|
39 | | simp31 1097 |
. . . . . . . . 9
|
40 | 39 | snssd 4340 |
. . . . . . . 8
|
41 | | simp22 1095 |
. . . . . . . 8
|
42 | 40, 41 | sstrd 3613 |
. . . . . . 7
|
43 | | simp23 1096 |
. . . . . . . 8
|
44 | 43 | snssd 4340 |
. . . . . . 7
|
45 | | simp11 1091 |
. . . . . . . 8
|
46 | | simp12 1092 |
. . . . . . . . . 10
|
47 | 46, 39 | sseldd 3604 |
. . . . . . . . 9
|
48 | 47 | snssd 4340 |
. . . . . . . 8
|
49 | | simp21 1094 |
. . . . . . . . . . 11
|
50 | 45, 49, 26 | syl2anc 693 |
. . . . . . . . . 10
|
51 | 50, 43 | sseldd 3604 |
. . . . . . . . 9
|
52 | 51 | snssd 4340 |
. . . . . . . 8
|
53 | 6, 25, 7 | paddss 35131 |
. . . . . . . 8
|
54 | 45, 48, 52, 49, 53 | syl13anc 1328 |
. . . . . . 7
|
55 | 42, 44, 54 | mpbi2and 956 |
. . . . . 6
|
56 | | simp33 1099 |
. . . . . . 7
|
57 | 45, 15 | syl 17 |
. . . . . . . 8
|
58 | | simp13 1093 |
. . . . . . . . 9
|
59 | | simp32 1098 |
. . . . . . . . 9
|
60 | 58, 59 | sseldd 3604 |
. . . . . . . 8
|
61 | 34, 35, 6, 7 | elpadd2at2 35093 |
. . . . . . . 8
|
62 | 57, 47, 51, 60, 61 | syl13anc 1328 |
. . . . . . 7
|
63 | 56, 62 | mpbird 247 |
. . . . . 6
|
64 | 55, 63 | sseldd 3604 |
. . . . 5
|
65 | 14, 17, 18, 22, 23, 24, 20, 21, 38, 64 | syl333anc 1358 |
. . . 4
|
66 | 21, 65 | elind 3798 |
. . 3
|
67 | 34, 35, 6, 7 | elpaddri 35088 |
. . 3
|
68 | 16, 17, 19, 20, 66, 28, 33, 67 | syl322anc 1354 |
. 2
|
69 | 13, 68 | pm2.61dane 2881 |
1
|