Metamath Proof Explorer

Theorem lcvexchlem4

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.f ⊢ ( 𝜑 → 𝑇 𝐶 ( 𝑇 ⊕ 𝑈 ) )
Assertion lcvexchlem4 ( 𝜑 → ( 𝑇 ∩ 𝑈 ) 𝐶 𝑈 )

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.f ⊢ ( 𝜑 → 𝑇 𝐶 ( 𝑇 ⊕ 𝑈 ) )
8 1 2 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 )
9 4 5 6 8 syl3anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 )
10 1 3 4 5 9 7 lcvpss ⊢ ( 𝜑 → 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) )
11 1 2 3 4 5 6 lcvexchlem1 ⊢ ( 𝜑 → ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 ) )
12 10 11 mpbid ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 )
13 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑊 ∈ LMod )
14 1 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
15 13 14 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
16 simp2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑠 ∈ 𝑆 )
17 15 16 sseldd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑠 ∈ ( SubGrp ‘ 𝑊 ) )
18 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑇 ∈ 𝑆 )
19 15 18 sseldd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
20 2 lsmub2 ⊢ ( ( 𝑠 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) )
21 17 19 20 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) )
22 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑈 ∈ 𝑆 )
23 15 22 sseldd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
24 simp3r ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑠 ⊆ 𝑈 )
25 2 lsmless1 ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑠 ⊆ 𝑈 ) → ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑈 ⊕ 𝑇 ) )
26 23 19 24 25 syl3anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑈 ⊕ 𝑇 ) )
27 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
28 4 27 syl ⊢ ( 𝜑 → 𝑊 ∈ Abel )
29 4 14 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
30 29 5 sseldd ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
31 29 6 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
32 2 lsmcom ⊢ ( ( 𝑊 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
33 28 30 31 32 syl3anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
34 33 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
35 26 34 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
36 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑇 𝐶 ( 𝑇 ⊕ 𝑈 ) )
37 1 3 4 5 9 lcvbr3 ⊢ ( 𝜑 → ( 𝑇 𝐶 ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ∧ ∀ 𝑟 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑟 ∧ 𝑟 ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑟 = 𝑇 ∨ 𝑟 = ( 𝑇 ⊕ 𝑈 ) ) ) ) ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑇 𝐶 ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ∧ ∀ 𝑟 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑟 ∧ 𝑟 ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑟 = 𝑇 ∨ 𝑟 = ( 𝑇 ⊕ 𝑈 ) ) ) ) ) )
39 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝑊 ∈ LMod )
40 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ 𝑆 )
41 5 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝑇 ∈ 𝑆 )
42 1 2 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑠 ∈ 𝑆 ∧ 𝑇 ∈ 𝑆 ) → ( 𝑠 ⊕ 𝑇 ) ∈ 𝑆 )
43 39 40 41 42 syl3anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑠 ⊕ 𝑇 ) ∈ 𝑆 )
44 sseq2 ⊢ ( 𝑟 = ( 𝑠 ⊕ 𝑇 ) → ( 𝑇 ⊆ 𝑟 ↔ 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) ) )
45 sseq1 ⊢ ( 𝑟 = ( 𝑠 ⊕ 𝑇 ) → ( 𝑟 ⊆ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) )
46 44 45 anbi12d ⊢ ( 𝑟 = ( 𝑠 ⊕ 𝑇 ) → ( ( 𝑇 ⊆ 𝑟 ∧ 𝑟 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ↔ ( 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) ∧ ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) )
47 eqeq1 ⊢ ( 𝑟 = ( 𝑠 ⊕ 𝑇 ) → ( 𝑟 = 𝑇 ↔ ( 𝑠 ⊕ 𝑇 ) = 𝑇 ) )
48 eqeq1 ⊢ ( 𝑟 = ( 𝑠 ⊕ 𝑇 ) → ( 𝑟 = ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) )
49 47 48 orbi12d ⊢ ( 𝑟 = ( 𝑠 ⊕ 𝑇 ) → ( ( 𝑟 = 𝑇 ∨ 𝑟 = ( 𝑇 ⊕ 𝑈 ) ) ↔ ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 ∨ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) ) )
50 46 49 imbi12d ⊢ ( 𝑟 = ( 𝑠 ⊕ 𝑇 ) → ( ( ( 𝑇 ⊆ 𝑟 ∧ 𝑟 ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑟 = 𝑇 ∨ 𝑟 = ( 𝑇 ⊕ 𝑈 ) ) ) ↔ ( ( 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) ∧ ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 ∨ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) ) ) )
51 50 rspcv ⊢ ( ( 𝑠 ⊕ 𝑇 ) ∈ 𝑆 → ( ∀ 𝑟 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑟 ∧ 𝑟 ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑟 = 𝑇 ∨ 𝑟 = ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) ∧ ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 ∨ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) ) ) )
52 43 51 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( ∀ 𝑟 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑟 ∧ 𝑟 ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑟 = 𝑇 ∨ 𝑟 = ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) ∧ ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 ∨ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) ) ) )
53 52 adantld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ∧ ∀ 𝑟 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑟 ∧ 𝑟 ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑟 = 𝑇 ∨ 𝑟 = ( 𝑇 ⊕ 𝑈 ) ) ) ) → ( ( 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) ∧ ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 ∨ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) ) ) )
54 38 53 sylbid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑇 𝐶 ( 𝑇 ⊕ 𝑈 ) → ( ( 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) ∧ ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 ∨ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) ) ) )
55 54 3adant3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( 𝑇 𝐶 ( 𝑇 ⊕ 𝑈 ) → ( ( 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) ∧ ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 ∨ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) ) ) )
56 36 55 mpd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( ( 𝑇 ⊆ ( 𝑠 ⊕ 𝑇 ) ∧ ( 𝑠 ⊕ 𝑇 ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 ∨ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) ) )
57 21 35 56 mp2and ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 ∨ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) )
58 ineq1 ⊢ ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 → ( ( 𝑠 ⊕ 𝑇 ) ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) )
59 simp3l ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 )
60 1 2 3 13 18 22 16 59 24 lcvexchlem2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) ∩ 𝑈 ) = 𝑠 )
61 60 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( ( ( 𝑠 ⊕ 𝑇 ) ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ↔ 𝑠 = ( 𝑇 ∩ 𝑈 ) ) )
62 58 61 imbitrid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 → 𝑠 = ( 𝑇 ∩ 𝑈 ) ) )
63 ineq1 ⊢ ( ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) → ( ( 𝑠 ⊕ 𝑇 ) ∩ 𝑈 ) = ( ( 𝑇 ⊕ 𝑈 ) ∩ 𝑈 ) )
64 2 lsmub2 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) )
65 19 23 64 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) )
66 sseqin2 ⊢ ( 𝑈 ⊆ ( 𝑇 ⊕ 𝑈 ) ↔ ( ( 𝑇 ⊕ 𝑈 ) ∩ 𝑈 ) = 𝑈 )
67 65 66 sylib ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( ( 𝑇 ⊕ 𝑈 ) ∩ 𝑈 ) = 𝑈 )
68 60 67 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( ( ( 𝑠 ⊕ 𝑇 ) ∩ 𝑈 ) = ( ( 𝑇 ⊕ 𝑈 ) ∩ 𝑈 ) ↔ 𝑠 = 𝑈 ) )
69 63 68 imbitrid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) → 𝑠 = 𝑈 ) )
70 62 69 orim12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( ( ( 𝑠 ⊕ 𝑇 ) = 𝑇 ∨ ( 𝑠 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑠 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑠 = 𝑈 ) ) )
71 57 70 mpd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ) → ( 𝑠 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑠 = 𝑈 ) )
72 71 3exp ⊢ ( 𝜑 → ( 𝑠 ∈ 𝑆 → ( ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → ( 𝑠 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑠 = 𝑈 ) ) ) )
73 72 ralrimiv ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑆 ( ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → ( 𝑠 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑠 = 𝑈 ) ) )
74 1 lssincl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ∩ 𝑈 ) ∈ 𝑆 )
75 4 5 6 74 syl3anc ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ∈ 𝑆 )
76 1 3 4 75 6 lcvbr3 ⊢ ( 𝜑 → ( ( 𝑇 ∩ 𝑈 ) 𝐶 𝑈 ↔ ( ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 ∧ ∀ 𝑠 ∈ 𝑆 ( ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → ( 𝑠 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑠 = 𝑈 ) ) ) ) )
77 12 73 76 mpbir2and ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) 𝐶 𝑈 )