# Metamath Proof Explorer

## Theorem cdlemk8

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 26-Jun-2013)

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

### Proof

Step Hyp Ref Expression
1 cdlemk.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemk.l
3 cdlemk.j
4 cdlemk.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdlemk.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdlemk.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
7 cdlemk.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
8 cdlemk.m
9 coass ${⊢}\left({X}\circ {{G}}^{-1}\right)\circ {G}={X}\circ \left({{G}}^{-1}\circ {G}\right)$
10 simp1
11 simp2l
12 1 5 6 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\right)\to {G}:{B}\underset{1-1 onto}{⟶}{B}$
13 10 11 12 syl2anc
14 f1ococnv1 ${⊢}{G}:{B}\underset{1-1 onto}{⟶}{B}\to {{G}}^{-1}\circ {G}={\mathrm{I}↾}_{{B}}$
15 13 14 syl
16 15 coeq2d
17 simp2r
18 1 5 6 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {T}\right)\to {X}:{B}\underset{1-1 onto}{⟶}{B}$
19 10 17 18 syl2anc
20 f1of ${⊢}{X}:{B}\underset{1-1 onto}{⟶}{B}\to {X}:{B}⟶{B}$
21 fcoi1 ${⊢}{X}:{B}⟶{B}\to {X}\circ \left({\mathrm{I}↾}_{{B}}\right)={X}$
22 19 20 21 3syl
23 16 22 eqtrd
24 9 23 syl5eq
25 24 fveq1d
26 5 6 ltrncnv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\right)\to {{G}}^{-1}\in {T}$
27 10 11 26 syl2anc
28 5 6 ltrnco ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {T}\wedge {{G}}^{-1}\in {T}\right)\to {X}\circ {{G}}^{-1}\in {T}$
29 10 17 27 28 syl3anc
30 simp3l
31 2 4 5 6 ltrncoval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\circ {{G}}^{-1}\in {T}\wedge {G}\in {T}\right)\wedge {P}\in {A}\right)\to \left(\left({X}\circ {{G}}^{-1}\right)\circ {G}\right)\left({P}\right)=\left({X}\circ {{G}}^{-1}\right)\left({G}\left({P}\right)\right)$
32 10 29 11 30 31 syl121anc
33 25 32 eqtr3d
34 33 oveq2d
35 2 4 5 6 ltrnel