tendoipl

Description: Property of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013)

	Ref	Expression
Hypotheses	tendoicl.h	$⊢ H = LHyp (K)$
	tendoicl.t	$⊢ T = LTrn (K) (W)$
	tendoicl.e	$⊢ E = TEndo (K) (W)$
	tendoicl.i	$⊢ I = (s \in E ⟼ (f \in T ⟼ {s (f)}^{-1}))$
	tendoi.b	$⊢ B = {Base}_{K}$
	tendoi.p	$⊢ P = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
	tendoi.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
Assertion	tendoipl	$⊢ ((K \in HL \land W \in H) \land S \in E) \to I (S) P S = O$

Proof

Step	Hyp	Ref	Expression
1		tendoicl.h	$⊢ H = LHyp (K)$
2		tendoicl.t	$⊢ T = LTrn (K) (W)$
3		tendoicl.e	$⊢ E = TEndo (K) (W)$
4		tendoicl.i	$⊢ I = (s \in E ⟼ (f \in T ⟼ {s (f)}^{-1}))$
5		tendoi.b	$⊢ B = {Base}_{K}$
6		tendoi.p	$⊢ P = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
7		tendoi.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
8		simpl	$⊢ ((K \in HL \land W \in H) \land S \in E) \to (K \in HL \land W \in H)$
9	1 2 3 4	tendoicl	$⊢ ((K \in HL \land W \in H) \land S \in E) \to I (S) \in E$
10		simpr	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S \in E$
11	1 2 3 6	tendoplcl	$⊢ ((K \in HL \land W \in H) \land I (S) \in E \land S \in E) \to I (S) P S \in E$
12	8 9 10 11	syl3anc	$⊢ ((K \in HL \land W \in H) \land S \in E) \to I (S) P S \in E$
13	5 1 2 3 7	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
14	13	adantr	$⊢ ((K \in HL \land W \in H) \land S \in E) \to O \in E$
15	4 2	tendoi2	$⊢ (S \in E \land g \in T) \to I (S) (g) = {S (g)}^{-1}$
16	15	adantll	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to I (S) (g) = {S (g)}^{-1}$
17	16	coeq1d	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to I (S) (g) \circ S (g) = {S (g)}^{-1} \circ S (g)$
18		simpll	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to (K \in HL \land W \in H)$
19	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land S \in E \land g \in T) \to S (g) \in T$
20	19	3expa	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to S (g) \in T$
21	5 1 2	ltrn1o	$⊢ ((K \in HL \land W \in H) \land S (g) \in T) \to S (g) : B \underset{1-1 onto}{⟶} B$
22	18 20 21	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to S (g) : B \underset{1-1 onto}{⟶} B$
23		f1ococnv1	$⊢ S (g) : B \underset{1-1 onto}{⟶} B \to {S (g)}^{-1} \circ S (g) = {I ↾}_{B}$
24	22 23	syl	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to {S (g)}^{-1} \circ S (g) = {I ↾}_{B}$
25	17 24	eqtrd	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to I (S) (g) \circ S (g) = {I ↾}_{B}$
26	9	adantr	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to I (S) \in E$
27		simplr	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to S \in E$
28		simpr	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to g \in T$
29	6 2	tendopl2	$⊢ (I (S) \in E \land S \in E \land g \in T) \to (I (S) P S) (g) = I (S) (g) \circ S (g)$
30	26 27 28 29	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to (I (S) P S) (g) = I (S) (g) \circ S (g)$
31	7 5	tendo02	$⊢ g \in T \to O (g) = {I ↾}_{B}$
32	31	adantl	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to O (g) = {I ↾}_{B}$
33	25 30 32	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to (I (S) P S) (g) = O (g)$
34	33	ralrimiva	$⊢ ((K \in HL \land W \in H) \land S \in E) \to \forall g \in T (I (S) P S) (g) = O (g)$
35	1 2 3	tendoeq1	$⊢ ((K \in HL \land W \in H) \land (I (S) P S \in E \land O \in E) \land \forall g \in T (I (S) P S) (g) = O (g)) \to I (S) P S = O$
36	8 12 14 34 35	syl121anc	$⊢ ((K \in HL \land W \in H) \land S \in E) \to I (S) P S = O$

Metamath Proof Explorer

Theorem tendoipl

Proof