tendoinvcl

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 . (Contributed by NM, 10-Apr-2014) (Revised by Mario Carneiro, 23-Jun-2014)

	Ref	Expression
Hypotheses	tendoinv.b	$⊢ B = {Base}_{K}$
	tendoinv.h	$⊢ H = LHyp (K)$
	tendoinv.t	$⊢ T = LTrn (K) (W)$
	tendoinv.e	$⊢ E = TEndo (K) (W)$
	tendoinv.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	tendoinv.u	$⊢ U = DVecH (K) (W)$
	tendoinv.f	$⊢ F = Scalar (U)$
	tendoinv.n	$⊢ N = {inv}_{r} (F)$
Assertion	tendoinvcl	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to (N (S) \in E \land N (S) \neq O)$

Proof

Step	Hyp	Ref	Expression
1		tendoinv.b	$⊢ B = {Base}_{K}$
2		tendoinv.h	$⊢ H = LHyp (K)$
3		tendoinv.t	$⊢ T = LTrn (K) (W)$
4		tendoinv.e	$⊢ E = TEndo (K) (W)$
5		tendoinv.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
6		tendoinv.u	$⊢ U = DVecH (K) (W)$
7		tendoinv.f	$⊢ F = Scalar (U)$
8		tendoinv.n	$⊢ N = {inv}_{r} (F)$
9		eqid	$⊢ EDRing (K) (W) = EDRing (K) (W)$
10	2 9 6 7	dvhsca	$⊢ (K \in HL \land W \in H) \to F = EDRing (K) (W)$
11	2 9	erngdv	$⊢ (K \in HL \land W \in H) \to EDRing (K) (W) \in DivRing$
12	10 11	eqeltrd	$⊢ (K \in HL \land W \in H) \to F \in DivRing$
13	12	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to F \in DivRing$
14		simp2	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to S \in E$
15		eqid	$⊢ {Base}_{F} = {Base}_{F}$
16	2 4 6 7 15	dvhbase	$⊢ (K \in HL \land W \in H) \to {Base}_{F} = E$
17	16	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to {Base}_{F} = E$
18	14 17	eleqtrrd	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to S \in {Base}_{F}$
19		simp3	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to S \neq O$
20	10	fveq2d	$⊢ (K \in HL \land W \in H) \to 0_{F} = 0_{EDRing (K) (W)}$
21		eqid	$⊢ 0_{EDRing (K) (W)} = 0_{EDRing (K) (W)}$
22	1 2 3 9 5 21	erng0g	$⊢ (K \in HL \land W \in H) \to 0_{EDRing (K) (W)} = O$
23	20 22	eqtrd	$⊢ (K \in HL \land W \in H) \to 0_{F} = O$
24	23	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to 0_{F} = O$
25	19 24	neeqtrrd	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to S \neq 0_{F}$
26		eqid	$⊢ 0_{F} = 0_{F}$
27	15 26 8	drnginvrcl	$⊢ (F \in DivRing \land S \in {Base}_{F} \land S \neq 0_{F}) \to N (S) \in {Base}_{F}$
28	13 18 25 27	syl3anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to N (S) \in {Base}_{F}$
29	28 17	eleqtrd	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to N (S) \in E$
30	15 26 8	drnginvrn0	$⊢ (F \in DivRing \land S \in {Base}_{F} \land S \neq 0_{F}) \to N (S) \neq 0_{F}$
31	13 18 25 30	syl3anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to N (S) \neq 0_{F}$
32	31 24	neeqtrd	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to N (S) \neq O$
33	29 32	jca	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to (N (S) \in E \land N (S) \neq O)$

Metamath Proof Explorer

Theorem tendoinvcl

Proof