erng1lem

Description: Value of the endomorphism division ring unit. (Contributed by NM, 12-Oct-2013)

	Ref	Expression
Hypotheses	erng1.h	$⊢ H = LHyp (K)$
	erng1.t	$⊢ T = LTrn (K) (W)$
	erng1.e	$⊢ E = TEndo (K) (W)$
	erng1.d	$⊢ D = EDRing (K) (W)$
	erng1.r	$⊢ (K \in HL \land W \in H) \to D \in Ring$
Assertion	erng1lem	$⊢ (K \in HL \land W \in H) \to 1_{D} = {I ↾}_{T}$

Proof

Step	Hyp	Ref	Expression
1		erng1.h	$⊢ H = LHyp (K)$
2		erng1.t	$⊢ T = LTrn (K) (W)$
3		erng1.e	$⊢ E = TEndo (K) (W)$
4		erng1.d	$⊢ D = EDRing (K) (W)$
5		erng1.r	$⊢ (K \in HL \land W \in H) \to D \in Ring$
6	1 2 3	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in E$
7		eqid	$⊢ {Base}_{D} = {Base}_{D}$
8	1 2 3 4 7	erngbase	$⊢ (K \in HL \land W \in H) \to {Base}_{D} = E$
9	6 8	eleqtrrd	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in {Base}_{D}$
10	8	eleq2d	$⊢ (K \in HL \land W \in H) \to (u \in {Base}_{D} \leftrightarrow u \in E)$
11		simpl	$⊢ ((K \in HL \land W \in H) \land u \in E) \to (K \in HL \land W \in H)$
12	6	adantr	$⊢ ((K \in HL \land W \in H) \land u \in E) \to {I ↾}_{T} \in E$
13		simpr	$⊢ ((K \in HL \land W \in H) \land u \in E) \to u \in E$
14		eqid	$⊢ \cdot_{D} = \cdot_{D}$
15	1 2 3 4 14	erngmul	$⊢ ((K \in HL \land W \in H) \land ({I ↾}_{T} \in E \land u \in E)) \to ({I ↾}_{T}) \cdot_{D} u = ({I ↾}_{T}) \circ u$
16	11 12 13 15	syl12anc	$⊢ ((K \in HL \land W \in H) \land u \in E) \to ({I ↾}_{T}) \cdot_{D} u = ({I ↾}_{T}) \circ u$
17	1 2 3	tendo1mul	$⊢ ((K \in HL \land W \in H) \land u \in E) \to ({I ↾}_{T}) \circ u = u$
18	16 17	eqtrd	$⊢ ((K \in HL \land W \in H) \land u \in E) \to ({I ↾}_{T}) \cdot_{D} u = u$
19	1 2 3 4 14	erngmul	$⊢ ((K \in HL \land W \in H) \land (u \in E \land {I ↾}_{T} \in E)) \to u \cdot_{D} ({I ↾}_{T}) = u \circ ({I ↾}_{T})$
20	11 13 12 19	syl12anc	$⊢ ((K \in HL \land W \in H) \land u \in E) \to u \cdot_{D} ({I ↾}_{T}) = u \circ ({I ↾}_{T})$
21	1 2 3	tendo1mulr	$⊢ ((K \in HL \land W \in H) \land u \in E) \to u \circ ({I ↾}_{T}) = u$
22	20 21	eqtrd	$⊢ ((K \in HL \land W \in H) \land u \in E) \to u \cdot_{D} ({I ↾}_{T}) = u$
23	18 22	jca	$⊢ ((K \in HL \land W \in H) \land u \in E) \to (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u)$
24	23	ex	$⊢ (K \in HL \land W \in H) \to (u \in E \to (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u))$
25	10 24	sylbid	$⊢ (K \in HL \land W \in H) \to (u \in {Base}_{D} \to (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u))$
26	25	ralrimiv	$⊢ (K \in HL \land W \in H) \to \forall u \in {Base}_{D} (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u)$
27		eqid	$⊢ 1_{D} = 1_{D}$
28	7 14 27	isringid	$⊢ D \in Ring \to (({I ↾}_{T} \in {Base}_{D} \land \forall u \in {Base}_{D} (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u)) \leftrightarrow 1_{D} = {I ↾}_{T})$
29	5 28	syl	$⊢ (K \in HL \land W \in H) \to (({I ↾}_{T} \in {Base}_{D} \land \forall u \in {Base}_{D} (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u)) \leftrightarrow 1_{D} = {I ↾}_{T})$
30	9 26 29	mpbi2and	$⊢ (K \in HL \land W \in H) \to 1_{D} = {I ↾}_{T}$

Metamath Proof Explorer

Theorem erng1lem

Proof