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
|- .+ = ( +g ` U )
lcfrlem17.z
|- .0. = ( 0g ` U )
lcfrlem17.n
|- N = ( LSpan ` U )
lcfrlem17.a
|- A = ( LSAtoms ` U )
lcfrlem17.k
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfrlem17.x
|- ( ph -> X e. ( V \ { .0. } ) )
lcfrlem17.y
|- ( ph -> Y e. ( V \ { .0. } ) )
lcfrlem17.ne
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
Assertion lcfrlem18
|- ( ph -> ( ._|_ ` { X , Y } ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { 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
 |-  .+ = ( +g ` U )
6 lcfrlem17.z
 |-  .0. = ( 0g ` U )
7 lcfrlem17.n
 |-  N = ( LSpan ` U )
8 lcfrlem17.a
 |-  A = ( LSAtoms ` U )
9 lcfrlem17.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lcfrlem17.x
 |-  ( ph -> X e. ( V \ { .0. } ) )
11 lcfrlem17.y
 |-  ( ph -> Y e. ( V \ { .0. } ) )
12 lcfrlem17.ne
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
13 df-pr
 |-  { X , Y } = ( { X } u. { Y } )
14 13 fveq2i
 |-  ( ._|_ ` { X , Y } ) = ( ._|_ ` ( { X } u. { Y } ) )
15 10 eldifad
 |-  ( ph -> X e. V )
16 15 snssd
 |-  ( ph -> { X } C_ V )
17 11 eldifad
 |-  ( ph -> Y e. V )
18 17 snssd
 |-  ( ph -> { Y } C_ V )
19 1 3 4 2 dochdmj1
 |-  ( ( ( K e. HL /\ W e. H ) /\ { X } C_ V /\ { Y } C_ V ) -> ( ._|_ ` ( { X } u. { Y } ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
20 9 16 18 19 syl3anc
 |-  ( ph -> ( ._|_ ` ( { X } u. { Y } ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
21 14 20 syl5eq
 |-  ( ph -> ( ._|_ ` { X , Y } ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )