Metamath Proof Explorer

Theorem lcvexchlem4

Description: Lemma for lcvexch . (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lcvexch.s ⊢S=LSubSp⁡W
lcvexch.p ⊢⊕˙=LSSum⁡W
lcvexch.c ⊢C=⋖L⁡W
lcvexch.w ⊢φ→W∈LMod
lcvexch.t ⊢φ→T∈S
lcvexch.u ⊢φ→U∈S
lcvexch.f ⊢φ→TCT⊕˙U
Assertion lcvexchlem4 ⊢φ→T∩UCU

Proof

Step Hyp Ref Expression
1 lcvexch.s ⊢S=LSubSp⁡W
2 lcvexch.p ⊢⊕˙=LSSum⁡W
3 lcvexch.c ⊢C=⋖L⁡W
4 lcvexch.w ⊢φ→W∈LMod
5 lcvexch.t ⊢φ→T∈S
6 lcvexch.u ⊢φ→U∈S
7 lcvexch.f ⊢φ→TCT⊕˙U
8 1 2 lsmcl ⊢W∈LMod∧T∈S∧U∈S→T⊕˙U∈S
9 4 5 6 8 syl3anc ⊢φ→T⊕˙U∈S
10 1 3 4 5 9 7 lcvpss ⊢φ→T⊂T⊕˙U
11 1 2 3 4 5 6 lcvexchlem1 ⊢φ→T⊂T⊕˙U↔T∩U⊂U
12 10 11 mpbid ⊢φ→T∩U⊂U
13 4 3ad2ant1 ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→W∈LMod
14 1 lsssssubg ⊢W∈LMod→S⊆SubGrp⁡W
15 13 14 syl ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→S⊆SubGrp⁡W
16 simp2 ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s∈S
17 15 16 sseldd ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s∈SubGrp⁡W
18 5 3ad2ant1 ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→T∈S
19 15 18 sseldd ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→T∈SubGrp⁡W
20 2 lsmub2 ⊢s∈SubGrp⁡W∧T∈SubGrp⁡W→T⊆s⊕˙T
21 17 19 20 syl2anc ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→T⊆s⊕˙T
22 6 3ad2ant1 ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→U∈S
23 15 22 sseldd ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→U∈SubGrp⁡W
24 simp3r ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s⊆U
25 2 lsmless1 ⊢U∈SubGrp⁡W∧T∈SubGrp⁡W∧s⊆U→s⊕˙T⊆U⊕˙T
26 23 19 24 25 syl3anc ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s⊕˙T⊆U⊕˙T
27 lmodabl ⊢W∈LMod→W∈Abel
28 4 27 syl ⊢φ→W∈Abel
29 4 14 syl ⊢φ→S⊆SubGrp⁡W
30 29 5 sseldd ⊢φ→T∈SubGrp⁡W
31 29 6 sseldd ⊢φ→U∈SubGrp⁡W
32 2 lsmcom ⊢W∈Abel∧T∈SubGrp⁡W∧U∈SubGrp⁡W→T⊕˙U=U⊕˙T
33 28 30 31 32 syl3anc ⊢φ→T⊕˙U=U⊕˙T
34 33 3ad2ant1 ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→T⊕˙U=U⊕˙T
35 26 34 sseqtrrd ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s⊕˙T⊆T⊕˙U
36 7 3ad2ant1 ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→TCT⊕˙U
37 1 3 4 5 9 lcvbr3 ⊢φ→TCT⊕˙U↔T⊂T⊕˙U∧∀r∈ST⊆r∧r⊆T⊕˙U→r=T∨r=T⊕˙U
38 37 adantr ⊢φ∧s∈S→TCT⊕˙U↔T⊂T⊕˙U∧∀r∈ST⊆r∧r⊆T⊕˙U→r=T∨r=T⊕˙U
39 4 adantr ⊢φ∧s∈S→W∈LMod
40 simpr ⊢φ∧s∈S→s∈S
41 5 adantr ⊢φ∧s∈S→T∈S
42 1 2 lsmcl ⊢W∈LMod∧s∈S∧T∈S→s⊕˙T∈S
43 39 40 41 42 syl3anc ⊢φ∧s∈S→s⊕˙T∈S
44 sseq2 ⊢r=s⊕˙T→T⊆r↔T⊆s⊕˙T
45 sseq1 ⊢r=s⊕˙T→r⊆T⊕˙U↔s⊕˙T⊆T⊕˙U
46 44 45 anbi12d ⊢r=s⊕˙T→T⊆r∧r⊆T⊕˙U↔T⊆s⊕˙T∧s⊕˙T⊆T⊕˙U
47 eqeq1 ⊢r=s⊕˙T→r=T↔s⊕˙T=T
48 eqeq1 ⊢r=s⊕˙T→r=T⊕˙U↔s⊕˙T=T⊕˙U
49 47 48 orbi12d ⊢r=s⊕˙T→r=T∨r=T⊕˙U↔s⊕˙T=T∨s⊕˙T=T⊕˙U
50 46 49 imbi12d ⊢r=s⊕˙T→T⊆r∧r⊆T⊕˙U→r=T∨r=T⊕˙U↔T⊆s⊕˙T∧s⊕˙T⊆T⊕˙U→s⊕˙T=T∨s⊕˙T=T⊕˙U
51 50 rspcv ⊢s⊕˙T∈S→∀r∈ST⊆r∧r⊆T⊕˙U→r=T∨r=T⊕˙U→T⊆s⊕˙T∧s⊕˙T⊆T⊕˙U→s⊕˙T=T∨s⊕˙T=T⊕˙U
52 43 51 syl ⊢φ∧s∈S→∀r∈ST⊆r∧r⊆T⊕˙U→r=T∨r=T⊕˙U→T⊆s⊕˙T∧s⊕˙T⊆T⊕˙U→s⊕˙T=T∨s⊕˙T=T⊕˙U
53 52 adantld ⊢φ∧s∈S→T⊂T⊕˙U∧∀r∈ST⊆r∧r⊆T⊕˙U→r=T∨r=T⊕˙U→T⊆s⊕˙T∧s⊕˙T⊆T⊕˙U→s⊕˙T=T∨s⊕˙T=T⊕˙U
54 38 53 sylbid ⊢φ∧s∈S→TCT⊕˙U→T⊆s⊕˙T∧s⊕˙T⊆T⊕˙U→s⊕˙T=T∨s⊕˙T=T⊕˙U
55 54 3adant3 ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→TCT⊕˙U→T⊆s⊕˙T∧s⊕˙T⊆T⊕˙U→s⊕˙T=T∨s⊕˙T=T⊕˙U
56 36 55 mpd ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→T⊆s⊕˙T∧s⊕˙T⊆T⊕˙U→s⊕˙T=T∨s⊕˙T=T⊕˙U
57 21 35 56 mp2and ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s⊕˙T=T∨s⊕˙T=T⊕˙U
58 ineq1 ⊢s⊕˙T=T→s⊕˙T∩U=T∩U
59 simp3l ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→T∩U⊆s
60 1 2 3 13 18 22 16 59 24 lcvexchlem2 ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s⊕˙T∩U=s
61 60 eqeq1d ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s⊕˙T∩U=T∩U↔s=T∩U
62 58 61 imbitrid ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s⊕˙T=T→s=T∩U
63 ineq1 ⊢s⊕˙T=T⊕˙U→s⊕˙T∩U=T⊕˙U∩U
64 2 lsmub2 ⊢T∈SubGrp⁡W∧U∈SubGrp⁡W→U⊆T⊕˙U
65 19 23 64 syl2anc ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→U⊆T⊕˙U
66 sseqin2 ⊢U⊆T⊕˙U↔T⊕˙U∩U=U
67 65 66 sylib ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→T⊕˙U∩U=U
68 60 67 eqeq12d ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s⊕˙T∩U=T⊕˙U∩U↔s=U
69 63 68 imbitrid ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s⊕˙T=T⊕˙U→s=U
70 62 69 orim12d ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s⊕˙T=T∨s⊕˙T=T⊕˙U→s=T∩U∨s=U
71 57 70 mpd ⊢φ∧s∈S∧T∩U⊆s∧s⊆U→s=T∩U∨s=U
72 71 3exp ⊢φ→s∈S→T∩U⊆s∧s⊆U→s=T∩U∨s=U
73 72 ralrimiv ⊢φ→∀s∈ST∩U⊆s∧s⊆U→s=T∩U∨s=U
74 1 lssincl ⊢W∈LMod∧T∈S∧U∈S→T∩U∈S
75 4 5 6 74 syl3anc ⊢φ→T∩U∈S
76 1 3 4 75 6 lcvbr3 ⊢φ→T∩UCU↔T∩U⊂U∧∀s∈ST∩U⊆s∧s⊆U→s=T∩U∨s=U
77 12 73 76 mpbir2and ⊢φ→T∩UCU