Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lcvexchlem5 Structured version   Visualization version   GIF version

Theorem lcvexchlem5 34643
 Description: Lemma for lcvexch 34644. (Contributed by NM, 10-Jan-2015.)
Hypotheses
Ref Expression
lcvexch.s 𝑆 = (LSubSp‘𝑊)
lcvexch.p = (LSSum‘𝑊)
lcvexch.c 𝐶 = ( ⋖L𝑊)
lcvexch.w (𝜑𝑊 ∈ LMod)
lcvexch.t (𝜑𝑇𝑆)
lcvexch.u (𝜑𝑈𝑆)
lcvexch.g (𝜑 → (𝑇𝑈)𝐶𝑈)
Assertion
Ref Expression
lcvexchlem5 (𝜑𝑇𝐶(𝑇 𝑈))

Proof of Theorem lcvexchlem5
Dummy variables 𝑠 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lcvexch.s . . . 4 𝑆 = (LSubSp‘𝑊)
2 lcvexch.c . . . 4 𝐶 = ( ⋖L𝑊)
3 lcvexch.w . . . 4 (𝜑𝑊 ∈ LMod)
4 lcvexch.t . . . . 5 (𝜑𝑇𝑆)
5 lcvexch.u . . . . 5 (𝜑𝑈𝑆)
61lssincl 19013 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑇𝑆𝑈𝑆) → (𝑇𝑈) ∈ 𝑆)
73, 4, 5, 6syl3anc 1366 . . . 4 (𝜑 → (𝑇𝑈) ∈ 𝑆)
8 lcvexch.g . . . 4 (𝜑 → (𝑇𝑈)𝐶𝑈)
91, 2, 3, 7, 5, 8lcvpss 34629 . . 3 (𝜑 → (𝑇𝑈) ⊊ 𝑈)
10 lcvexch.p . . . 4 = (LSSum‘𝑊)
111, 10, 2, 3, 4, 5lcvexchlem1 34639 . . 3 (𝜑 → (𝑇 ⊊ (𝑇 𝑈) ↔ (𝑇𝑈) ⊊ 𝑈))
129, 11mpbird 247 . 2 (𝜑𝑇 ⊊ (𝑇 𝑈))
13 simp3l 1109 . . . . . . . 8 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → 𝑇𝑠)
14 ssrin 3871 . . . . . . . 8 (𝑇𝑠 → (𝑇𝑈) ⊆ (𝑠𝑈))
1513, 14syl 17 . . . . . . 7 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → (𝑇𝑈) ⊆ (𝑠𝑈))
16 inss2 3867 . . . . . . 7 (𝑠𝑈) ⊆ 𝑈
1715, 16jctir 560 . . . . . 6 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → ((𝑇𝑈) ⊆ (𝑠𝑈) ∧ (𝑠𝑈) ⊆ 𝑈))
1883ad2ant1 1102 . . . . . . 7 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → (𝑇𝑈)𝐶𝑈)
191, 2, 3, 7, 5lcvbr3 34628 . . . . . . . . . 10 (𝜑 → ((𝑇𝑈)𝐶𝑈 ↔ ((𝑇𝑈) ⊊ 𝑈 ∧ ∀𝑟𝑆 (((𝑇𝑈) ⊆ 𝑟𝑟𝑈) → (𝑟 = (𝑇𝑈) ∨ 𝑟 = 𝑈)))))
2019adantr 480 . . . . . . . . 9 ((𝜑𝑠𝑆) → ((𝑇𝑈)𝐶𝑈 ↔ ((𝑇𝑈) ⊊ 𝑈 ∧ ∀𝑟𝑆 (((𝑇𝑈) ⊆ 𝑟𝑟𝑈) → (𝑟 = (𝑇𝑈) ∨ 𝑟 = 𝑈)))))
213adantr 480 . . . . . . . . . . . 12 ((𝜑𝑠𝑆) → 𝑊 ∈ LMod)
22 simpr 476 . . . . . . . . . . . 12 ((𝜑𝑠𝑆) → 𝑠𝑆)
235adantr 480 . . . . . . . . . . . 12 ((𝜑𝑠𝑆) → 𝑈𝑆)
241lssincl 19013 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ 𝑠𝑆𝑈𝑆) → (𝑠𝑈) ∈ 𝑆)
2521, 22, 23, 24syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝑠𝑆) → (𝑠𝑈) ∈ 𝑆)
26 sseq2 3660 . . . . . . . . . . . . . 14 (𝑟 = (𝑠𝑈) → ((𝑇𝑈) ⊆ 𝑟 ↔ (𝑇𝑈) ⊆ (𝑠𝑈)))
27 sseq1 3659 . . . . . . . . . . . . . 14 (𝑟 = (𝑠𝑈) → (𝑟𝑈 ↔ (𝑠𝑈) ⊆ 𝑈))
2826, 27anbi12d 747 . . . . . . . . . . . . 13 (𝑟 = (𝑠𝑈) → (((𝑇𝑈) ⊆ 𝑟𝑟𝑈) ↔ ((𝑇𝑈) ⊆ (𝑠𝑈) ∧ (𝑠𝑈) ⊆ 𝑈)))
29 eqeq1 2655 . . . . . . . . . . . . . 14 (𝑟 = (𝑠𝑈) → (𝑟 = (𝑇𝑈) ↔ (𝑠𝑈) = (𝑇𝑈)))
30 eqeq1 2655 . . . . . . . . . . . . . 14 (𝑟 = (𝑠𝑈) → (𝑟 = 𝑈 ↔ (𝑠𝑈) = 𝑈))
3129, 30orbi12d 746 . . . . . . . . . . . . 13 (𝑟 = (𝑠𝑈) → ((𝑟 = (𝑇𝑈) ∨ 𝑟 = 𝑈) ↔ ((𝑠𝑈) = (𝑇𝑈) ∨ (𝑠𝑈) = 𝑈)))
3228, 31imbi12d 333 . . . . . . . . . . . 12 (𝑟 = (𝑠𝑈) → ((((𝑇𝑈) ⊆ 𝑟𝑟𝑈) → (𝑟 = (𝑇𝑈) ∨ 𝑟 = 𝑈)) ↔ (((𝑇𝑈) ⊆ (𝑠𝑈) ∧ (𝑠𝑈) ⊆ 𝑈) → ((𝑠𝑈) = (𝑇𝑈) ∨ (𝑠𝑈) = 𝑈))))
3332rspcv 3336 . . . . . . . . . . 11 ((𝑠𝑈) ∈ 𝑆 → (∀𝑟𝑆 (((𝑇𝑈) ⊆ 𝑟𝑟𝑈) → (𝑟 = (𝑇𝑈) ∨ 𝑟 = 𝑈)) → (((𝑇𝑈) ⊆ (𝑠𝑈) ∧ (𝑠𝑈) ⊆ 𝑈) → ((𝑠𝑈) = (𝑇𝑈) ∨ (𝑠𝑈) = 𝑈))))
3425, 33syl 17 . . . . . . . . . 10 ((𝜑𝑠𝑆) → (∀𝑟𝑆 (((𝑇𝑈) ⊆ 𝑟𝑟𝑈) → (𝑟 = (𝑇𝑈) ∨ 𝑟 = 𝑈)) → (((𝑇𝑈) ⊆ (𝑠𝑈) ∧ (𝑠𝑈) ⊆ 𝑈) → ((𝑠𝑈) = (𝑇𝑈) ∨ (𝑠𝑈) = 𝑈))))
3534adantld 482 . . . . . . . . 9 ((𝜑𝑠𝑆) → (((𝑇𝑈) ⊊ 𝑈 ∧ ∀𝑟𝑆 (((𝑇𝑈) ⊆ 𝑟𝑟𝑈) → (𝑟 = (𝑇𝑈) ∨ 𝑟 = 𝑈))) → (((𝑇𝑈) ⊆ (𝑠𝑈) ∧ (𝑠𝑈) ⊆ 𝑈) → ((𝑠𝑈) = (𝑇𝑈) ∨ (𝑠𝑈) = 𝑈))))
3620, 35sylbid 230 . . . . . . . 8 ((𝜑𝑠𝑆) → ((𝑇𝑈)𝐶𝑈 → (((𝑇𝑈) ⊆ (𝑠𝑈) ∧ (𝑠𝑈) ⊆ 𝑈) → ((𝑠𝑈) = (𝑇𝑈) ∨ (𝑠𝑈) = 𝑈))))
37363adant3 1101 . . . . . . 7 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → ((𝑇𝑈)𝐶𝑈 → (((𝑇𝑈) ⊆ (𝑠𝑈) ∧ (𝑠𝑈) ⊆ 𝑈) → ((𝑠𝑈) = (𝑇𝑈) ∨ (𝑠𝑈) = 𝑈))))
3818, 37mpd 15 . . . . . 6 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → (((𝑇𝑈) ⊆ (𝑠𝑈) ∧ (𝑠𝑈) ⊆ 𝑈) → ((𝑠𝑈) = (𝑇𝑈) ∨ (𝑠𝑈) = 𝑈)))
3917, 38mpd 15 . . . . 5 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → ((𝑠𝑈) = (𝑇𝑈) ∨ (𝑠𝑈) = 𝑈))
40 oveq1 6697 . . . . . . 7 ((𝑠𝑈) = (𝑇𝑈) → ((𝑠𝑈) 𝑇) = ((𝑇𝑈) 𝑇))
4133ad2ant1 1102 . . . . . . . . 9 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → 𝑊 ∈ LMod)
4243ad2ant1 1102 . . . . . . . . 9 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → 𝑇𝑆)
4353ad2ant1 1102 . . . . . . . . 9 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → 𝑈𝑆)
44 simp2 1082 . . . . . . . . 9 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → 𝑠𝑆)
45 simp3r 1110 . . . . . . . . 9 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → 𝑠 ⊆ (𝑇 𝑈))
461, 10, 2, 41, 42, 43, 44, 13, 45lcvexchlem3 34641 . . . . . . . 8 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → ((𝑠𝑈) 𝑇) = 𝑠)
471lsssssubg 19006 . . . . . . . . . . . 12 (𝑊 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑊))
483, 47syl 17 . . . . . . . . . . 11 (𝜑𝑆 ⊆ (SubGrp‘𝑊))
4948, 7sseldd 3637 . . . . . . . . . 10 (𝜑 → (𝑇𝑈) ∈ (SubGrp‘𝑊))
5048, 4sseldd 3637 . . . . . . . . . 10 (𝜑𝑇 ∈ (SubGrp‘𝑊))
51 inss1 3866 . . . . . . . . . . 11 (𝑇𝑈) ⊆ 𝑇
5251a1i 11 . . . . . . . . . 10 (𝜑 → (𝑇𝑈) ⊆ 𝑇)
5310lsmss1 18125 . . . . . . . . . 10 (((𝑇𝑈) ∈ (SubGrp‘𝑊) ∧ 𝑇 ∈ (SubGrp‘𝑊) ∧ (𝑇𝑈) ⊆ 𝑇) → ((𝑇𝑈) 𝑇) = 𝑇)
5449, 50, 52, 53syl3anc 1366 . . . . . . . . 9 (𝜑 → ((𝑇𝑈) 𝑇) = 𝑇)
55543ad2ant1 1102 . . . . . . . 8 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → ((𝑇𝑈) 𝑇) = 𝑇)
5646, 55eqeq12d 2666 . . . . . . 7 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → (((𝑠𝑈) 𝑇) = ((𝑇𝑈) 𝑇) ↔ 𝑠 = 𝑇))
5740, 56syl5ib 234 . . . . . 6 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → ((𝑠𝑈) = (𝑇𝑈) → 𝑠 = 𝑇))
58 oveq1 6697 . . . . . . 7 ((𝑠𝑈) = 𝑈 → ((𝑠𝑈) 𝑇) = (𝑈 𝑇))
59 lmodabl 18958 . . . . . . . . . . 11 (𝑊 ∈ LMod → 𝑊 ∈ Abel)
603, 59syl 17 . . . . . . . . . 10 (𝜑𝑊 ∈ Abel)
6148, 5sseldd 3637 . . . . . . . . . 10 (𝜑𝑈 ∈ (SubGrp‘𝑊))
6210lsmcom 18307 . . . . . . . . . 10 ((𝑊 ∈ Abel ∧ 𝑈 ∈ (SubGrp‘𝑊) ∧ 𝑇 ∈ (SubGrp‘𝑊)) → (𝑈 𝑇) = (𝑇 𝑈))
6360, 61, 50, 62syl3anc 1366 . . . . . . . . 9 (𝜑 → (𝑈 𝑇) = (𝑇 𝑈))
64633ad2ant1 1102 . . . . . . . 8 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → (𝑈 𝑇) = (𝑇 𝑈))
6546, 64eqeq12d 2666 . . . . . . 7 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → (((𝑠𝑈) 𝑇) = (𝑈 𝑇) ↔ 𝑠 = (𝑇 𝑈)))
6658, 65syl5ib 234 . . . . . 6 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → ((𝑠𝑈) = 𝑈𝑠 = (𝑇 𝑈)))
6757, 66orim12d 901 . . . . 5 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → (((𝑠𝑈) = (𝑇𝑈) ∨ (𝑠𝑈) = 𝑈) → (𝑠 = 𝑇𝑠 = (𝑇 𝑈))))
6839, 67mpd 15 . . . 4 ((𝜑𝑠𝑆 ∧ (𝑇𝑠𝑠 ⊆ (𝑇 𝑈))) → (𝑠 = 𝑇𝑠 = (𝑇 𝑈)))
69683exp 1283 . . 3 (𝜑 → (𝑠𝑆 → ((𝑇𝑠𝑠 ⊆ (𝑇 𝑈)) → (𝑠 = 𝑇𝑠 = (𝑇 𝑈)))))
7069ralrimiv 2994 . 2 (𝜑 → ∀𝑠𝑆 ((𝑇𝑠𝑠 ⊆ (𝑇 𝑈)) → (𝑠 = 𝑇𝑠 = (𝑇 𝑈))))
711, 10lsmcl 19131 . . . 4 ((𝑊 ∈ LMod ∧ 𝑇𝑆𝑈𝑆) → (𝑇 𝑈) ∈ 𝑆)
723, 4, 5, 71syl3anc 1366 . . 3 (𝜑 → (𝑇 𝑈) ∈ 𝑆)
731, 2, 3, 4, 72lcvbr3 34628 . 2 (𝜑 → (𝑇𝐶(𝑇 𝑈) ↔ (𝑇 ⊊ (𝑇 𝑈) ∧ ∀𝑠𝑆 ((𝑇𝑠𝑠 ⊆ (𝑇 𝑈)) → (𝑠 = 𝑇𝑠 = (𝑇 𝑈))))))
7412, 70, 73mpbir2and 977 1 (𝜑𝑇𝐶(𝑇 𝑈))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∀wral 2941   ∩ cin 3606   ⊆ wss 3607   ⊊ wpss 3608   class class class wbr 4685  ‘cfv 5926  (class class class)co 6690  SubGrpcsubg 17635  LSSumclsm 18095  Abelcabl 18240  LModclmod 18911  LSubSpclss 18980   ⋖L clcv 34623 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-tpos 7397  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-0g 16149  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-grp 17472  df-minusg 17473  df-sbg 17474  df-subg 17638  df-cntz 17796  df-oppg 17822  df-lsm 18097  df-cmn 18241  df-abl 18242  df-mgp 18536  df-ur 18548  df-ring 18595  df-lmod 18913  df-lss 18981  df-lcv 34624 This theorem is referenced by:  lcvexch  34644
 Copyright terms: Public domain W3C validator