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 imbitrid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) → 𝑠 = 𝑇 ) )
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 imbitrid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑠 ∩ 𝑈 ) = 𝑈 → 𝑠 = ( 𝑇 ⊕ 𝑈 ) ) )
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 ⊢ ( 𝜑 → 𝑇 𝐶 ( 𝑇 ⊕ 𝑈 ) )