Description: Two atoms covering the zero subspace are equal. ( atcv1 analog.) (Contributed by NM, 29-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | atcvrj0.b | |
|
atcvrj0.j | |
||
atcvrj0.z | |
||
atcvrj0.c | |
||
atcvrj0.a | |
||
Assertion | atcvrj0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atcvrj0.b | |
|
2 | atcvrj0.j | |
|
3 | atcvrj0.z | |
|
4 | atcvrj0.c | |
|
5 | atcvrj0.a | |
|
6 | breq1 | |
|
7 | 6 | biimpd | |
8 | 7 | adantl | |
9 | 2 3 4 5 | atcvr0eq | |
10 | 9 | 3adant3r1 | |
11 | 10 | adantr | |
12 | 8 11 | sylibd | |
13 | 12 | ex | |
14 | 13 | com23 | |
15 | 14 | 3impia | |
16 | oveq1 | |
|
17 | 16 | breq2d | |
18 | 17 | biimpac | |
19 | simpr3 | |
|
20 | 2 5 | hlatjidm | |
21 | 19 20 | syldan | |
22 | 21 | breq2d | |
23 | hlatl | |
|
24 | 23 | adantr | |
25 | simpr1 | |
|
26 | eqid | |
|
27 | 1 26 3 4 5 | atcvreq0 | |
28 | 24 25 19 27 | syl3anc | |
29 | 28 | biimpd | |
30 | 22 29 | sylbid | |
31 | 18 30 | syl5 | |
32 | 31 | expd | |
33 | 32 | 3impia | |
34 | 15 33 | impbid | |