tendoicl

Description: Closure 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}))$
Assertion	tendoicl	$⊢ ((K \in HL \land W \in H) \land S \in E) \to I (S) \in E$

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		eqid	$⊢ \leq_{K} = \leq_{K}$
6		eqid	$⊢ trL (K) (W) = trL (K) (W)$
7		simpl	$⊢ ((K \in HL \land W \in H) \land S \in E) \to (K \in HL \land W \in H)$
8		simpll	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to (K \in HL \land W \in H)$
9	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land S \in E \land g \in T) \to S (g) \in T$
10	9	3expa	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to S (g) \in T$
11	1 2	ltrncnv	$⊢ ((K \in HL \land W \in H) \land S (g) \in T) \to {S (g)}^{-1} \in T$
12	8 10 11	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to {S (g)}^{-1} \in T$
13	12	fmpttd	$⊢ ((K \in HL \land W \in H) \land S \in E) \to (g \in T ⟼ {S (g)}^{-1}) : T ⟶ T$
14	4 2	tendoi	$⊢ S \in E \to I (S) = (g \in T ⟼ {S (g)}^{-1})$
15	14	adantl	$⊢ ((K \in HL \land W \in H) \land S \in E) \to I (S) = (g \in T ⟼ {S (g)}^{-1})$
16	15	feq1d	$⊢ ((K \in HL \land W \in H) \land S \in E) \to (I (S) : T ⟶ T \leftrightarrow (g \in T ⟼ {S (g)}^{-1}) : T ⟶ T)$
17	13 16	mpbird	$⊢ ((K \in HL \land W \in H) \land S \in E) \to I (S) : T ⟶ T$
18		simp1r	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to S \in E$
19	1 2	ltrnco	$⊢ ((K \in HL \land W \in H) \land g \in T \land h \in T) \to g \circ h \in T$
20	19	3adant1r	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to g \circ h \in T$
21	4 2	tendoi2	$⊢ (S \in E \land g \circ h \in T) \to I (S) (g \circ h) = {S (g \circ h)}^{-1}$
22	18 20 21	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to I (S) (g \circ h) = {S (g \circ h)}^{-1}$
23		cnvco	$⊢ {(S (h) \circ S (g))}^{-1} = {S (g)}^{-1} \circ {S (h)}^{-1}$
24	1 2	ltrncom	$⊢ ((K \in HL \land W \in H) \land g \in T \land h \in T) \to g \circ h = h \circ g$
25	24	3adant1r	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to g \circ h = h \circ g$
26	25	fveq2d	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to S (g \circ h) = S (h \circ g)$
27		simp1ll	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to K \in HL$
28		simp1lr	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to W \in H$
29		simp3	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to h \in T$
30		simp2	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to g \in T$
31	1 2 3	tendovalco	$⊢ ((K \in HL \land W \in H \land S \in E) \land (h \in T \land g \in T)) \to S (h \circ g) = S (h) \circ S (g)$
32	27 28 18 29 30 31	syl32anc	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to S (h \circ g) = S (h) \circ S (g)$
33	26 32	eqtrd	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to S (g \circ h) = S (h) \circ S (g)$
34	33	cnveqd	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to {S (g \circ h)}^{-1} = {(S (h) \circ S (g))}^{-1}$
35	4 2	tendoi2	$⊢ (S \in E \land g \in T) \to I (S) (g) = {S (g)}^{-1}$
36	18 30 35	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to I (S) (g) = {S (g)}^{-1}$
37	4 2	tendoi2	$⊢ (S \in E \land h \in T) \to I (S) (h) = {S (h)}^{-1}$
38	18 29 37	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to I (S) (h) = {S (h)}^{-1}$
39	36 38	coeq12d	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to I (S) (g) \circ I (S) (h) = {S (g)}^{-1} \circ {S (h)}^{-1}$
40	23 34 39	3eqtr4a	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to {S (g \circ h)}^{-1} = I (S) (g) \circ I (S) (h)$
41	22 40	eqtrd	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T \land h \in T) \to I (S) (g \circ h) = I (S) (g) \circ I (S) (h)$
42	35	adantll	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to I (S) (g) = {S (g)}^{-1}$
43	42	fveq2d	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to trL (K) (W) (I (S) (g)) = trL (K) (W) ({S (g)}^{-1})$
44	1 2 6	trlcnv	$⊢ ((K \in HL \land W \in H) \land S (g) \in T) \to trL (K) (W) ({S (g)}^{-1}) = trL (K) (W) (S (g))$
45	8 10 44	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to trL (K) (W) ({S (g)}^{-1}) = trL (K) (W) (S (g))$
46	43 45	eqtrd	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to trL (K) (W) (I (S) (g)) = trL (K) (W) (S (g))$
47	5 1 2 6 3	tendotp	$⊢ ((K \in HL \land W \in H) \land S \in E \land g \in T) \to trL (K) (W) (S (g)) \leq_{K} trL (K) (W) (g)$
48	47	3expa	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to trL (K) (W) (S (g)) \leq_{K} trL (K) (W) (g)$
49	46 48	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to trL (K) (W) (I (S) (g)) \leq_{K} trL (K) (W) (g)$
50	5 1 2 6 3 7 17 41 49	istendod	$⊢ ((K \in HL \land W \in H) \land S \in E) \to I (S) \in E$

Metamath Proof Explorer

Theorem tendoicl

Proof