lcfrlem21 - Mathbox for Norm Megill

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

Theorem lcfrlem21 35668

Description: Lemma for lcfr 35690. (Contributed by NM, 11-Mar-2015.)

**Hypotheses**
Ref	Expression
lcfrlem17.h	⊢ 𝐻 = (LHyp‘𝐾)
lcfrlem17.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
lcfrlem17.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
lcfrlem17.v	⊢ 𝑉 = (Base‘𝑈)
lcfrlem17.p	⊢ + = (+_g‘𝑈)
lcfrlem17.z	⊢ 0 = (0_g‘𝑈)
lcfrlem17.n	⊢ 𝑁 = (LSpan‘𝑈)
lcfrlem17.a	⊢ 𝐴 = (LSAtoms‘𝑈)
lcfrlem17.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
lcfrlem17.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
lcfrlem17.y	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
lcfrlem17.ne	⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))

**Assertion**
Ref	Expression
lcfrlem21	⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴)

**Proof of Theorem lcfrlem21**
Step	Hyp	Ref	Expression
1		lcfrlem17.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		lcfrlem17.o	. . 3 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
3		lcfrlem17.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
4		lcfrlem17.v	. . 3 ⊢ 𝑉 = (Base‘𝑈)
5		lcfrlem17.p	. . 3 ⊢ + = (+_g‘𝑈)
6		lcfrlem17.z	. . 3 ⊢ 0 = (0_g‘𝑈)
7		lcfrlem17.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑈)
8		lcfrlem17.a	. . 3 ⊢ 𝐴 = (LSAtoms‘𝑈)
9		lcfrlem17.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
10	9	adantr 479	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
11		lcfrlem17.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
12	11	adantr 479	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) → 𝑋 ∈ (𝑉 ∖ { 0 }))
13		lcfrlem17.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
14	13	adantr 479	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) → 𝑌 ∈ (𝑉 ∖ { 0 }))
15		lcfrlem17.ne	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
16	15	adantr 479	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
17		simpr 475	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) → ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}))
18	1, 2, 3, 4, 5, 6, 7, 8, 10, 12, 14, 16, 17	lcfrlem20 35667	. 2 ⊢ ((𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴)
19	1, 3, 9	dvhlmod 35215	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ LMod)
20	11	eldifad 3546	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
21	13	eldifad 3546	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
22	4, 5	lmodcom 18673	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
23	19, 20, 21, 22	syl3anc 1317	. . . . . . . 8 ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))
24	23	sneqd 4131	. . . . . . 7 ⊢ (𝜑 → {(𝑋 + 𝑌)} = {(𝑌 + 𝑋)})
25	24	fveq2d 6087	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = ( ⊥ ‘{(𝑌 + 𝑋)}))
26	25	eleq2d 2667	. . . . 5 ⊢ (𝜑 → (𝑌 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}) ↔ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)})))
27	26	biimprd 236	. . . 4 ⊢ (𝜑 → (𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)}) → 𝑌 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})))
28	27	con3dimp 455	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) → ¬ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)}))
29		prcom 4205	. . . . . . . 8 ⊢ {𝑋, 𝑌} = {𝑌, 𝑋}
30	29	fveq2i 6086	. . . . . . 7 ⊢ (𝑁‘{𝑋, 𝑌}) = (𝑁‘{𝑌, 𝑋})
31	30	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = (𝑁‘{𝑌, 𝑋}))
32	31, 25	ineq12d 3771	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) = ((𝑁‘{𝑌, 𝑋}) ∩ ( ⊥ ‘{(𝑌 + 𝑋)})))
33	32	adantr 479	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)})) → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) = ((𝑁‘{𝑌, 𝑋}) ∩ ( ⊥ ‘{(𝑌 + 𝑋)})))
34	9	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)})) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
35	13	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)})) → 𝑌 ∈ (𝑉 ∖ { 0 }))
36	11	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)})) → 𝑋 ∈ (𝑉 ∖ { 0 }))
37	15	necomd 2831	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑋}))
38	37	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)})) → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑋}))
39		simpr 475	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)})) → ¬ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)}))
40	1, 2, 3, 4, 5, 6, 7, 8, 34, 35, 36, 38, 39	lcfrlem20 35667	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)})) → ((𝑁‘{𝑌, 𝑋}) ∩ ( ⊥ ‘{(𝑌 + 𝑋)})) ∈ 𝐴)
41	33, 40	eqeltrd 2682	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑌 + 𝑋)})) → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴)
42	28, 41	syldan 485	. 2 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})) → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴)
43	1, 2, 3, 4, 5, 6, 7, 8, 9, 11, 13, 15	lcfrlem19 35666	. 2 ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{(𝑋 + 𝑌)}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{(𝑋 + 𝑌)})))
44	18, 42, 43	mpjaodan 822	1 ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 382 = wceq 1474 ∈ wcel 1975 ≠ wne 2774 ∖ cdif 3531 ∩ cin 3533 {csn 4119 {cpr 4121 ‘cfv 5785 (class class class)co 6522 Basecbs 15636 +_gcplusg 15709 0_gc0g 15864 LModclmod 18627 LSpanclspn 18733 LSAtomsclsa 33077 HLchlt 33453 LHypclh 34086 DVecHcdvh 35183 ocHcoch 35452

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1711 ax-4 1726 ax-5 1825 ax-6 1873 ax-7 1920 ax-8 1977 ax-9 1984 ax-10 2004 ax-11 2019 ax-12 2031 ax-13 2227 ax-ext 2584 ax-rep 4688 ax-sep 4698 ax-nul 4707 ax-pow 4759 ax-pr 4823 ax-un 6819 ax-cnex 9843 ax-resscn 9844 ax-1cn 9845 ax-icn 9846 ax-addcl 9847 ax-addrcl 9848 ax-mulcl 9849 ax-mulrcl 9850 ax-mulcom 9851 ax-addass 9852 ax-mulass 9853 ax-distr 9854 ax-i2m1 9855 ax-1ne0 9856 ax-1rid 9857 ax-rnegex 9858 ax-rrecex 9859 ax-cnre 9860 ax-pre-lttri 9861 ax-pre-lttrn 9862 ax-pre-ltadd 9863 ax-pre-mulgt0 9864 ax-riotaBAD 33055

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-fal 1480 df-ex 1695 df-nf 1700 df-sb 1866 df-eu 2456 df-mo 2457 df-clab 2591 df-cleq 2597 df-clel 2600 df-nfc 2734 df-ne 2776 df-nel 2777 df-ral 2895 df-rex 2896 df-reu 2897 df-rmo 2898 df-rab 2899 df-v 3169 df-sbc 3397 df-csb 3494 df-dif 3537 df-un 3539 df-in 3541 df-ss 3548 df-pss 3550 df-nul 3869 df-if 4031 df-pw 4104 df-sn 4120 df-pr 4122 df-tp 4124 df-op 4126 df-uni 4362 df-int 4400 df-iun 4446 df-iin 4447 df-br 4573 df-opab 4633 df-mpt 4634 df-tr 4670 df-eprel 4934 df-id 4938 df-po 4944 df-so 4945 df-fr 4982 df-we 4984 df-xp 5029 df-rel 5030 df-cnv 5031 df-co 5032 df-dm 5033 df-rn 5034 df-res 5035 df-ima 5036 df-pred 5578 df-ord 5624 df-on 5625 df-lim 5626 df-suc 5627 df-iota 5749 df-fun 5787 df-fn 5788 df-f 5789 df-f1 5790 df-fo 5791 df-f1o 5792 df-fv 5793 df-riota 6484 df-ov 6525 df-oprab 6526 df-mpt2 6527 df-om 6930 df-1st 7031 df-2nd 7032 df-tpos 7211 df-undef 7258 df-wrecs 7266 df-recs 7327 df-rdg 7365 df-1o 7419 df-oadd 7423 df-er 7601 df-map 7718 df-en 7814 df-dom 7815 df-sdom 7816 df-fin 7817 df-pnf 9927 df-mnf 9928 df-xr 9929 df-ltxr 9930 df-le 9931 df-sub 10114 df-neg 10115 df-nn 10863 df-2 10921 df-3 10922 df-4 10923 df-5 10924 df-6 10925 df-n0 11135 df-z 11206 df-uz 11515 df-fz 12148 df-struct 15638 df-ndx 15639 df-slot 15640 df-base 15641 df-sets 15642 df-ress 15643 df-plusg 15722 df-mulr 15723 df-sca 15725 df-vsca 15726 df-0g 15866 df-mre 16010 df-mrc 16011 df-acs 16013 df-preset 16692 df-poset 16710 df-plt 16722 df-lub 16738 df-glb 16739 df-join 16740 df-meet 16741 df-p0 16803 df-p1 16804 df-lat 16810 df-clat 16872 df-mgm 17006 df-sgrp 17048 df-mnd 17059 df-submnd 17100 df-grp 17189 df-minusg 17190 df-sbg 17191 df-subg 17355 df-cntz 17514 df-oppg 17540 df-lsm 17815 df-cmn 17959 df-abl 17960 df-mgp 18254 df-ur 18266 df-ring 18313 df-oppr 18387 df-dvdsr 18405 df-unit 18406 df-invr 18436 df-dvr 18447 df-drng 18513 df-lmod 18629 df-lss 18695 df-lsp 18734 df-lvec 18865 df-lsatoms 33079 df-lshyp 33080 df-lcv 33122 df-oposet 33279 df-ol 33281 df-oml 33282 df-covers 33369 df-ats 33370 df-atl 33401 df-cvlat 33425 df-hlat 33454 df-llines 33600 df-lplanes 33601 df-lvols 33602 df-lines 33603 df-psubsp 33605 df-pmap 33606 df-padd 33898 df-lhyp 34090 df-laut 34091 df-ldil 34206 df-ltrn 34207 df-trl 34262 df-tgrp 34847 df-tendo 34859 df-edring 34861 df-dveca 35107 df-disoa 35134 df-dvech 35184 df-dib 35244 df-dic 35278 df-dih 35334 df-doch 35453 df-djh 35500

This theorem is referenced by: lcfrlem22 35669 lcfrlem40 35687

W3C validator