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 42019

Description: Lemma for lcfr 42033. (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 41558	. . 3 ⊢ (𝜑 → 𝑈 ∈ LMod)
5		lcfrlem24.s	. . . 4 ⊢ 𝑆 = (Scalar‘𝑈)
6	5	lmodring 20865	. . 3 ⊢ (𝑈 ∈ LMod → 𝑆 ∈ Ring)
7	4, 6	syl 17	. 2 ⊢ (𝜑 → 𝑆 ∈ Ring)
8	1, 2, 3	dvhlvec 41557	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LVec)
9	5	lvecdrng 21102	. . . 4 ⊢ (𝑈 ∈ LVec → 𝑆 ∈ DivRing)
10	8, 9	syl 17	. . 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 2737	. . . . 5 ⊢ (LFnl‘𝑈) = (LFnl‘𝑈)
18		lcfrlem24.l	. . . . 5 ⊢ 𝐿 = (LKer‘𝑈)
19		lcfrlem25.d	. . . . 5 ⊢ 𝐷 = (LDual‘𝑈)
20		eqid 2737	. . . . 5 ⊢ (0_g‘𝐷) = (0_g‘𝐷)
21		eqid 2737	. . . . 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 42000	. . . 4 ⊢ (𝜑 → (𝐽‘𝑌) ∈ (LFnl‘𝑈))
25		eqid 2737	. . . . . 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 42012	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
32	25, 26, 4, 31	lsatlssel 39445	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑈))
33		lcfrlem24.ib	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ 𝐵)
34	12, 25	lssel 20934	. . . . 5 ⊢ ((𝐵 ∈ (LSubSp‘𝑈) ∧ 𝐼 ∈ 𝐵) → 𝐼 ∈ 𝑉)
35	32, 33, 34	syl2anc 585	. . . 4 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
36	5, 15, 12, 17	lflcl 39512	. . . 4 ⊢ ((𝑈 ∈ LMod ∧ (𝐽‘𝑌) ∈ (LFnl‘𝑈) ∧ 𝐼 ∈ 𝑉) → ((𝐽‘𝑌)‘𝐼) ∈ 𝑅)
37	4, 24, 35, 36	syl3anc 1374	. . 3 ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ∈ 𝑅)
38		lcfrlem28.jn	. . 3 ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)
39		lcfrlem24.q	. . . 4 ⊢ 𝑄 = (0_g‘𝑆)
40		lcfrlem29.i	. . . 4 ⊢ 𝐹 = (inv_r‘𝑆)
41	15, 39, 40	drnginvrcl 20732	. . 3 ⊢ ((𝑆 ∈ DivRing ∧ ((𝐽‘𝑌)‘𝐼) ∈ 𝑅 ∧ ((𝐽‘𝑌)‘𝐼) ≠ 𝑄) → (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅)
42	10, 37, 38, 41	syl3anc 1374	. 2 ⊢ (𝜑 → (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅)
43	1, 11, 2, 12, 13, 14, 5, 15, 16, 17, 18, 19, 20, 21, 22, 3, 28	lcfrlem10 42000	. . 3 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (LFnl‘𝑈))
44	5, 15, 12, 17	lflcl 39512	. . 3 ⊢ ((𝑈 ∈ LMod ∧ (𝐽‘𝑋) ∈ (LFnl‘𝑈) ∧ 𝐼 ∈ 𝑉) → ((𝐽‘𝑋)‘𝐼) ∈ 𝑅)
45	4, 43, 35, 44	syl3anc 1374	. 2 ⊢ (𝜑 → ((𝐽‘𝑋)‘𝐼) ∈ 𝑅)
46		eqid 2737	. . 3 ⊢ (._r‘𝑆) = (._r‘𝑆)
47	15, 46	ringcl 20233	. 2 ⊢ ((𝑆 ∈ Ring ∧ (𝐹‘((𝐽‘𝑌)‘𝐼)) ∈ 𝑅 ∧ ((𝐽‘𝑋)‘𝐼) ∈ 𝑅) → ((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼)) ∈ 𝑅)
48	7, 42, 45, 47	syl3anc 1374	1 ⊢ (𝜑 → ((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼)) ∈ 𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∃wrex 3062 {crab 3390 ∖ cdif 3887 ∩ cin 3889 {csn 4568 {cpr 4570 ↦ cmpt 5167 ‘cfv 6500 ℩crio 7325 (class class class)co 7369 Basecbs 17181 +_gcplusg 17222 ._rcmulr 17223 Scalarcsca 17225 ·_𝑠 cvsca 17226 0_gc0g 17404 Ringcrg 20216 inv_rcinvr 20369 DivRingcdr 20708 LModclmod 20857 LSubSpclss 20928 LSpanclspn 20968 LVecclvec 21099 LSAtomsclsa 39422 LFnlclfn 39505 LKerclk 39533 LDualcld 39571 HLchlt 39798 LHypclh 40432 DVecHcdvh 41526 ocHcoch 41795

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5308 ax-pr 5376 ax-un 7691 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117 ax-riotaBAD 39401

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7820 df-1st 7944 df-2nd 7945 df-tpos 8178 df-undef 8225 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-er 8645 df-map 8777 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-pnf 11183 df-mnf 11184 df-xr 11185 df-ltxr 11186 df-le 11187 df-sub 11381 df-neg 11382 df-nn 12177 df-2 12246 df-3 12247 df-4 12248 df-5 12249 df-6 12250 df-n0 12440 df-z 12527 df-uz 12791 df-fz 13464 df-struct 17119 df-sets 17136 df-slot 17154 df-ndx 17166 df-base 17182 df-ress 17203 df-plusg 17235 df-mulr 17236 df-sca 17238 df-vsca 17239 df-0g 17406 df-mre 17550 df-mrc 17551 df-acs 17553 df-proset 18262 df-poset 18281 df-plt 18296 df-lub 18312 df-glb 18313 df-join 18314 df-meet 18315 df-p0 18391 df-p1 18392 df-lat 18400 df-clat 18467 df-mgm 18610 df-sgrp 18689 df-mnd 18705 df-submnd 18754 df-grp 18914 df-minusg 18915 df-sbg 18916 df-subg 19101 df-cntz 19294 df-oppg 19323 df-lsm 19613 df-cmn 19759 df-abl 19760 df-mgp 20124 df-rng 20136 df-ur 20165 df-ring 20218 df-oppr 20319 df-dvdsr 20339 df-unit 20340 df-invr 20370 df-dvr 20383 df-drng 20710 df-lmod 20859 df-lss 20929 df-lsp 20969 df-lvec 21100 df-lsatoms 39424 df-lshyp 39425 df-lcv 39467 df-lfl 39506 df-oposet 39624 df-ol 39626 df-oml 39627 df-covers 39714 df-ats 39715 df-atl 39746 df-cvlat 39770 df-hlat 39799 df-llines 39946 df-lplanes 39947 df-lvols 39948 df-lines 39949 df-psubsp 39951 df-pmap 39952 df-padd 40244 df-lhyp 40436 df-laut 40437 df-ldil 40552 df-ltrn 40553 df-trl 40607 df-tgrp 41191 df-tendo 41203 df-edring 41205 df-dveca 41451 df-disoa 41477 df-dvech 41527 df-dib 41587 df-dic 41621 df-dih 41677 df-doch 41796 df-djh 41843

This theorem is referenced by: lcfrlem30 42020 lcfrlem31 42021 lcfrlem37 42027

W3C validator