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 ⊢ φ → T C T ⊕ ˙ U
Assertion lcvexchlem4 ⊢ φ → T ∩ U C U

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 ⊢ φ → T C T ⊕ ˙ 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 → T C T ⊕ ˙ U
37 1 3 4 5 9 lcvbr3 ⊢ φ → T C T ⊕ ˙ U ↔ T ⊂ T ⊕ ˙ U ∧ ∀ r ∈ S T ⊆ r ∧ r ⊆ T ⊕ ˙ U → r = T ∨ r = T ⊕ ˙ U
38 37 adantr ⊢ φ ∧ s ∈ S → T C T ⊕ ˙ U ↔ T ⊂ T ⊕ ˙ U ∧ ∀ r ∈ S T ⊆ 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 ∈ S T ⊆ 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 ∈ S T ⊆ 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 ∈ S T ⊆ 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 → T C T ⊕ ˙ 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 → T C T ⊕ ˙ 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 ∈ S T ∩ 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 ∩ U C U ↔ T ∩ U ⊂ U ∧ ∀ s ∈ S T ∩ U ⊆ s ∧ s ⊆ U → s = T ∩ U ∨ s = U
77 12 73 76 mpbir2and ⊢ φ → T ∩ U C U