Metamath Proof Explorer


Theorem lcfrlem18

Description: Lemma for lcfr . (Contributed by NM, 24-Feb-2015)

Ref Expression
Hypotheses lcfrlem17.h H = LHyp K
lcfrlem17.o ˙ = ocH K W
lcfrlem17.u U = DVecH K W
lcfrlem17.v V = Base U
lcfrlem17.p + ˙ = + U
lcfrlem17.z 0 ˙ = 0 U
lcfrlem17.n N = LSpan U
lcfrlem17.a A = LSAtoms U
lcfrlem17.k φ K HL W H
lcfrlem17.x φ X V 0 ˙
lcfrlem17.y φ Y V 0 ˙
lcfrlem17.ne φ N X N Y
Assertion lcfrlem18 φ ˙ X Y = ˙ X ˙ Y

Proof

Step Hyp Ref Expression
1 lcfrlem17.h H = LHyp K
2 lcfrlem17.o ˙ = ocH K W
3 lcfrlem17.u U = DVecH K W
4 lcfrlem17.v V = Base U
5 lcfrlem17.p + ˙ = + U
6 lcfrlem17.z 0 ˙ = 0 U
7 lcfrlem17.n N = LSpan U
8 lcfrlem17.a A = LSAtoms U
9 lcfrlem17.k φ K HL W H
10 lcfrlem17.x φ X V 0 ˙
11 lcfrlem17.y φ Y V 0 ˙
12 lcfrlem17.ne φ N X N Y
13 df-pr X Y = X Y
14 13 fveq2i ˙ X Y = ˙ X Y
15 10 eldifad φ X V
16 15 snssd φ X V
17 11 eldifad φ Y V
18 17 snssd φ Y V
19 1 3 4 2 dochdmj1 K HL W H X V Y V ˙ X Y = ˙ X ˙ Y
20 9 16 18 19 syl3anc φ ˙ X Y = ˙ X ˙ Y
21 14 20 syl5eq φ ˙ X Y = ˙ X ˙ Y