Metamath Proof Explorer

Theorem cdlemj2

Description: Part of proof of Lemma J of Crawley p. 118. Eliminate p . (Contributed by NM, 20-Jun-2013)

Ref Expression
Hypotheses cdlemj.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemj.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemj.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemj.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemj.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
Assertion cdlemj2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to {U}\left({h}\right)={V}\left({h}\right)$

Proof

Step Hyp Ref Expression
1 cdlemj.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemj.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 cdlemj.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 cdlemj.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
5 cdlemj.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
6 simpl1 ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to \left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)$
7 simpl2 ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)$
8 simpl3l ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {R}\left({F}\right)\ne {R}\left({g}\right)$
9 simpl3r ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {R}\left({g}\right)\ne {R}\left({h}\right)$
10 simpr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)$
11 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
12 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
13 1 2 3 4 5 11 12 cdlemj1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\right)\to {U}\left({h}\right)\left({p}\right)={V}\left({h}\right)\left({p}\right)$
14 6 7 8 9 10 13 syl113anc ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {U}\left({h}\right)\left({p}\right)={V}\left({h}\right)\left({p}\right)$
15 14 exp32 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to \left({p}\in \mathrm{Atoms}\left({K}\right)\to \left(¬{p}{\le }_{{K}}{W}\to {U}\left({h}\right)\left({p}\right)={V}\left({h}\right)\left({p}\right)\right)\right)$
16 15 ralrimiv ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to \forall {p}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(¬{p}{\le }_{{K}}{W}\to {U}\left({h}\right)\left({p}\right)={V}\left({h}\right)\left({p}\right)\right)$
17 simp11 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
18 simp121 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to {U}\in {E}$
19 simp133 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to {h}\in {T}$
20 2 3 5 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\wedge {h}\in {T}\right)\to {U}\left({h}\right)\in {T}$
21 17 18 19 20 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to {U}\left({h}\right)\in {T}$
22 simp122 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to {V}\in {E}$
23 2 3 5 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {V}\in {E}\wedge {h}\in {T}\right)\to {V}\left({h}\right)\in {T}$
24 17 22 19 23 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to {V}\left({h}\right)\in {T}$
25 11 12 2 3 ltrneq ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\left({h}\right)\in {T}\wedge {V}\left({h}\right)\in {T}\right)\to \left(\forall {p}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(¬{p}{\le }_{{K}}{W}\to {U}\left({h}\right)\left({p}\right)={V}\left({h}\right)\left({p}\right)\right)↔{U}\left({h}\right)={V}\left({h}\right)\right)$
26 17 21 24 25 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to \left(\forall {p}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(¬{p}{\le }_{{K}}{W}\to {U}\left({h}\right)\left({p}\right)={V}\left({h}\right)\left({p}\right)\right)↔{U}\left({h}\right)={V}\left({h}\right)\right)$
27 16 26 mpbid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to {U}\left({h}\right)={V}\left({h}\right)$