lcfrlem32 - Mathbox for Norm Megill

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

Theorem lcfrlem32 37384

Description: Lemma for lcfr 37395. (Contributed by NM, 10-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	⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
lcfrlem22.b	⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))
lcfrlem24.t	⊢ · = ( ·_𝑠 ‘𝑈)
lcfrlem24.s	⊢ 𝑆 = (Scalar‘𝑈)
lcfrlem24.q	⊢ 𝑄 = (0_g‘𝑆)
lcfrlem24.r	⊢ 𝑅 = (Base‘𝑆)
lcfrlem24.j	⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))
lcfrlem24.ib	⊢ (𝜑 → 𝐼 ∈ 𝐵)
lcfrlem24.l	⊢ 𝐿 = (LKer‘𝑈)
lcfrlem25.d	⊢ 𝐷 = (LDual‘𝑈)
lcfrlem28.jn	⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)
lcfrlem29.i	⊢ 𝐹 = (inv_r‘𝑆)
lcfrlem30.m	⊢ − = (-_g‘𝐷)
lcfrlem30.c	⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·_𝑠 ‘𝐷)(𝐽‘𝑌)))
lcfrlem31.xi	⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) ≠ 𝑄)

**Assertion**
Ref	Expression
lcfrlem32	⊢ (𝜑 → 𝐶 ≠ (0_g‘𝐷))

Distinct variable groups: 𝑣,𝑘,𝑤,𝑥, ⊥ + ,𝑘,𝑣,𝑤,𝑥 𝑅,𝑘,𝑣,𝑥 𝑆,𝑘 · ,𝑘,𝑣,𝑤,𝑥 𝑣,𝑉,𝑥 𝑘,𝑋,𝑣,𝑤,𝑥 𝑘,𝑌,𝑣,𝑤,𝑥 𝑥, 0 Allowed substitution hints: 𝜑(𝑥,𝑤,𝑣,𝑘) 𝐴(𝑥,𝑤,𝑣,𝑘) 𝐵(𝑥,𝑤,𝑣,𝑘) 𝐶(𝑥,𝑤,𝑣,𝑘) 𝐷(𝑥,𝑤,𝑣,𝑘) 𝑄(𝑥,𝑤,𝑣,𝑘) 𝑅(𝑤) 𝑆(𝑥,𝑤,𝑣) 𝑈(𝑥,𝑤,𝑣,𝑘) 𝐹(𝑥,𝑤,𝑣,𝑘) 𝐻(𝑥,𝑤,𝑣,𝑘) 𝐼(𝑥,𝑤,𝑣,𝑘) 𝐽(𝑥,𝑤,𝑣,𝑘) 𝐾(𝑥,𝑤,𝑣,𝑘) 𝐿(𝑥,𝑤,𝑣,𝑘) − (𝑥,𝑤,𝑣,𝑘) 𝑁(𝑥,𝑤,𝑣,𝑘) 𝑉(𝑤,𝑘) 𝑊(𝑥,𝑤,𝑣,𝑘) 0 (𝑤,𝑣,𝑘)

