# Metamath Proof Explorer

## Theorem cdlemkfid1N

Description: Lemma for cdlemkfid3N . (Contributed by NM, 29-Jul-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemk5.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemk5.l
cdlemk5.j
cdlemk5.m
cdlemk5.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemk5.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemk5.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemk5.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
Assertion cdlemkfid1N

### Proof

Step Hyp Ref Expression
1 cdlemk5.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemk5.l
3 cdlemk5.j
4 cdlemk5.m
5 cdlemk5.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdlemk5.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdlemk5.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 cdlemk5.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
9 simp1
10 simp23
11 simp3r
12 2 3 5 6 7 8 trljat3
13 9 10 11 12 syl3anc
14 simp1l
15 simp21
16 simp3rl
17 2 5 6 7 ltrnat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {P}\in {A}\right)\to {F}\left({P}\right)\in {A}$
18 9 15 16 17 syl3anc
19 2 5 6 7 ltrnat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\wedge {P}\in {A}\right)\to {G}\left({P}\right)\in {A}$
20 9 10 16 19 syl3anc
21 3 5 hlatjcom
22 14 18 20 21 syl3anc
23 2 3 5 6 7 8 trlcoabs2N
24 9 15 10 11 23 syl121anc
25 6 7 8 trlcocnv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to {R}\left({F}\circ {{G}}^{-1}\right)={R}\left({G}\circ {{F}}^{-1}\right)$
26 9 15 10 25 syl3anc
27 26 oveq2d
28 2 3 5 6 7 8 trlcoabs2N
29 9 10 15 11 28 syl121anc
30 27 29 eqtr3d
31 22 24 30 3eqtr4d
32 13 31 oveq12d
33 1 6 7 8 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\right)\to {R}\left({G}\right)\in {B}$
34 9 10 33 syl2anc
35 simp1r
36 simp3l
37 5 6 7 8 trlcocnvat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({G}\in {T}\wedge {F}\in {T}\right)\wedge {R}\left({G}\right)\ne {R}\left({F}\right)\right)\to {R}\left({G}\circ {{F}}^{-1}\right)\in {A}$
38 14 35 10 15 36 37 syl221anc
39 2 5 6 7 ltrnel
40 9 10 11 39 syl3anc
41 6 7 ltrncnv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {{F}}^{-1}\in {T}$
42 9 15 41 syl2anc
43 6 7 8 trlcnv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {R}\left({{F}}^{-1}\right)={R}\left({F}\right)$
44 9 15 43 syl2anc
45 36 44 neeqtrrd
46 simp22
47 1 6 7 ltrncnvnid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\to {{F}}^{-1}\ne {\mathrm{I}↾}_{{B}}$
48 9 15 46 47 syl3anc
49 1 6 7 8 trlcone ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({G}\in {T}\wedge {{F}}^{-1}\in {T}\right)\wedge \left({R}\left({G}\right)\ne {R}\left({{F}}^{-1}\right)\wedge {{F}}^{-1}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {R}\left({G}\right)\ne {R}\left({G}\circ {{F}}^{-1}\right)$
50 9 10 42 45 48 49 syl122anc
51 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
52 51 5 6 7 8 trlator0 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\right)\to \left({R}\left({G}\right)\in {A}\vee {R}\left({G}\right)=\mathrm{0.}\left({K}\right)\right)$
53 9 10 52 syl2anc
54 2 6 7 8 trlle
55 14 35 10 54 syl21anc
56 6 7 ltrnco ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\wedge {{F}}^{-1}\in {T}\right)\to {G}\circ {{F}}^{-1}\in {T}$
57 9 10 42 56 syl3anc
58 2 6 7 8 trlle
59 9 57 58 syl2anc
60 2 3 51 5 6 lhp2at0nle
61 9 40 50 53 55 38 59 60 syl322anc
62 1 2 3 4 5 2llnma1b
63 14 34 20 38 61 62 syl131anc
64 32 63 eqtrd