Metamath Proof Explorer


Theorem cdleme31snd

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 1-Apr-2013)

Ref Expression
Hypotheses cdleme31snd.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme31snd.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
cdleme31snd.e E = O ˙ U ˙ Q ˙ P ˙ O ˙ W
cdleme31snd.o O = S ˙ V ˙ P ˙ Q ˙ S ˙ W
Assertion cdleme31snd S A S / v N / t D = E

Proof

Step Hyp Ref Expression
1 cdleme31snd.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
2 cdleme31snd.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
3 cdleme31snd.e E = O ˙ U ˙ Q ˙ P ˙ O ˙ W
4 cdleme31snd.o O = S ˙ V ˙ P ˙ Q ˙ S ˙ W
5 csbnestgw S A S / v N / t D = S / v N / t D
6 2 4 cdleme31sc S A S / v N = O
7 6 csbeq1d S A S / v N / t D = O / t D
8 4 ovexi O V
9 1 3 cdleme31sc O V O / t D = E
10 8 9 ax-mp O / t D = E
11 7 10 eqtrdi S A S / v N / t D = E
12 5 11 eqtrd S A S / v N / t D = E