Metamath Proof Explorer


Theorem lcfrlem21

Description: Lemma for lcfr . (Contributed by NM, 11-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h H=LHypK
lcfrlem17.o ˙=ocHKW
lcfrlem17.u U=DVecHKW
lcfrlem17.v V=BaseU
lcfrlem17.p +˙=+U
lcfrlem17.z 0˙=0U
lcfrlem17.n N=LSpanU
lcfrlem17.a A=LSAtomsU
lcfrlem17.k φKHLWH
lcfrlem17.x φXV0˙
lcfrlem17.y φYV0˙
lcfrlem17.ne φNXNY
Assertion lcfrlem21 φNXY˙X+˙YA

Proof

Step Hyp Ref Expression
1 lcfrlem17.h H=LHypK
2 lcfrlem17.o ˙=ocHKW
3 lcfrlem17.u U=DVecHKW
4 lcfrlem17.v V=BaseU
5 lcfrlem17.p +˙=+U
6 lcfrlem17.z 0˙=0U
7 lcfrlem17.n N=LSpanU
8 lcfrlem17.a A=LSAtomsU
9 lcfrlem17.k φKHLWH
10 lcfrlem17.x φXV0˙
11 lcfrlem17.y φYV0˙
12 lcfrlem17.ne φNXNY
13 9 adantr φ¬X˙X+˙YKHLWH
14 10 adantr φ¬X˙X+˙YXV0˙
15 11 adantr φ¬X˙X+˙YYV0˙
16 12 adantr φ¬X˙X+˙YNXNY
17 simpr φ¬X˙X+˙Y¬X˙X+˙Y
18 1 2 3 4 5 6 7 8 13 14 15 16 17 lcfrlem20 φ¬X˙X+˙YNXY˙X+˙YA
19 1 3 9 dvhlmod φULMod
20 10 eldifad φXV
21 11 eldifad φYV
22 4 5 lmodcom ULModXVYVX+˙Y=Y+˙X
23 19 20 21 22 syl3anc φX+˙Y=Y+˙X
24 23 sneqd φX+˙Y=Y+˙X
25 24 fveq2d φ˙X+˙Y=˙Y+˙X
26 25 eleq2d φY˙X+˙YY˙Y+˙X
27 26 biimprd φY˙Y+˙XY˙X+˙Y
28 27 con3dimp φ¬Y˙X+˙Y¬Y˙Y+˙X
29 prcom XY=YX
30 29 fveq2i NXY=NYX
31 30 a1i φNXY=NYX
32 31 25 ineq12d φNXY˙X+˙Y=NYX˙Y+˙X
33 32 adantr φ¬Y˙Y+˙XNXY˙X+˙Y=NYX˙Y+˙X
34 9 adantr φ¬Y˙Y+˙XKHLWH
35 11 adantr φ¬Y˙Y+˙XYV0˙
36 10 adantr φ¬Y˙Y+˙XXV0˙
37 12 necomd φNYNX
38 37 adantr φ¬Y˙Y+˙XNYNX
39 simpr φ¬Y˙Y+˙X¬Y˙Y+˙X
40 1 2 3 4 5 6 7 8 34 35 36 38 39 lcfrlem20 φ¬Y˙Y+˙XNYX˙Y+˙XA
41 33 40 eqeltrd φ¬Y˙Y+˙XNXY˙X+˙YA
42 28 41 syldan φ¬Y˙X+˙YNXY˙X+˙YA
43 1 2 3 4 5 6 7 8 9 10 11 12 lcfrlem19 φ¬X˙X+˙Y¬Y˙X+˙Y
44 18 42 43 mpjaodan φNXY˙X+˙YA