tendoinvcl - Mathbox for Norm Megill

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

Theorem tendoinvcl 41091

Description: Closure of multiplicative inverse for endomorphism. We use the scalar inverse of the vector space since it is much simpler than the direct inverse of cdleml8 40970. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.)

**Hypotheses**
Ref	Expression
tendoinv.b	⊢ 𝐵 = (Base‘𝐾)
tendoinv.h	⊢ 𝐻 = (LHyp‘𝐾)
tendoinv.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
tendoinv.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
tendoinv.o	⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
tendoinv.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
tendoinv.f	⊢ 𝐹 = (Scalar‘𝑈)
tendoinv.n	⊢ 𝑁 = (inv_r‘𝐹)

**Assertion**
Ref	Expression
tendoinvcl	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → ((𝑁‘𝑆) ∈ 𝐸 ∧ (𝑁‘𝑆) ≠ 𝑂))

Distinct variable groups: 𝐵,ℎ ℎ,𝐻 ℎ,𝐾 𝑇,ℎ ℎ,𝑊 Allowed substitution hints: 𝑆(ℎ) 𝑈(ℎ) 𝐸(ℎ) 𝐹(ℎ) 𝑁(ℎ) 𝑂(ℎ)

**Proof of Theorem tendoinvcl**
Step	Hyp	Ref	Expression
1		tendoinv.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
2		eqid 2729	. . . . . . 7 ⊢ ((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊)
3		tendoinv.u	. . . . . . 7 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
4		tendoinv.f	. . . . . . 7 ⊢ 𝐹 = (Scalar‘𝑈)
5	1, 2, 3, 4	dvhsca 41069	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐹 = ((EDRing‘𝐾)‘𝑊))
6	1, 2	erngdv 40980	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ DivRing)
7	5, 6	eqeltrd 2828	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐹 ∈ DivRing)
8	7	3ad2ant1 1133	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → 𝐹 ∈ DivRing)
9		simp2 1137	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → 𝑆 ∈ 𝐸)
10		tendoinv.e	. . . . . . 7 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
11		eqid 2729	. . . . . . 7 ⊢ (Base‘𝐹) = (Base‘𝐹)
12	1, 10, 3, 4, 11	dvhbase 41070	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝐹) = 𝐸)
13	12	3ad2ant1 1133	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → (Base‘𝐹) = 𝐸)
14	9, 13	eleqtrrd 2831	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → 𝑆 ∈ (Base‘𝐹))
15		simp3 1138	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → 𝑆 ≠ 𝑂)
16	5	fveq2d 6844	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (0_g‘𝐹) = (0_g‘((EDRing‘𝐾)‘𝑊)))
17		tendoinv.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐾)
18		tendoinv.t	. . . . . . . 8 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
19		tendoinv.o	. . . . . . . 8 ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
20		eqid 2729	. . . . . . . 8 ⊢ (0_g‘((EDRing‘𝐾)‘𝑊)) = (0_g‘((EDRing‘𝐾)‘𝑊))
21	17, 1, 18, 2, 19, 20	erng0g 40981	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (0_g‘((EDRing‘𝐾)‘𝑊)) = 𝑂)
22	16, 21	eqtrd 2764	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (0_g‘𝐹) = 𝑂)
23	22	3ad2ant1 1133	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → (0_g‘𝐹) = 𝑂)
24	15, 23	neeqtrrd 2999	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → 𝑆 ≠ (0_g‘𝐹))
25		eqid 2729	. . . . 5 ⊢ (0_g‘𝐹) = (0_g‘𝐹)
26		tendoinv.n	. . . . 5 ⊢ 𝑁 = (inv_r‘𝐹)
27	11, 25, 26	drnginvrcl 20673	. . . 4 ⊢ ((𝐹 ∈ DivRing ∧ 𝑆 ∈ (Base‘𝐹) ∧ 𝑆 ≠ (0_g‘𝐹)) → (𝑁‘𝑆) ∈ (Base‘𝐹))
28	8, 14, 24, 27	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → (𝑁‘𝑆) ∈ (Base‘𝐹))
29	28, 13	eleqtrd 2830	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → (𝑁‘𝑆) ∈ 𝐸)
30	11, 25, 26	drnginvrn0 20674	. . . 4 ⊢ ((𝐹 ∈ DivRing ∧ 𝑆 ∈ (Base‘𝐹) ∧ 𝑆 ≠ (0_g‘𝐹)) → (𝑁‘𝑆) ≠ (0_g‘𝐹))
31	8, 14, 24, 30	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → (𝑁‘𝑆) ≠ (0_g‘𝐹))
32	31, 23	neeqtrd 2994	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → (𝑁‘𝑆) ≠ 𝑂)
33	29, 32	jca 511	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → ((𝑁‘𝑆) ∈ 𝐸 ∧ (𝑁‘𝑆) ≠ 𝑂))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ↦ cmpt 5183 I cid 5525 ↾ cres 5633 ‘cfv 6499 Basecbs 17155 Scalarcsca 17199 0_gc0g 17378 inv_rcinvr 20307 DivRingcdr 20649 HLchlt 39336 LHypclh 39971 LTrncltrn 40088 TEndoctendo 40739 EDRingcedring 40740 DVecHcdvh 41065

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-riotaBAD 38939

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-tpos 8182 df-undef 8229 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-6 12229 df-n0 12419 df-z 12506 df-uz 12770 df-fz 13445 df-struct 17093 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-sca 17212 df-vsca 17213 df-0g 17380 df-proset 18235 df-poset 18254 df-plt 18269 df-lub 18285 df-glb 18286 df-join 18287 df-meet 18288 df-p0 18364 df-p1 18365 df-lat 18373 df-clat 18440 df-mgm 18549 df-sgrp 18628 df-mnd 18644 df-grp 18850 df-minusg 18851 df-cmn 19696 df-abl 19697 df-mgp 20061 df-rng 20073 df-ur 20102 df-ring 20155 df-oppr 20257 df-dvdsr 20277 df-unit 20278 df-invr 20308 df-dvr 20321 df-drng 20651 df-oposet 39162 df-ol 39164 df-oml 39165 df-covers 39252 df-ats 39253 df-atl 39284 df-cvlat 39308 df-hlat 39337 df-llines 39485 df-lplanes 39486 df-lvols 39487 df-lines 39488 df-psubsp 39490 df-pmap 39491 df-padd 39783 df-lhyp 39975 df-laut 39976 df-ldil 40091 df-ltrn 40092 df-trl 40146 df-tendo 40742 df-edring 40744 df-dvech 41066

This theorem is referenced by: tendolinv 41092 tendorinv 41093 dih1dimatlem0 41315 dih1dimatlem 41316

W3C validator