Metamath Proof Explorer

Theorem trlcoat

Description: The trace of a composition of two translations is an atom if their traces are different. (Contributed by NM, 15-Jun-2013)

Ref Expression
Hypotheses trlcoat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
trlcoat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
trlcoat.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
trlcoat.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion trlcoat ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 trlcoat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 trlcoat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 trlcoat.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 trlcoat.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 2 3 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
6 5 3expb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
9 7 8 2 3 4 trlid0b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 0. ‘ 𝐾 ) ) )
10 6 9 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 0. ‘ 𝐾 ) ) )
11 coass ⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) )
12 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → 𝐹 ∈ 𝑇 )
14 7 2 3 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
15 12 13 14 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
16 f1ococnv1 ⊢ ( 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝐾 ) ) )
17 15 16 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝐾 ) ) )
18 17 coeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ 𝐺 ) )
19 coeq2 ⊢ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) = ( ◡ 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) )
20 19 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) = ( ◡ 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) )
21 11 18 20 3eqtr3a ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ 𝐺 ) = ( ◡ 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) )
22 simplrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → 𝐺 ∈ 𝑇 )
23 7 2 3 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
24 12 22 23 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
25 f1of ⊢ ( 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) )
26 fcoi2 ⊢ ( 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ 𝐺 ) = 𝐺 )
27 24 25 26 3syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ 𝐺 ) = 𝐺 )
28 2 3 ltrncnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ◡ 𝐹 ∈ 𝑇 )
29 12 13 28 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ◡ 𝐹 ∈ 𝑇 )
30 7 2 3 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ◡ 𝐹 ∈ 𝑇 ) → ◡ 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
31 12 29 30 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ◡ 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
32 f1of ⊢ ( ◡ 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → ◡ 𝐹 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) )
33 fcoi1 ⊢ ( ◡ 𝐹 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) → ( ◡ 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ◡ 𝐹 )
34 31 32 33 3syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ◡ 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ◡ 𝐹 )
35 21 27 34 3eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → 𝐺 = ◡ 𝐹 )
36 35 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ ◡ 𝐹 ) )
37 2 3 4 trlcnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) )
38 12 13 37 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ ◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) )
39 36 38 eqtr2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) )
40 39 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) )
41 10 40 sylbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 0. ‘ 𝐾 ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) )
42 41 necon3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ≠ ( 0. ‘ 𝐾 ) ) )
43 8 1 2 3 4 trlatn0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → ( ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ 𝐴 ↔ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ≠ ( 0. ‘ 𝐾 ) ) )
44 6 43 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ 𝐴 ↔ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ≠ ( 0. ‘ 𝐾 ) ) )
45 42 44 sylibrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ 𝐴 ) )
46 45 3impia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ 𝐴 )