Metamath Proof Explorer


Theorem atcvrj0

Description: Two atoms covering the zero subspace are equal. ( atcv1 analog.) (Contributed by NM, 29-Nov-2011)

Ref Expression
Hypotheses atcvrj0.b B=BaseK
atcvrj0.j ˙=joinK
atcvrj0.z 0˙=0.K
atcvrj0.c C=K
atcvrj0.a A=AtomsK
Assertion atcvrj0 KHLXBPAQAXCP˙QX=0˙P=Q

Proof

Step Hyp Ref Expression
1 atcvrj0.b B=BaseK
2 atcvrj0.j ˙=joinK
3 atcvrj0.z 0˙=0.K
4 atcvrj0.c C=K
5 atcvrj0.a A=AtomsK
6 breq1 X=0˙XCP˙Q0˙CP˙Q
7 6 biimpd X=0˙XCP˙Q0˙CP˙Q
8 7 adantl KHLXBPAQAX=0˙XCP˙Q0˙CP˙Q
9 2 3 4 5 atcvr0eq KHLPAQA0˙CP˙QP=Q
10 9 3adant3r1 KHLXBPAQA0˙CP˙QP=Q
11 10 adantr KHLXBPAQAX=0˙0˙CP˙QP=Q
12 8 11 sylibd KHLXBPAQAX=0˙XCP˙QP=Q
13 12 ex KHLXBPAQAX=0˙XCP˙QP=Q
14 13 com23 KHLXBPAQAXCP˙QX=0˙P=Q
15 14 3impia KHLXBPAQAXCP˙QX=0˙P=Q
16 oveq1 P=QP˙Q=Q˙Q
17 16 breq2d P=QXCP˙QXCQ˙Q
18 17 biimpac XCP˙QP=QXCQ˙Q
19 simpr3 KHLXBPAQAQA
20 2 5 hlatjidm KHLQAQ˙Q=Q
21 19 20 syldan KHLXBPAQAQ˙Q=Q
22 21 breq2d KHLXBPAQAXCQ˙QXCQ
23 hlatl KHLKAtLat
24 23 adantr KHLXBPAQAKAtLat
25 simpr1 KHLXBPAQAXB
26 eqid K=K
27 1 26 3 4 5 atcvreq0 KAtLatXBQAXCQX=0˙
28 24 25 19 27 syl3anc KHLXBPAQAXCQX=0˙
29 28 biimpd KHLXBPAQAXCQX=0˙
30 22 29 sylbid KHLXBPAQAXCQ˙QX=0˙
31 18 30 syl5 KHLXBPAQAXCP˙QP=QX=0˙
32 31 expd KHLXBPAQAXCP˙QP=QX=0˙
33 32 3impia KHLXBPAQAXCP˙QP=QX=0˙
34 15 33 impbid KHLXBPAQAXCP˙QX=0˙P=Q