ltrncoidN

Description: Two translations are equal if the composition of one with the converse of the other is the zero translation. This is an analogue of vector subtraction. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ltrn1o.b	$⊢ B = {Base}_{K}$
	ltrn1o.h	$⊢ H = LHyp (K)$
	ltrn1o.t	$⊢ T = LTrn (K) (W)$
Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		ltrn1o.b	$⊢ B = {Base}_{K}$
2		ltrn1o.h	$⊢ H = LHyp (K)$
3		ltrn1o.t	$⊢ T = LTrn (K) (W)$
4		simpl1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to (K \in HL \land W \in H)$
5		simpl3	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to G \in T$
6	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : B \underset{1-1 onto}{⟶} B$
7	4 5 6	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to G : B \underset{1-1 onto}{⟶} B$
8		f1ococnv1	$⊢ G : B \underset{1-1 onto}{⟶} B \to G^{-1} \circ G = {I ↾}_{B}$
9	7 8	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to G^{-1} \circ G = {I ↾}_{B}$
10	9	coeq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to F \circ (G^{-1} \circ G) = F \circ ({I ↾}_{B})$
11		simpl2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to F \in T$
12	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
13	4 11 12	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to F : B \underset{1-1 onto}{⟶} B$
14		f1of	$⊢ F : B \underset{1-1 onto}{⟶} B \to F : B ⟶ B$
15		fcoi1	$⊢ F : B ⟶ B \to F \circ ({I ↾}_{B}) = F$
16	13 14 15	3syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to F \circ ({I ↾}_{B}) = F$
17	10 16	eqtr2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to F = F \circ (G^{-1} \circ G)$
18		coass	$⊢ (F \circ G^{-1}) \circ G = F \circ (G^{-1} \circ G)$
19	17 18	eqtr4di	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to F = (F \circ G^{-1}) \circ G$
20		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to F \circ G^{-1} = {I ↾}_{B}$
21	20	coeq1d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to (F \circ G^{-1}) \circ G = ({I ↾}_{B}) \circ G$
22		f1of	$⊢ G : B \underset{1-1 onto}{⟶} B \to G : B ⟶ B$
23		fcoi2	$⊢ G : B ⟶ B \to ({I ↾}_{B}) \circ G = G$
24	7 22 23	3syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to ({I ↾}_{B}) \circ G = G$
25	21 24	eqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to (F \circ G^{-1}) \circ G = G$
26	19 25	eqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F \circ G^{-1} = {I ↾}_{B}) \to F = G$
27		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = G) \to F = G$
28	27	coeq1d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = G) \to F \circ G^{-1} = G \circ G^{-1}$
29		simpl1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = G) \to (K \in HL \land W \in H)$
30		simpl3	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = G) \to G \in T$
31	29 30 6	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = G) \to G : B \underset{1-1 onto}{⟶} B$
32		f1ococnv2	$⊢ G : B \underset{1-1 onto}{⟶} B \to G \circ G^{-1} = {I ↾}_{B}$
33	31 32	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = G) \to G \circ G^{-1} = {I ↾}_{B}$
34	28 33	eqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land F = G) \to F \circ G^{-1} = {I ↾}_{B}$
35	26 34	impbida	$⊢ ((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)$

Metamath Proof Explorer

Theorem ltrncoidN

Proof