# Metamath Proof Explorer

## Theorem cdlemn9

Description: Part of proof of Lemma N of Crawley p. 121 line 36. (Contributed by NM, 27-Feb-2014)

Ref Expression
Hypotheses cdlemn8.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemn8.l
cdlemn8.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemn8.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemn8.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
cdlemn8.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
cdlemn8.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemn8.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
cdlemn8.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
cdlemn8.s
cdlemn8.f ${⊢}{F}=\left(\iota {h}\in {T}|{h}\left({P}\right)={Q}\right)$
cdlemn8.g ${⊢}{G}=\left(\iota {h}\in {T}|{h}\left({P}\right)={R}\right)$
Assertion cdlemn9

### Proof

Step Hyp Ref Expression
1 cdlemn8.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemn8.l
3 cdlemn8.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 cdlemn8.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
5 cdlemn8.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
6 cdlemn8.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
7 cdlemn8.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 cdlemn8.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
9 cdlemn8.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
10 cdlemn8.s
11 cdlemn8.f ${⊢}{F}=\left(\iota {h}\in {T}|{h}\left({P}\right)={Q}\right)$
12 cdlemn8.g ${⊢}{G}=\left(\iota {h}\in {T}|{h}\left({P}\right)={R}\right)$
13 1 2 3 4 5 6 7 8 9 10 11 12 cdlemn8
14 13 fveq1d
15 simp1
16 2 3 4 5 lhpocnel2
18 simp2l
19 2 3 4 7 11 ltrniotacl
20 15 17 18 19 syl3anc
21 1 4 7 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {F}:{B}\underset{1-1 onto}{⟶}{B}$
22 15 20 21 syl2anc
23 f1ocnv ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{B}\underset{1-1 onto}{⟶}{B}$
24 f1of ${⊢}{{F}}^{-1}:{B}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{B}⟶{B}$
25 22 23 24 3syl
26 simp2ll
27 1 3 atbase ${⊢}{Q}\in {A}\to {Q}\in {B}$
28 26 27 syl
29 fvco3 ${⊢}\left({{F}}^{-1}:{B}⟶{B}\wedge {Q}\in {B}\right)\to \left({G}\circ {{F}}^{-1}\right)\left({Q}\right)={G}\left({{F}}^{-1}\left({Q}\right)\right)$
30 25 28 29 syl2anc
31 2 3 4 7 11 ltrniotacnvval
32 15 17 18 31 syl3anc
33 32 fveq2d
34 simp2r
35 2 3 4 7 12 ltrniotaval
36 15 17 34 35 syl3anc
37 33 36 eqtrd
38 14 30 37 3eqtrd