Metamath Proof Explorer


Theorem lcvexchlem5

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

Ref Expression
Hypotheses lcvexch.s 𝑆 = ( LSubSp ‘ 𝑊 )
lcvexch.p = ( LSSum ‘ 𝑊 )
lcvexch.c 𝐶 = ( ⋖L𝑊 )
lcvexch.w ( 𝜑𝑊 ∈ LMod )
lcvexch.t ( 𝜑𝑇𝑆 )
lcvexch.u ( 𝜑𝑈𝑆 )
lcvexch.g ( 𝜑 → ( 𝑇𝑈 ) 𝐶 𝑈 )
Assertion lcvexchlem5 ( 𝜑𝑇 𝐶 ( 𝑇 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lcvexch.s 𝑆 = ( LSubSp ‘ 𝑊 )
2 lcvexch.p = ( LSSum ‘ 𝑊 )
3 lcvexch.c 𝐶 = ( ⋖L𝑊 )
4 lcvexch.w ( 𝜑𝑊 ∈ LMod )
5 lcvexch.t ( 𝜑𝑇𝑆 )
6 lcvexch.u ( 𝜑𝑈𝑆 )
7 lcvexch.g ( 𝜑 → ( 𝑇𝑈 ) 𝐶 𝑈 )
8 1 lssincl ( ( 𝑊 ∈ LMod ∧ 𝑇𝑆𝑈𝑆 ) → ( 𝑇𝑈 ) ∈ 𝑆 )
9 4 5 6 8 syl3anc ( 𝜑 → ( 𝑇𝑈 ) ∈ 𝑆 )
10 1 3 4 9 6 7 lcvpss ( 𝜑 → ( 𝑇𝑈 ) ⊊ 𝑈 )
11 1 2 3 4 5 6 lcvexchlem1 ( 𝜑 → ( 𝑇 ⊊ ( 𝑇 𝑈 ) ↔ ( 𝑇𝑈 ) ⊊ 𝑈 ) )
12 10 11 mpbird ( 𝜑𝑇 ⊊ ( 𝑇 𝑈 ) )
13 simp3l ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → 𝑇𝑠 )
14 13 ssrind ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) )
15 inss2 ( 𝑠𝑈 ) ⊆ 𝑈
16 14 15 jctir ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) ∧ ( 𝑠𝑈 ) ⊆ 𝑈 ) )
17 7 3ad2ant1 ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( 𝑇𝑈 ) 𝐶 𝑈 )
18 1 3 4 9 6 lcvbr3 ( 𝜑 → ( ( 𝑇𝑈 ) 𝐶 𝑈 ↔ ( ( 𝑇𝑈 ) ⊊ 𝑈 ∧ ∀ 𝑟𝑆 ( ( ( 𝑇𝑈 ) ⊆ 𝑟𝑟𝑈 ) → ( 𝑟 = ( 𝑇𝑈 ) ∨ 𝑟 = 𝑈 ) ) ) ) )
19 18 adantr ( ( 𝜑𝑠𝑆 ) → ( ( 𝑇𝑈 ) 𝐶 𝑈 ↔ ( ( 𝑇𝑈 ) ⊊ 𝑈 ∧ ∀ 𝑟𝑆 ( ( ( 𝑇𝑈 ) ⊆ 𝑟𝑟𝑈 ) → ( 𝑟 = ( 𝑇𝑈 ) ∨ 𝑟 = 𝑈 ) ) ) ) )
20 4 adantr ( ( 𝜑𝑠𝑆 ) → 𝑊 ∈ LMod )
21 simpr ( ( 𝜑𝑠𝑆 ) → 𝑠𝑆 )
22 6 adantr ( ( 𝜑𝑠𝑆 ) → 𝑈𝑆 )
23 1 lssincl ( ( 𝑊 ∈ LMod ∧ 𝑠𝑆𝑈𝑆 ) → ( 𝑠𝑈 ) ∈ 𝑆 )
24 20 21 22 23 syl3anc ( ( 𝜑𝑠𝑆 ) → ( 𝑠𝑈 ) ∈ 𝑆 )
25 sseq2 ( 𝑟 = ( 𝑠𝑈 ) → ( ( 𝑇𝑈 ) ⊆ 𝑟 ↔ ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) ) )
26 sseq1 ( 𝑟 = ( 𝑠𝑈 ) → ( 𝑟𝑈 ↔ ( 𝑠𝑈 ) ⊆ 𝑈 ) )
27 25 26 anbi12d ( 𝑟 = ( 𝑠𝑈 ) → ( ( ( 𝑇𝑈 ) ⊆ 𝑟𝑟𝑈 ) ↔ ( ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) ∧ ( 𝑠𝑈 ) ⊆ 𝑈 ) ) )
28 eqeq1 ( 𝑟 = ( 𝑠𝑈 ) → ( 𝑟 = ( 𝑇𝑈 ) ↔ ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ) )
29 eqeq1 ( 𝑟 = ( 𝑠𝑈 ) → ( 𝑟 = 𝑈 ↔ ( 𝑠𝑈 ) = 𝑈 ) )
30 28 29 orbi12d ( 𝑟 = ( 𝑠𝑈 ) → ( ( 𝑟 = ( 𝑇𝑈 ) ∨ 𝑟 = 𝑈 ) ↔ ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ∨ ( 𝑠𝑈 ) = 𝑈 ) ) )
31 27 30 imbi12d ( 𝑟 = ( 𝑠𝑈 ) → ( ( ( ( 𝑇𝑈 ) ⊆ 𝑟𝑟𝑈 ) → ( 𝑟 = ( 𝑇𝑈 ) ∨ 𝑟 = 𝑈 ) ) ↔ ( ( ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) ∧ ( 𝑠𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ∨ ( 𝑠𝑈 ) = 𝑈 ) ) ) )
32 31 rspcv ( ( 𝑠𝑈 ) ∈ 𝑆 → ( ∀ 𝑟𝑆 ( ( ( 𝑇𝑈 ) ⊆ 𝑟𝑟𝑈 ) → ( 𝑟 = ( 𝑇𝑈 ) ∨ 𝑟 = 𝑈 ) ) → ( ( ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) ∧ ( 𝑠𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ∨ ( 𝑠𝑈 ) = 𝑈 ) ) ) )
33 24 32 syl ( ( 𝜑𝑠𝑆 ) → ( ∀ 𝑟𝑆 ( ( ( 𝑇𝑈 ) ⊆ 𝑟𝑟𝑈 ) → ( 𝑟 = ( 𝑇𝑈 ) ∨ 𝑟 = 𝑈 ) ) → ( ( ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) ∧ ( 𝑠𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ∨ ( 𝑠𝑈 ) = 𝑈 ) ) ) )
34 33 adantld ( ( 𝜑𝑠𝑆 ) → ( ( ( 𝑇𝑈 ) ⊊ 𝑈 ∧ ∀ 𝑟𝑆 ( ( ( 𝑇𝑈 ) ⊆ 𝑟𝑟𝑈 ) → ( 𝑟 = ( 𝑇𝑈 ) ∨ 𝑟 = 𝑈 ) ) ) → ( ( ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) ∧ ( 𝑠𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ∨ ( 𝑠𝑈 ) = 𝑈 ) ) ) )
35 19 34 sylbid ( ( 𝜑𝑠𝑆 ) → ( ( 𝑇𝑈 ) 𝐶 𝑈 → ( ( ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) ∧ ( 𝑠𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ∨ ( 𝑠𝑈 ) = 𝑈 ) ) ) )
36 35 3adant3 ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( 𝑇𝑈 ) 𝐶 𝑈 → ( ( ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) ∧ ( 𝑠𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ∨ ( 𝑠𝑈 ) = 𝑈 ) ) ) )
37 17 36 mpd ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( ( 𝑇𝑈 ) ⊆ ( 𝑠𝑈 ) ∧ ( 𝑠𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ∨ ( 𝑠𝑈 ) = 𝑈 ) ) )
38 16 37 mpd ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ∨ ( 𝑠𝑈 ) = 𝑈 ) )
39 oveq1 ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) → ( ( 𝑠𝑈 ) 𝑇 ) = ( ( 𝑇𝑈 ) 𝑇 ) )
40 4 3ad2ant1 ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → 𝑊 ∈ LMod )
41 5 3ad2ant1 ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → 𝑇𝑆 )
42 6 3ad2ant1 ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → 𝑈𝑆 )
43 simp2 ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → 𝑠𝑆 )
44 simp3r ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → 𝑠 ⊆ ( 𝑇 𝑈 ) )
45 1 2 3 40 41 42 43 13 44 lcvexchlem3 ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( 𝑠𝑈 ) 𝑇 ) = 𝑠 )
46 1 lsssssubg ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
47 4 46 syl ( 𝜑𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
48 47 9 sseldd ( 𝜑 → ( 𝑇𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) )
49 47 5 sseldd ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
50 inss1 ( 𝑇𝑈 ) ⊆ 𝑇
51 50 a1i ( 𝜑 → ( 𝑇𝑈 ) ⊆ 𝑇 )
52 2 lsmss1 ( ( ( 𝑇𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑇𝑈 ) ⊆ 𝑇 ) → ( ( 𝑇𝑈 ) 𝑇 ) = 𝑇 )
53 48 49 51 52 syl3anc ( 𝜑 → ( ( 𝑇𝑈 ) 𝑇 ) = 𝑇 )
54 53 3ad2ant1 ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( 𝑇𝑈 ) 𝑇 ) = 𝑇 )
55 45 54 eqeq12d ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( ( 𝑠𝑈 ) 𝑇 ) = ( ( 𝑇𝑈 ) 𝑇 ) ↔ 𝑠 = 𝑇 ) )
56 39 55 syl5ib ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) → 𝑠 = 𝑇 ) )
57 oveq1 ( ( 𝑠𝑈 ) = 𝑈 → ( ( 𝑠𝑈 ) 𝑇 ) = ( 𝑈 𝑇 ) )
58 lmodabl ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
59 4 58 syl ( 𝜑𝑊 ∈ Abel )
60 47 6 sseldd ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
61 2 lsmcom ( ( 𝑊 ∈ Abel ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑈 𝑇 ) = ( 𝑇 𝑈 ) )
62 59 60 49 61 syl3anc ( 𝜑 → ( 𝑈 𝑇 ) = ( 𝑇 𝑈 ) )
63 62 3ad2ant1 ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( 𝑈 𝑇 ) = ( 𝑇 𝑈 ) )
64 45 63 eqeq12d ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( ( 𝑠𝑈 ) 𝑇 ) = ( 𝑈 𝑇 ) ↔ 𝑠 = ( 𝑇 𝑈 ) ) )
65 57 64 syl5ib ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( 𝑠𝑈 ) = 𝑈𝑠 = ( 𝑇 𝑈 ) ) )
66 56 65 orim12d ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( ( ( 𝑠𝑈 ) = ( 𝑇𝑈 ) ∨ ( 𝑠𝑈 ) = 𝑈 ) → ( 𝑠 = 𝑇𝑠 = ( 𝑇 𝑈 ) ) ) )
67 38 66 mpd ( ( 𝜑𝑠𝑆 ∧ ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) ) → ( 𝑠 = 𝑇𝑠 = ( 𝑇 𝑈 ) ) )
68 67 3exp ( 𝜑 → ( 𝑠𝑆 → ( ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) → ( 𝑠 = 𝑇𝑠 = ( 𝑇 𝑈 ) ) ) ) )
69 68 ralrimiv ( 𝜑 → ∀ 𝑠𝑆 ( ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) → ( 𝑠 = 𝑇𝑠 = ( 𝑇 𝑈 ) ) ) )
70 1 2 lsmcl ( ( 𝑊 ∈ LMod ∧ 𝑇𝑆𝑈𝑆 ) → ( 𝑇 𝑈 ) ∈ 𝑆 )
71 4 5 6 70 syl3anc ( 𝜑 → ( 𝑇 𝑈 ) ∈ 𝑆 )
72 1 3 4 5 71 lcvbr3 ( 𝜑 → ( 𝑇 𝐶 ( 𝑇 𝑈 ) ↔ ( 𝑇 ⊊ ( 𝑇 𝑈 ) ∧ ∀ 𝑠𝑆 ( ( 𝑇𝑠𝑠 ⊆ ( 𝑇 𝑈 ) ) → ( 𝑠 = 𝑇𝑠 = ( 𝑇 𝑈 ) ) ) ) ) )
73 12 69 72 mpbir2and ( 𝜑𝑇 𝐶 ( 𝑇 𝑈 ) )