tendolinv

Description: Left multiplicative inverse for endomorphism. (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	tendolinv	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to N (S) \circ S = {I ↾}_{T}$

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		simp1	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to (K \in HL \land W \in H)$
10		eqid	$⊢ EDRing (K) (W) = EDRing (K) (W)$
11	2 10 6 7	dvhsca	$⊢ (K \in HL \land W \in H) \to F = EDRing (K) (W)$
12	9 11	syl	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to F = EDRing (K) (W)$
13	2 10	erngdv	$⊢ (K \in HL \land W \in H) \to EDRing (K) (W) \in DivRing$
14	9 13	syl	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to EDRing (K) (W) \in DivRing$
15	12 14	eqeltrd	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to F \in DivRing$
16		simp2	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to S \in E$
17		eqid	$⊢ {Base}_{F} = {Base}_{F}$
18	2 4 6 7 17	dvhbase	$⊢ (K \in HL \land W \in H) \to {Base}_{F} = E$
19	9 18	syl	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to {Base}_{F} = E$
20	16 19	eleqtrrd	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to S \in {Base}_{F}$
21		simp3	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to S \neq O$
22	11	fveq2d	$⊢ (K \in HL \land W \in H) \to 0_{F} = 0_{EDRing (K) (W)}$
23		eqid	$⊢ 0_{EDRing (K) (W)} = 0_{EDRing (K) (W)}$
24	1 2 3 10 5 23	erng0g	$⊢ (K \in HL \land W \in H) \to 0_{EDRing (K) (W)} = O$
25	22 24	eqtrd	$⊢ (K \in HL \land W \in H) \to 0_{F} = O$
26	9 25	syl	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to 0_{F} = O$
27	21 26	neeqtrrd	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to S \neq 0_{F}$
28		eqid	$⊢ 0_{F} = 0_{F}$
29		eqid	$⊢ \cdot_{F} = \cdot_{F}$
30		eqid	$⊢ 1_{F} = 1_{F}$
31	17 28 29 30 8	drnginvrl	$⊢ (F \in DivRing \land S \in {Base}_{F} \land S \neq 0_{F}) \to N (S) \cdot_{F} S = 1_{F}$
32	15 20 27 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to N (S) \cdot_{F} S = 1_{F}$
33	1 2 3 4 5 6 7 8	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)$
34	33	simpld	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to N (S) \in E$
35	2 3 4 6 7 29	dvhmulr	$⊢ ((K \in HL \land W \in H) \land (N (S) \in E \land S \in E)) \to N (S) \cdot_{F} S = N (S) \circ S$
36	9 34 16 35	syl12anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to N (S) \cdot_{F} S = N (S) \circ S$
37	11	fveq2d	$⊢ (K \in HL \land W \in H) \to 1_{F} = 1_{EDRing (K) (W)}$
38		eqid	$⊢ 1_{EDRing (K) (W)} = 1_{EDRing (K) (W)}$
39	2 3 10 38	erng1r	$⊢ (K \in HL \land W \in H) \to 1_{EDRing (K) (W)} = {I ↾}_{T}$
40	37 39	eqtrd	$⊢ (K \in HL \land W \in H) \to 1_{F} = {I ↾}_{T}$
41	9 40	syl	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to 1_{F} = {I ↾}_{T}$
42	32 36 41	3eqtr3d	$⊢ ((K \in HL \land W \in H) \land S \in E \land S \neq O) \to N (S) \circ S = {I ↾}_{T}$

Metamath Proof Explorer

Theorem tendolinv

Proof