Metamath Proof Explorer


Theorem cdleme50rnlem

Description: Part of proof of Lemma D in Crawley p. 113. TODO: fix comment. TODO: can we get rid of G stuff if we show G =`' F ` earlier? (Contributed by NM, 9-Apr-2013)

Ref Expression
Hypotheses cdlemef50.b B = Base K
cdlemef50.l ˙ = K
cdlemef50.j ˙ = join K
cdlemef50.m ˙ = meet K
cdlemef50.a A = Atoms K
cdlemef50.h H = LHyp K
cdlemef50.u U = P ˙ Q ˙ W
cdlemef50.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemefs50.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemef50.f F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
cdlemef50.v V = Q ˙ P ˙ W
cdlemef50.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
cdlemefs50.o O = Q ˙ P ˙ N ˙ u ˙ v ˙ W
cdlemef50.g G = a B if Q P ¬ a ˙ W ι c B | u A ¬ u ˙ W u ˙ a ˙ W = a c = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N ˙ a ˙ W a
Assertion cdleme50rnlem K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W ran F = B

Proof

Step Hyp Ref Expression
1 cdlemef50.b B = Base K
2 cdlemef50.l ˙ = K
3 cdlemef50.j ˙ = join K
4 cdlemef50.m ˙ = meet K
5 cdlemef50.a A = Atoms K
6 cdlemef50.h H = LHyp K
7 cdlemef50.u U = P ˙ Q ˙ W
8 cdlemef50.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemefs50.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemef50.f F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
11 cdlemef50.v V = Q ˙ P ˙ W
12 cdlemef50.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
13 cdlemefs50.o O = Q ˙ P ˙ N ˙ u ˙ v ˙ W
14 cdlemef50.g G = a B if Q P ¬ a ˙ W ι c B | u A ¬ u ˙ W u ˙ a ˙ W = a c = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N ˙ a ˙ W a
15 1 2 3 4 5 6 7 8 9 10 cdleme50f K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F : B B
16 15 frnd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W ran F B
17 1 2 3 4 5 6 11 12 13 14 cdlemeg46fvcl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W e B G e B
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme48fgv K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W e B F G e = e
19 fveqeq2 d = G e F d = e F G e = e
20 19 rspcev G e B F G e = e d B F d = e
21 17 18 20 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W e B d B F d = e
22 15 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W e B F : B B
23 ffn F : B B F Fn B
24 fvelrnb F Fn B e ran F d B F d = e
25 22 23 24 3syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W e B e ran F d B F d = e
26 21 25 mpbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W e B e ran F
27 16 26 eqelssd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W ran F = B