# Metamath Proof Explorer

## Theorem ltrniotacl

Description: Version of cdleme50ltrn with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 17-Apr-2013)

Ref Expression
Hypotheses ltrniotaval.l
ltrniotaval.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
ltrniotaval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
ltrniotaval.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
ltrniotaval.f ${⊢}{F}=\left(\iota {f}\in {T}|{f}\left({P}\right)={Q}\right)$
Assertion ltrniotacl

### Proof

Step Hyp Ref Expression
1 ltrniotaval.l
2 ltrniotaval.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 ltrniotaval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 ltrniotaval.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
5 ltrniotaval.f ${⊢}{F}=\left(\iota {f}\in {T}|{f}\left({P}\right)={Q}\right)$
6 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
7 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
8 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
9 eqid ${⊢}\left({P}\mathrm{join}\left({K}\right){Q}\right)\mathrm{meet}\left({K}\right){W}=\left({P}\mathrm{join}\left({K}\right){Q}\right)\mathrm{meet}\left({K}\right){W}$
10 eqid ${⊢}\left({t}\mathrm{join}\left({K}\right)\left(\left({P}\mathrm{join}\left({K}\right){Q}\right)\mathrm{meet}\left({K}\right){W}\right)\right)\mathrm{meet}\left({K}\right)\left({Q}\mathrm{join}\left({K}\right)\left(\left({P}\mathrm{join}\left({K}\right){t}\right)\mathrm{meet}\left({K}\right){W}\right)\right)=\left({t}\mathrm{join}\left({K}\right)\left(\left({P}\mathrm{join}\left({K}\right){Q}\right)\mathrm{meet}\left({K}\right){W}\right)\right)\mathrm{meet}\left({K}\right)\left({Q}\mathrm{join}\left({K}\right)\left(\left({P}\mathrm{join}\left({K}\right){t}\right)\mathrm{meet}\left({K}\right){W}\right)\right)$
11 eqid ${⊢}\left({P}\mathrm{join}\left({K}\right){Q}\right)\mathrm{meet}\left({K}\right)\left(\left(\left({t}\mathrm{join}\left({K}\right)\left(\left({P}\mathrm{join}\left({K}\right){Q}\right)\mathrm{meet}\left({K}\right){W}\right)\right)\mathrm{meet}\left({K}\right)\left({Q}\mathrm{join}\left({K}\right)\left(\left({P}\mathrm{join}\left({K}\right){t}\right)\mathrm{meet}\left({K}\right){W}\right)\right)\right)\mathrm{join}\left({K}\right)\left(\left({s}\mathrm{join}\left({K}\right){t}\right)\mathrm{meet}\left({K}\right){W}\right)\right)=\left({P}\mathrm{join}\left({K}\right){Q}\right)\mathrm{meet}\left({K}\right)\left(\left(\left({t}\mathrm{join}\left({K}\right)\left(\left({P}\mathrm{join}\left({K}\right){Q}\right)\mathrm{meet}\left({K}\right){W}\right)\right)\mathrm{meet}\left({K}\right)\left({Q}\mathrm{join}\left({K}\right)\left(\left({P}\mathrm{join}\left({K}\right){t}\right)\mathrm{meet}\left({K}\right){W}\right)\right)\right)\mathrm{join}\left({K}\right)\left(\left({s}\mathrm{join}\left({K}\right){t}\right)\mathrm{meet}\left({K}\right){W}\right)\right)$
12 eqid
13 6 1 7 8 2 3 9 10 11 12 4 5 cdlemg1ltrnlem