tendospcanN

Description: Cancellation law for trace-preserving endomorphism values (used as scalar product). (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	tendospcan.b	$⊢ B = {Base}_{K}$
	tendospcan.h	$⊢ H = LHyp (K)$
	tendospcan.t	$⊢ T = LTrn (K) (W)$
	tendospcan.e	$⊢ E = TEndo (K) (W)$
	tendospcan.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
Assertion	tendospcanN	$⊢ ((K \in HL \land W \in H) \land (S \in E \land S \neq O) \land (F \in T \land G \in T)) \to (S (F) = S (G) \leftrightarrow F = G)$

Proof

Step	Hyp	Ref	Expression
1		tendospcan.b	$⊢ B = {Base}_{K}$
2		tendospcan.h	$⊢ H = LHyp (K)$
3		tendospcan.t	$⊢ T = LTrn (K) (W)$
4		tendospcan.e	$⊢ E = TEndo (K) (W)$
5		tendospcan.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
6	2 3 4	tendocnv	$⊢ ((K \in HL \land W \in H) \land S \in E \land G \in T) \to {S (G)}^{-1} = S (G^{-1})$
7	6	3adant3l	$⊢ ((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \to {S (G)}^{-1} = S (G^{-1})$
8	7	coeq2d	$⊢ ((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \to S (F) \circ {S (G)}^{-1} = S (F) \circ S (G^{-1})$
9		simp1	$⊢ ((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \to (K \in HL \land W \in H)$
10		simp2	$⊢ ((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \to S \in E$
11		simp3l	$⊢ ((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \to F \in T$
12		simp3r	$⊢ ((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \to G \in T$
13	2 3	ltrncnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G^{-1} \in T$
14	9 12 13	syl2anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \to G^{-1} \in T$
15	2 3 4	tendospdi1	$⊢ ((K \in HL \land W \in H) \land (S \in E \land F \in T \land G^{-1} \in T)) \to S (F \circ G^{-1}) = S (F) \circ S (G^{-1})$
16	9 10 11 14 15	syl13anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \to S (F \circ G^{-1}) = S (F) \circ S (G^{-1})$
17	8 16	eqtr4d	$⊢ ((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \to S (F) \circ {S (G)}^{-1} = S (F \circ G^{-1})$
18	17	adantr	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to S (F) \circ {S (G)}^{-1} = S (F \circ G^{-1})$
19	18	eqeq1d	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to (S (F) \circ {S (G)}^{-1} = {I ↾}_{B} \leftrightarrow S (F \circ G^{-1}) = {I ↾}_{B})$
20		simpl1	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to (K \in HL \land W \in H)$
21		simpl2	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to S \in E$
22		simpl3l	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to F \in T$
23	2 3 4	tendocl	$⊢ ((K \in HL \land W \in H) \land S \in E \land F \in T) \to S (F) \in T$
24	20 21 22 23	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to S (F) \in T$
25		simpl3r	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to G \in T$
26	2 3 4	tendocl	$⊢ ((K \in HL \land W \in H) \land S \in E \land G \in T) \to S (G) \in T$
27	20 21 25 26	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to S (G) \in T$
28	1 2 3	ltrncoidN	$⊢ ((K \in HL \land W \in H) \land S (F) \in T \land S (G) \in T) \to (S (F) \circ {S (G)}^{-1} = {I ↾}_{B} \leftrightarrow S (F) = S (G))$
29	20 24 27 28	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to (S (F) \circ {S (G)}^{-1} = {I ↾}_{B} \leftrightarrow S (F) = S (G))$
30	20 25 13	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to G^{-1} \in T$
31	2 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G^{-1} \in T) \to F \circ G^{-1} \in T$
32	20 22 30 31	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to F \circ G^{-1} \in T$
33		simpr	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to F \circ G^{-1} \neq {I ↾}_{B}$
34	1 2 3 4 5	tendoid0	$⊢ ((K \in HL \land W \in H) \land S \in E \land (F \circ G^{-1} \in T \land F \circ G^{-1} \neq {I ↾}_{B})) \to (S (F \circ G^{-1}) = {I ↾}_{B} \leftrightarrow S = O)$
35	20 21 32 33 34	syl112anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to (S (F \circ G^{-1}) = {I ↾}_{B} \leftrightarrow S = O)$
36	19 29 35	3bitr3d	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to (S (F) = S (G) \leftrightarrow S = O)$
37	36	biimpd	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land F \circ G^{-1} \neq {I ↾}_{B}) \to (S (F) = S (G) \to S = O)$
38	37	impancom	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land S (F) = S (G)) \to (F \circ G^{-1} \neq {I ↾}_{B} \to S = O)$
39	38	necon1d	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land S (F) = S (G)) \to (S \neq O \to F \circ G^{-1} = {I ↾}_{B})$
40		simpl1	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land S (F) = S (G)) \to (K \in HL \land W \in H)$
41		simpl3l	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land S (F) = S (G)) \to F \in T$
42		simpl3r	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land S (F) = S (G)) \to G \in T$
43	1 2 3	ltrncoidN	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (F \circ G^{-1} = {I ↾}_{B} \leftrightarrow F = G)$
44	40 41 42 43	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land S (F) = S (G)) \to (F \circ G^{-1} = {I ↾}_{B} \leftrightarrow F = G)$
45	39 44	sylibd	$⊢ (((K \in HL \land W \in H) \land S \in E \land (F \in T \land G \in T)) \land S (F) = S (G)) \to (S \neq O \to F = G)$
46	45	3exp1	$⊢ (K \in HL \land W \in H) \to (S \in E \to ((F \in T \land G \in T) \to (S (F) = S (G) \to (S \neq O \to F = G))))$
47	46	com24	$⊢ (K \in HL \land W \in H) \to (S (F) = S (G) \to ((F \in T \land G \in T) \to (S \in E \to (S \neq O \to F = G))))$
48	47	imp5a	$⊢ (K \in HL \land W \in H) \to (S (F) = S (G) \to ((F \in T \land G \in T) \to ((S \in E \land S \neq O) \to F = G)))$
49	48	com24	$⊢ (K \in HL \land W \in H) \to ((S \in E \land S \neq O) \to ((F \in T \land G \in T) \to (S (F) = S (G) \to F = G)))$
50	49	3imp	$⊢ ((K \in HL \land W \in H) \land (S \in E \land S \neq O) \land (F \in T \land G \in T)) \to (S (F) = S (G) \to F = G)$
51		fveq2	$⊢ F = G \to S (F) = S (G)$
52	50 51	impbid1	$⊢ ((K \in HL \land W \in H) \land (S \in E \land S \neq O) \land (F \in T \land G \in T)) \to (S (F) = S (G) \leftrightarrow F = G)$

Metamath Proof Explorer

Theorem tendospcanN

Proof