lcfrlem33 - Mathbox for Norm Megill

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

Theorem lcfrlem33 41613

Description: Lemma for lcfr 41623. (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‘𝑆)((𝐽‘𝑋)‘𝐼))( ·_𝑠 ‘𝐷)(𝐽‘𝑌)))
lcfrlem33.xi	⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) = 𝑄)

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

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

Proof of Theorem lcfrlem33 Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lcfrlem30.c	. . 3 ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·_𝑠 ‘𝐷)(𝐽‘𝑌)))
2		lcfrlem33.xi	. . . . . . . . 9 ⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) = 𝑄)
3	2	oveq2d 7362	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼)) = ((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)𝑄))
4		lcfrlem17.h	. . . . . . . . . . 11 ⊢ 𝐻 = (LHyp‘𝐾)
5		lcfrlem17.u	. . . . . . . . . . 11 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
6		lcfrlem17.k	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
7	4, 5, 6	dvhlmod 41148	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ LMod)
8		lcfrlem24.s	. . . . . . . . . . 11 ⊢ 𝑆 = (Scalar‘𝑈)
9	8	lmodring 20799	. . . . . . . . . 10 ⊢ (𝑈 ∈ LMod → 𝑆 ∈ Ring)
10	7, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ Ring)
11	4, 5, 6	dvhlvec 41147	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ LVec)
12	8	lvecdrng 21037	. . . . . . . . . . 11 ⊢ (𝑈 ∈ LVec → 𝑆 ∈ DivRing)
13	11, 12	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ DivRing)
14		lcfrlem17.o	. . . . . . . . . . . 12 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
15		lcfrlem17.v	. . . . . . . . . . . 12 ⊢ 𝑉 = (Base‘𝑈)
16		lcfrlem17.p	. . . . . . . . . . . 12 ⊢ + = (+_g‘𝑈)
17		lcfrlem24.t	. . . . . . . . . . . 12 ⊢ · = ( ·_𝑠 ‘𝑈)
18		lcfrlem24.r	. . . . . . . . . . . 12 ⊢ 𝑅 = (Base‘𝑆)
19		lcfrlem17.z	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘𝑈)
20		eqid 2731	. . . . . . . . . . . 12 ⊢ (LFnl‘𝑈) = (LFnl‘𝑈)
21		lcfrlem24.l	. . . . . . . . . . . 12 ⊢ 𝐿 = (LKer‘𝑈)
22		lcfrlem25.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (LDual‘𝑈)
23		eqid 2731	. . . . . . . . . . . 12 ⊢ (0_g‘𝐷) = (0_g‘𝐷)
24		eqid 2731	. . . . . . . . . . . 12 ⊢ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}
25		lcfrlem24.j	. . . . . . . . . . . 12 ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))
26		lcfrlem17.y	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
27	4, 14, 5, 15, 16, 17, 8, 18, 19, 20, 21, 22, 23, 24, 25, 6, 26	lcfrlem10 41590	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽‘𝑌) ∈ (LFnl‘𝑈))
28		lcfrlem17.a	. . . . . . . . . . . . 13 ⊢ 𝐴 = (LSAtoms‘𝑈)
29		lcfrlem17.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (LSpan‘𝑈)
30		lcfrlem17.x	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
31		lcfrlem17.ne	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
32		lcfrlem22.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))
33	4, 14, 5, 15, 16, 19, 29, 28, 6, 30, 26, 31, 32	lcfrlem22 41602	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
34	15, 28, 7, 33	lsatssv 39036	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ⊆ 𝑉)
35		lcfrlem24.ib	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ 𝐵)
36	34, 35	sseldd 3935	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
37	8, 18, 15, 20	lflcl 39102	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ LMod ∧ (𝐽‘𝑌) ∈ (LFnl‘𝑈) ∧ 𝐼 ∈ 𝑉) → ((𝐽‘𝑌)‘𝐼) ∈ 𝑅)
38	7, 27, 36, 37	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ∈ 𝑅)
39		lcfrlem28.jn	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)
40		lcfrlem24.q	. . . . . . . . . . 11 ⊢ 𝑄 = (0_g‘𝑆)
41		lcfrlem29.i	. . . . . . . . . . 11 ⊢ 𝐹 = (inv_r‘𝑆)
42	18, 40, 41	drnginvrcl 20666	. . . . . . . . . 10 ⊢ ((𝑆 ∈ DivRing ∧ ((𝐽‘𝑌)‘𝐼) ∈ 𝑅 ∧ ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) → (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅)
43	13, 38, 39, 42	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅)
44		eqid 2731	. . . . . . . . . 10 ⊢ (._r‘𝑆) = (._r‘𝑆)
45	18, 44, 40	ringrz 20210	. . . . . . . . 9 ⊢ ((𝑆 ∈ Ring ∧ (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅) → ((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)𝑄) = 𝑄)
46	10, 43, 45	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)𝑄) = 𝑄)
47	3, 46	eqtrd 2766	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼)) = 𝑄)
48	47	oveq1d 7361	. . . . . 6 ⊢ (𝜑 → (((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·_𝑠 ‘𝐷)(𝐽‘𝑌)) = (𝑄( ·_𝑠 ‘𝐷)(𝐽‘𝑌)))
49		eqid 2731	. . . . . . 7 ⊢ ( ·_𝑠 ‘𝐷) = ( ·_𝑠 ‘𝐷)
50	20, 8, 40, 22, 49, 23, 7, 27	ldual0vs 39198	. . . . . 6 ⊢ (𝜑 → (𝑄( ·_𝑠 ‘𝐷)(𝐽‘𝑌)) = (0_g‘𝐷))
51	48, 50	eqtrd 2766	. . . . 5 ⊢ (𝜑 → (((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·_𝑠 ‘𝐷)(𝐽‘𝑌)) = (0_g‘𝐷))
52	51	oveq2d 7362	. . . 4 ⊢ (𝜑 → ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·_𝑠 ‘𝐷)(𝐽‘𝑌))) = ((𝐽‘𝑋) − (0_g‘𝐷)))
53	22, 7	ldualgrp 39184	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ Grp)
54		eqid 2731	. . . . . 6 ⊢ (Base‘𝐷) = (Base‘𝐷)
55	4, 14, 5, 15, 16, 17, 8, 18, 19, 20, 21, 22, 23, 24, 25, 6, 30	lcfrlem10 41590	. . . . . 6 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (LFnl‘𝑈))
56	20, 22, 54, 7, 55	ldualelvbase 39165	. . . . 5 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (Base‘𝐷))
57		lcfrlem30.m	. . . . . 6 ⊢ − = (-_g‘𝐷)
58	54, 23, 57	grpsubid1 18935	. . . . 5 ⊢ ((𝐷 ∈ Grp ∧ (𝐽‘𝑋) ∈ (Base‘𝐷)) → ((𝐽‘𝑋) − (0_g‘𝐷)) = (𝐽‘𝑋))
59	53, 56, 58	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝐽‘𝑋) − (0_g‘𝐷)) = (𝐽‘𝑋))
60	52, 59	eqtrd 2766	. . 3 ⊢ (𝜑 → ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·_𝑠 ‘𝐷)(𝐽‘𝑌))) = (𝐽‘𝑋))
61	1, 60	eqtrid 2778	. 2 ⊢ (𝜑 → 𝐶 = (𝐽‘𝑋))
62	4, 14, 5, 15, 16, 17, 8, 18, 19, 20, 21, 22, 23, 24, 25, 6, 30	lcfrlem13 41593	. . 3 ⊢ (𝜑 → (𝐽‘𝑋) ∈ ({𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ∖ {(0_g‘𝐷)}))
63		eldifsni 4742	. . 3 ⊢ ((𝐽‘𝑋) ∈ ({𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} ∖ {(0_g‘𝐷)}) → (𝐽‘𝑋) ≠ (0_g‘𝐷))
64	62, 63	syl 17	. 2 ⊢ (𝜑 → (𝐽‘𝑋) ≠ (0_g‘𝐷))
65	61, 64	eqnetrd 2995	1 ⊢ (𝜑 → 𝐶 ≠ (0_g‘𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∃wrex 3056 {crab 3395 ∖ cdif 3899 ∩ cin 3901 {csn 4576 {cpr 4578 ↦ cmpt 5172 ‘cfv 6481 ℩crio 7302 (class class class)co 7346 Basecbs 17117 +_gcplusg 17158 ._rcmulr 17159 Scalarcsca 17161 ·_𝑠 cvsca 17162 0_gc0g 17340 Grpcgrp 18843 -_gcsg 18845 Ringcrg 20149 inv_rcinvr 20303 DivRingcdr 20642 LModclmod 20791 LSpanclspn 20902 LVecclvec 21034 LSAtomsclsa 39012 LFnlclfn 39095 LKerclk 39123 LDualcld 39161 HLchlt 39388 LHypclh 40022 DVecHcdvh 41116 ocHcoch 41385

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11059 ax-resscn 11060 ax-1cn 11061 ax-icn 11062 ax-addcl 11063 ax-addrcl 11064 ax-mulcl 11065 ax-mulrcl 11066 ax-mulcom 11067 ax-addass 11068 ax-mulass 11069 ax-distr 11070 ax-i2m1 11071 ax-1ne0 11072 ax-1rid 11073 ax-rnegex 11074 ax-rrecex 11075 ax-cnre 11076 ax-pre-lttri 11077 ax-pre-lttrn 11078 ax-pre-ltadd 11079 ax-pre-mulgt0 11080 ax-riotaBAD 38991

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-iin 4944 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-om 7797 df-1st 7921 df-2nd 7922 df-tpos 8156 df-undef 8203 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-er 8622 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-pnf 11145 df-mnf 11146 df-xr 11147 df-ltxr 11148 df-le 11149 df-sub 11343 df-neg 11344 df-nn 12123 df-2 12185 df-3 12186 df-4 12187 df-5 12188 df-6 12189 df-n0 12379 df-z 12466 df-uz 12730 df-fz 13405 df-struct 17055 df-sets 17072 df-slot 17090 df-ndx 17102 df-base 17118 df-ress 17139 df-plusg 17171 df-mulr 17172 df-sca 17174 df-vsca 17175 df-0g 17342 df-mre 17485 df-mrc 17486 df-acs 17488 df-proset 18197 df-poset 18216 df-plt 18231 df-lub 18247 df-glb 18248 df-join 18249 df-meet 18250 df-p0 18326 df-p1 18327 df-lat 18335 df-clat 18402 df-mgm 18545 df-sgrp 18624 df-mnd 18640 df-submnd 18689 df-grp 18846 df-minusg 18847 df-sbg 18848 df-subg 19033 df-cntz 19227 df-oppg 19256 df-lsm 19546 df-cmn 19692 df-abl 19693 df-mgp 20057 df-rng 20069 df-ur 20098 df-ring 20151 df-oppr 20253 df-dvdsr 20273 df-unit 20274 df-invr 20304 df-dvr 20317 df-drng 20644 df-lmod 20793 df-lss 20863 df-lsp 20903 df-lvec 21035 df-lsatoms 39014 df-lshyp 39015 df-lcv 39057 df-lfl 39096 df-lkr 39124 df-ldual 39162 df-oposet 39214 df-ol 39216 df-oml 39217 df-covers 39304 df-ats 39305 df-atl 39336 df-cvlat 39360 df-hlat 39389 df-llines 39536 df-lplanes 39537 df-lvols 39538 df-lines 39539 df-psubsp 39541 df-pmap 39542 df-padd 39834 df-lhyp 40026 df-laut 40027 df-ldil 40142 df-ltrn 40143 df-trl 40197 df-tgrp 40781 df-tendo 40793 df-edring 40795 df-dveca 41041 df-disoa 41067 df-dvech 41117 df-dib 41177 df-dic 41211 df-dih 41267 df-doch 41386 df-djh 41433

This theorem is referenced by: lcfrlem34 41614

W3C validator