Theorem lcv1 35708

Description: Covering property of a subspace plus an atom. (chcv1 29823 analog.) (Contributed by NM, 10-Jan-2015.)

Hypotheses

Ref	Expression
lcv1.s	⊢ 𝑆 = (LSubSp‘𝑊)
lcv1.p	⊢ ⊕ = (LSSum‘𝑊)
lcv1.a	⊢ 𝐴 = (LSAtoms‘𝑊)
lcv1.c	⊢ 𝐶 = ( ⋖L ‘𝑊)
lcv1.w	⊢ (𝜑 → 𝑊 ∈ LVec)
lcv1.u	⊢ (𝜑 → 𝑈 ∈ 𝑆)
lcv1.q	⊢ (𝜑 → 𝑄 ∈ 𝐴)

Assertion

Ref	Expression
lcv1	⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ 𝑈𝐶(𝑈 ⊕ 𝑄)))

Proof of Theorem lcv1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lcv1.q	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ 𝐴)
2		lcv1.w	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ LVec)
3		eqid 2795	. . . . . . 7 ⊢ (Base‘𝑊) = (Base‘𝑊)
4		eqid 2795	. . . . . . 7 ⊢ (LSpan‘𝑊) = (LSpan‘𝑊)
5		eqid 2795	. . . . . . 7 ⊢ (0g‘𝑊) = (0g‘𝑊)
6		lcv1.a	. . . . . . 7 ⊢ 𝐴 = (LSAtoms‘𝑊)
7	3, 4, 5, 6	islsat 35658	. . . . . 6 ⊢ (𝑊 ∈ LVec → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑄 = ((LSpan‘𝑊)‘{𝑥})))
8	2, 7	syl 17	. . . . 5 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑄 = ((LSpan‘𝑊)‘{𝑥})))
9	1, 8	mpbid 233	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑄 = ((LSpan‘𝑊)‘{𝑥}))
10	9	adantr 481	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) → ∃𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑄 = ((LSpan‘𝑊)‘{𝑥}))
11		lcv1.s	. . . . . 6 ⊢ 𝑆 = (LSubSp‘𝑊)
12		lcv1.p	. . . . . 6 ⊢ ⊕ = (LSSum‘𝑊)
13		lcv1.c	. . . . . 6 ⊢ 𝐶 = ( ⋖L ‘𝑊)
14	2	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) → 𝑊 ∈ LVec)
15	14	3ad2ant1 1126	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑊 ∈ LVec)
16		lcv1.u	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ 𝑆)
17	16	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) → 𝑈 ∈ 𝑆)
18	17	3ad2ant1 1126	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑈 ∈ 𝑆)
19		eldifi 4024	. . . . . . 7 ⊢ (𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) → 𝑥 ∈ (Base‘𝑊))
20	19	3ad2ant2 1127	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑥 ∈ (Base‘𝑊))
21		simp1r 1191	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → ¬ 𝑄 ⊆ 𝑈)
22		simp3 1131	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑄 = ((LSpan‘𝑊)‘{𝑥}))
23	22	sseq1d 3919	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → (𝑄 ⊆ 𝑈 ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈))
24	21, 23	mtbid 325	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → ¬ ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈)
25	3, 11, 4, 12, 13, 15, 18, 20, 24	lsmcv2 35696	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑈𝐶(𝑈 ⊕ ((LSpan‘𝑊)‘{𝑥})))
26	22	oveq2d 7032	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → (𝑈 ⊕ 𝑄) = (𝑈 ⊕ ((LSpan‘𝑊)‘{𝑥})))
27	25, 26	breqtrrd 4990	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑈𝐶(𝑈 ⊕ 𝑄))
28	27	rexlimdv3a 3249	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) → (∃𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑄 = ((LSpan‘𝑊)‘{𝑥}) → 𝑈𝐶(𝑈 ⊕ 𝑄)))
29	10, 28	mpd 15	. 2 ⊢ ((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) → 𝑈𝐶(𝑈 ⊕ 𝑄))
30	2	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → 𝑊 ∈ LVec)
31	16	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → 𝑈 ∈ 𝑆)
32		lveclmod 19568	. . . . . . 7 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
33	2, 32	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ LMod)
34	11, 6, 33, 1	lsatlssel 35664	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ 𝑆)
35	11, 12	lsmcl 19545	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆) → (𝑈 ⊕ 𝑄) ∈ 𝑆)
36	33, 16, 34, 35	syl3anc 1364	. . . . 5 ⊢ (𝜑 → (𝑈 ⊕ 𝑄) ∈ 𝑆)
37	36	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → (𝑈 ⊕ 𝑄) ∈ 𝑆)
38		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → 𝑈𝐶(𝑈 ⊕ 𝑄))
39	11, 13, 30, 31, 37, 38	lcvpss 35691	. . 3 ⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → 𝑈 ⊊ (𝑈 ⊕ 𝑄))
40	11	lsssssubg 19420	. . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑊))
41	33, 40	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝑊))
42	41, 16	sseldd 3890	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑊))
43	41, 34	sseldd 3890	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (SubGrp‘𝑊))
44	12, 42, 43	lssnle 18527	. . . 4 ⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 ⊊ (𝑈 ⊕ 𝑄)))
45	44	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → (¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 ⊊ (𝑈 ⊕ 𝑄)))
46	39, 45	mpbird 258	. 2 ⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → ¬ 𝑄 ⊆ 𝑈)
47	29, 46	impbida 797	1 ⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ 𝑈𝐶(𝑈 ⊕ 𝑄)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   = wceq 1522   ∈ wcel 2081  ∃wrex 3106   ∖ cdif 3856   ⊆ wss 3859   ⊊ wpss 3860  {csn 4472   class class class wbr 4962  ‘cfv 6225  (class class class)co 7016  Basecbs 16312  0_gc0g 16542  SubGrpcsubg 18027  LSSumclsm 18489  LModclmod 19324  LSubSpclss 19393  LSpanclspn 19433  LVecclvec 19564  LSAtomsclsa 35641   ⋖_L clcv 35685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-tpos 7743  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-nn 11487  df-2 11548  df-3 11549  df-ndx 16315  df-slot 16316  df-base 16318  df-sets 16319  df-ress 16320  df-plusg 16407  df-mulr 16408  df-0g 16544  df-mgm 17681  df-sgrp 17723  df-mnd 17734  df-submnd 17775  df-grp 17864  df-minusg 17865  df-sbg 17866  df-subg 18030  df-cntz 18188  df-lsm 18491  df-cmn 18635  df-abl 18636  df-mgp 18930  df-ur 18942  df-ring 18989  df-oppr 19063  df-dvdsr 19081  df-unit 19082  df-invr 19112  df-drng 19194  df-lmod 19326  df-lss 19394  df-lsp 19434  df-lvec 19565  df-lsatoms 35643  df-lcv 35686

This theorem is referenced by:  lcv2  35709  lsatnle  35711  lsatcvat3  35719