**Proof of Theorem lcfrlem32**
Step	Hyp	Ref	Expression
1		lcfrlem17.ne	. 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
2		lcfrlem17.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3		lcfrlem17.o	. . . . 5 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
4		lcfrlem17.u	. . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
5		lcfrlem17.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
6		lcfrlem17.p	. . . . 5 ⊢ + = (+_g‘𝑈)
7		lcfrlem17.z	. . . . 5 ⊢ 0 = (0_g‘𝑈)
8		lcfrlem17.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
9		lcfrlem17.a	. . . . 5 ⊢ 𝐴 = (LSAtoms‘𝑈)
10		lcfrlem17.k	. . . . . 6 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
11	10	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 = (0_g‘𝐷)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
12		lcfrlem17.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
13	12	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 = (0_g‘𝐷)) → 𝑋 ∈ (𝑉 ∖ { 0 }))
14		lcfrlem17.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
15	14	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 = (0_g‘𝐷)) → 𝑌 ∈ (𝑉 ∖ { 0 }))
16	1	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 = (0_g‘𝐷)) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
17		lcfrlem22.b	. . . . 5 ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))
18		lcfrlem24.t	. . . . 5 ⊢ · = ( ·_𝑠 ‘𝑈)
19		lcfrlem24.s	. . . . 5 ⊢ 𝑆 = (Scalar‘𝑈)
20		lcfrlem24.q	. . . . 5 ⊢ 𝑄 = (0_g‘𝑆)
21		lcfrlem24.r	. . . . 5 ⊢ 𝑅 = (Base‘𝑆)
22		lcfrlem24.j	. . . . 5 ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))
23		lcfrlem24.ib	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝐵)
24	23	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 = (0_g‘𝐷)) → 𝐼 ∈ 𝐵)
25		lcfrlem24.l	. . . . 5 ⊢ 𝐿 = (LKer‘𝑈)
26		lcfrlem25.d	. . . . 5 ⊢ 𝐷 = (LDual‘𝑈)
27		lcfrlem28.jn	. . . . . 6 ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)
28	27	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 = (0_g‘𝐷)) → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)
29		lcfrlem29.i	. . . . 5 ⊢ 𝐹 = (inv_r‘𝑆)
30		lcfrlem30.m	. . . . 5 ⊢ − = (-_g‘𝐷)
31		lcfrlem30.c	. . . . 5 ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·_𝑠 ‘𝐷)(𝐽‘𝑌)))
32		lcfrlem31.xi	. . . . . 6 ⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) ≠ 𝑄)
33	32	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 = (0_g‘𝐷)) → ((𝐽‘𝑋)‘𝐼) ≠ 𝑄)
34		simpr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 = (0_g‘𝐷)) → 𝐶 = (0_g‘𝐷))
35	2, 3, 4, 5, 6, 7, 8, 9, 11, 13, 15, 16, 17, 18, 19, 20, 21, 22, 24, 25, 26, 28, 29, 30, 31, 33, 34	lcfrlem31 37383	. . . 4 ⊢ ((𝜑 ∧ 𝐶 = (0_g‘𝐷)) → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))
36	35	ex 449	. . 3 ⊢ (𝜑 → (𝐶 = (0_g‘𝐷) → (𝑁‘{𝑋}) = (𝑁‘{𝑌})))
37	36	necon3d 2954	. 2 ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) → 𝐶 ≠ (0_g‘𝐷)))
38	1, 37	mpd 15	1 ⊢ (𝜑 → 𝐶 ≠ (0_g‘𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 ∈ wcel 2140 ≠ wne 2933 ∃wrex 3052 ∖ cdif 3713 ∩ cin 3715 {csn 4322 {cpr 4324 ↦ cmpt 4882 ‘cfv 6050 ℩crio 6775 (class class class)co 6815 Basecbs 16080 +_gcplusg 16164 ._rcmulr 16165 Scalarcsca 16167 ·_𝑠 cvsca 16168 0_gc0g 16323 -_gcsg 17646 inv_rcinvr 18892 LSpanclspn 19194 LSAtomsclsa 34783 LKerclk 34894 LDualcld 34932 HLchlt 35159 LHypclh 35792 DVecHcdvh 36888 ocHcoch 37157

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1989 ax-6 2055 ax-7 2091 ax-8 2142 ax-9 2149 ax-10 2169 ax-11 2184 ax-12 2197 ax-13 2392 ax-ext 2741 ax-rep 4924 ax-sep 4934 ax-nul 4942 ax-pow 4993 ax-pr 5056 ax-un 7116 ax-cnex 10205 ax-resscn 10206 ax-1cn 10207 ax-icn 10208 ax-addcl 10209 ax-addrcl 10210 ax-mulcl 10211 ax-mulrcl 10212 ax-mulcom 10213 ax-addass 10214 ax-mulass 10215 ax-distr 10216 ax-i2m1 10217 ax-1ne0 10218 ax-1rid 10219 ax-rnegex 10220 ax-rrecex 10221 ax-cnre 10222 ax-pre-lttri 10223 ax-pre-lttrn 10224 ax-pre-ltadd 10225 ax-pre-mulgt0 10226 ax-riotaBAD 34761

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-fal 1638 df-ex 1854 df-nf 1859 df-sb 2048 df-eu 2612 df-mo 2613 df-clab 2748 df-cleq 2754 df-clel 2757 df-nfc 2892 df-ne 2934 df-nel 3037 df-ral 3056 df-rex 3057 df-reu 3058 df-rmo 3059 df-rab 3060 df-v 3343 df-sbc 3578 df-csb 3676 df-dif 3719 df-un 3721 df-in 3723 df-ss 3730 df-pss 3732 df-nul 4060 df-if 4232 df-pw 4305 df-sn 4323 df-pr 4325 df-tp 4327 df-op 4329 df-uni 4590 df-int 4629 df-iun 4675 df-iin 4676 df-br 4806 df-opab 4866 df-mpt 4883 df-tr 4906 df-id 5175 df-eprel 5180 df-po 5188 df-so 5189 df-fr 5226 df-we 5228 df-xp 5273 df-rel 5274 df-cnv 5275 df-co 5276 df-dm 5277 df-rn 5278 df-res 5279 df-ima 5280 df-pred 5842 df-ord 5888 df-on 5889 df-lim 5890 df-suc 5891 df-iota 6013 df-fun 6052 df-fn 6053 df-f 6054 df-f1 6055 df-fo 6056 df-f1o 6057 df-fv 6058 df-riota 6776 df-ov 6818 df-oprab 6819 df-mpt2 6820 df-of 7064 df-om 7233 df-1st 7335 df-2nd 7336 df-tpos 7523 df-undef 7570 df-wrecs 7578 df-recs 7639 df-rdg 7677 df-1o 7731 df-oadd 7735 df-er 7914 df-map 8028 df-en 8125 df-dom 8126 df-sdom 8127 df-fin 8128 df-pnf 10289 df-mnf 10290 df-xr 10291 df-ltxr 10292 df-le 10293 df-sub 10481 df-neg 10482 df-nn 11234 df-2 11292 df-3 11293 df-4 11294 df-5 11295 df-6 11296 df-n0 11506 df-z 11591 df-uz 11901 df-fz 12541 df-struct 16082 df-ndx 16083 df-slot 16084 df-base 16086 df-sets 16087 df-ress 16088 df-plusg 16177 df-mulr 16178 df-sca 16180 df-vsca 16181 df-0g 16325 df-mre 16469 df-mrc 16470 df-acs 16472 df-preset 17150 df-poset 17168 df-plt 17180 df-lub 17196 df-glb 17197 df-join 17198 df-meet 17199 df-p0 17261 df-p1 17262 df-lat 17268 df-clat 17330 df-mgm 17464 df-sgrp 17506 df-mnd 17517 df-submnd 17558 df-grp 17647 df-minusg 17648 df-sbg 17649 df-subg 17813 df-cntz 17971 df-oppg 17997 df-lsm 18272 df-cmn 18416 df-abl 18417 df-mgp 18711 df-ur 18723 df-ring 18770 df-oppr 18844 df-dvdsr 18862 df-unit 18863 df-invr 18893 df-dvr 18904 df-drng 18972 df-lmod 19088 df-lss 19156 df-lsp 19195 df-lvec 19326 df-lsatoms 34785 df-lshyp 34786 df-lcv 34828 df-lfl 34867 df-lkr 34895 df-ldual 34933 df-oposet 34985 df-ol 34987 df-oml 34988 df-covers 35075 df-ats 35076 df-atl 35107 df-cvlat 35131 df-hlat 35160 df-llines 35306 df-lplanes 35307 df-lvols 35308 df-lines 35309 df-psubsp 35311 df-pmap 35312 df-padd 35604 df-lhyp 35796 df-laut 35797 df-ldil 35912 df-ltrn 35913 df-trl 35968 df-tgrp 36552 df-tendo 36564 df-edring 36566 df-dveca 36812 df-disoa 36839 df-dvech 36889 df-dib 36949 df-dic 36983 df-dih 37039 df-doch 37158 df-djh 37205

This theorem is referenced by: lcfrlem34 37386

W3C validator