lcfrlem29 - Mathbox for Norm Megill

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

Theorem lcfrlem29 42831

Description: Lemma for lcfr 42845. (Contributed by NM, 9-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‘𝑆)

**Assertion**
Ref	Expression
lcfrlem29	⊢ (𝜑 → ((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼)) ∈ 𝑅)

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

**Proof of Theorem lcfrlem29**
Step	Hyp	Ref	Expression
1		lcfrlem17.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
2		lcfrlem17.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
3		lcfrlem17.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4	1, 2, 3	dvhlmod 42370	. . 3 ⊢ (𝜑 → 𝑈 ∈ LMod)
5		lcfrlem24.s	. . . 4 ⊢ 𝑆 = (Scalar‘𝑈)
6	5	lmodring 21176	. . 3 ⊢ (𝑈 ∈ LMod → 𝑆 ∈ Ring)
7	4, 6	syl 18	. 2 ⊢ (𝜑 → 𝑆 ∈ Ring)
8	1, 2, 3	dvhlvec 42369	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LVec)
9	5	lvecdrng 21413	. . . 4 ⊢ (𝑈 ∈ LVec → 𝑆 ∈ DivRing)
10	8, 9	syl 18	. . 3 ⊢ (𝜑 → 𝑆 ∈ DivRing)
11		lcfrlem17.o	. . . . 5 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
12		lcfrlem17.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
13		lcfrlem17.p	. . . . 5 ⊢ + = (+_g‘𝑈)
14		lcfrlem24.t	. . . . 5 ⊢ · = ( ·_𝑠 ‘𝑈)
15		lcfrlem24.r	. . . . 5 ⊢ 𝑅 = (Base‘𝑆)
16		lcfrlem17.z	. . . . 5 ⊢ 0 = (0_g‘𝑈)
17		eqid 2763	. . . . 5 ⊢ (LFnl‘𝑈) = (LFnl‘𝑈)
18		lcfrlem24.l	. . . . 5 ⊢ 𝐿 = (LKer‘𝑈)
19		lcfrlem25.d	. . . . 5 ⊢ 𝐷 = (LDual‘𝑈)
20		eqid 2763	. . . . 5 ⊢ (0_g‘𝐷) = (0_g‘𝐷)
21		eqid 2763	. . . . 5 ⊢ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}
22		lcfrlem24.j	. . . . 5 ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))
23		lcfrlem17.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
24	1, 11, 2, 12, 13, 14, 5, 15, 16, 17, 18, 19, 20, 21, 22, 3, 23	lcfrlem10 42812	. . . 4 ⊢ (𝜑 → (𝐽‘𝑌) ∈ (LFnl‘𝑈))
25		eqid 2763	. . . . . 6 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
26		lcfrlem17.a	. . . . . 6 ⊢ 𝐴 = (LSAtoms‘𝑈)
27		lcfrlem17.n	. . . . . . 7 ⊢ 𝑁 = (LSpan‘𝑈)
28		lcfrlem17.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
29		lcfrlem17.ne	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
30		lcfrlem22.b	. . . . . . 7 ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))
31	1, 11, 2, 12, 13, 16, 27, 26, 3, 28, 23, 29, 30	lcfrlem22 42824	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
32	25, 26, 4, 31	lsatlssel 40257	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑈))
33		lcfrlem24.ib	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ 𝐵)
34	12, 25	lssel 21245	. . . . 5 ⊢ ((𝐵 ∈ (LSubSp‘𝑈) ∧ 𝐼 ∈ 𝐵) → 𝐼 ∈ 𝑉)
35	32, 33, 34	syl2anc 596	. . . 4 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
36	5, 15, 12, 17	lflcl 40324	. . . 4 ⊢ ((𝑈 ∈ LMod ∧ (𝐽‘𝑌) ∈ (LFnl‘𝑈) ∧ 𝐼 ∈ 𝑉) → ((𝐽‘𝑌)‘𝐼) ∈ 𝑅)
37	4, 24, 35, 36	syl3anc 1399	. . 3 ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ∈ 𝑅)
38		lcfrlem28.jn	. . 3 ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)
39		lcfrlem24.q	. . . 4 ⊢ 𝑄 = (0_g‘𝑆)
40		lcfrlem29.i	. . . 4 ⊢ 𝐹 = (inv_r‘𝑆)
41	15, 39, 40	drnginvrcl 21044	. . 3 ⊢ ((𝑆 ∈ DivRing ∧ ((𝐽‘𝑌)‘𝐼) ∈ 𝑅 ∧ ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) → (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅)
42	10, 37, 38, 41	syl3anc 1399	. 2 ⊢ (𝜑 → (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅)
43	1, 11, 2, 12, 13, 14, 5, 15, 16, 17, 18, 19, 20, 21, 22, 3, 28	lcfrlem10 42812	. . 3 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (LFnl‘𝑈))
44	5, 15, 12, 17	lflcl 40324	. . 3 ⊢ ((𝑈 ∈ LMod ∧ (𝐽‘𝑋) ∈ (LFnl‘𝑈) ∧ 𝐼 ∈ 𝑉) → ((𝐽‘𝑋)‘𝐼) ∈ 𝑅)
45	4, 43, 35, 44	syl3anc 1399	. 2 ⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) ∈ 𝑅)
46		eqid 2763	. . 3 ⊢ (._r‘𝑆) = (._r‘𝑆)
47	15, 46	ringcl 20510	. 2 ⊢ ((𝑆 ∈ Ring ∧ (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅 ∧ ((𝐽‘𝑋)‘𝐼) ∈ 𝑅) → ((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼)) ∈ 𝑅)
48	7, 42, 45, 47	syl3anc 1399	1 ⊢ (𝜑 → ((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼)) ∈ 𝑅)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∃wrex 3090 {crab 3416 ∖ cdif 4048 ∩ cin 4092 {csn 4588 {cpr 4590 ↦ cmpt 5190 ‘cfv 6561 ℩crio 7402 (class class class)co 7446 Basecbs 17419 +_gcplusg 17460 ._rcmulr 17461 Scalarcsca 17463 ·_𝑠 cvsca 17464 0_gc0g 17642 Ringcrg 20492 inv_rcinvr 20650 DivRingcdr 21013 LModclmod 21168 LSubSpclss 21239 LSpanclspn 21279 LVecclvec 21410 LSAtomsclsa 40234 LFnlclfn 40317 LKerclk 40345 LDualcld 40383 HLchlt 40610 LHypclh 41244 DVecHcdvh 42338 ocHcoch 42607

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-riotaBAD 40213

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-tpos 8274 df-undef 8321 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-2o 8508 df-er 8748 df-map 8880 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-nn 12366 df-2 12435 df-3 12436 df-4 12437 df-5 12438 df-6 12439 df-n0 12637 df-z 12724 df-uz 12996 df-fz 13670 df-struct 17357 df-sets 17374 df-slot 17392 df-ndx 17404 df-base 17420 df-ress 17441 df-plusg 17473 df-mulr 17474 df-sca 17476 df-vsca 17477 df-0g 17644 df-mre 17788 df-mrc 17789 df-acs 17791 df-proset 18500 df-poset 18519 df-plt 18534 df-lub 18550 df-glb 18551 df-join 18552 df-meet 18553 df-p0 18629 df-p1 18630 df-lat 18638 df-clat 18705 df-mgm 18848 df-sgrp 18940 df-mnd 18956 df-submnd 19011 df-grp 19179 df-minusg 19180 df-sbg 19181 df-subg 19365 df-cntz 19564 df-oppg 19593 df-lsm 19883 df-cmn 20029 df-abl 20030 df-mgp 20394 df-rng 20408 df-ur 20441 df-ring 20494 df-oppr 20600 df-dvdsr 20620 df-unit 20621 df-invr 20651 df-dvr 20664 df-drng 21015 df-lmod 21170 df-lss 21240 df-lsp 21280 df-lvec 21411 df-lsatoms 40236 df-lshyp 40237 df-lcv 40279 df-lfl 40318 df-oposet 40436 df-ol 40438 df-oml 40439 df-covers 40526 df-ats 40527 df-atl 40558 df-cvlat 40582 df-hlat 40611 df-llines 40758 df-lplanes 40759 df-lvols 40760 df-lines 40761 df-psubsp 40763 df-pmap 40764 df-padd 41056 df-lhyp 41248 df-laut 41249 df-ldil 41364 df-ltrn 41365 df-trl 41419 df-tgrp 42003 df-tendo 42015 df-edring 42017 df-dveca 42263 df-disoa 42289 df-dvech 42339 df-dib 42399 df-dic 42433 df-dih 42489 df-doch 42608 df-djh 42655

This theorem is used by: lcfrlem30 42832 lcfrlem31 42833 lcfrlem37 42839

W3C validator