Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
ltrn1o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
ltrn1o.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrncoidN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ↔ 𝐹 = 𝐺 ) )

Proof

Step Hyp Ref Expression
1 ltrn1o.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ltrn1o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 ltrn1o.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐺 ∈ 𝑇 )
6 1 2 3 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 )
7 4 5 6 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 )
8 f1ococnv1 ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 → ( ◡ 𝐺 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
9 7 8 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → ( ◡ 𝐺 ∘ 𝐺 ) = ( I ↾ 𝐵 ) )
10 9 coeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → ( 𝐹 ∘ ( ◡ 𝐺 ∘ 𝐺 ) ) = ( 𝐹 ∘ ( I ↾ 𝐵 ) ) )
11 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐹 ∈ 𝑇 )
12 1 2 3 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
13 4 11 12 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
14 f1of ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → 𝐹 : 𝐵 ⟶ 𝐵 )
15 fcoi1 ⊢ ( 𝐹 : 𝐵 ⟶ 𝐵 → ( 𝐹 ∘ ( I ↾ 𝐵 ) ) = 𝐹 )
16 13 14 15 3syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → ( 𝐹 ∘ ( I ↾ 𝐵 ) ) = 𝐹 )
17 10 16 eqtr2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐹 = ( 𝐹 ∘ ( ◡ 𝐺 ∘ 𝐺 ) ) )
18 coass ⊢ ( ( 𝐹 ∘ ◡ 𝐺 ) ∘ 𝐺 ) = ( 𝐹 ∘ ( ◡ 𝐺 ∘ 𝐺 ) )
19 17 18 eqtr4di ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐹 = ( ( 𝐹 ∘ ◡ 𝐺 ) ∘ 𝐺 ) )
20 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) )
21 20 coeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → ( ( 𝐹 ∘ ◡ 𝐺 ) ∘ 𝐺 ) = ( ( I ↾ 𝐵 ) ∘ 𝐺 ) )
22 f1of ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 → 𝐺 : 𝐵 ⟶ 𝐵 )
23 fcoi2 ⊢ ( 𝐺 : 𝐵 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ 𝐺 ) = 𝐺 )
24 7 22 23 3syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ∘ 𝐺 ) = 𝐺 )
25 21 24 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → ( ( 𝐹 ∘ ◡ 𝐺 ) ∘ 𝐺 ) = 𝐺 )
26 19 25 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) → 𝐹 = 𝐺 )
27 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = 𝐺 ) → 𝐹 = 𝐺 )
28 27 coeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = 𝐺 ) → ( 𝐹 ∘ ◡ 𝐺 ) = ( 𝐺 ∘ ◡ 𝐺 ) )
29 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = 𝐺 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
30 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = 𝐺 ) → 𝐺 ∈ 𝑇 )
31 29 30 6 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = 𝐺 ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 )
32 f1ococnv2 ⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 → ( 𝐺 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) )
33 31 32 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = 𝐺 ) → ( 𝐺 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) )
34 28 33 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = 𝐺 ) → ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) )
35 26 34 impbida ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ↔ 𝐹 = 𝐺 ) )