Metamath Proof Explorer

Theorem lcfrlem21

Description: Lemma for lcfr . (Contributed by NM, 11-Mar-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 lcfrlem21 
|- ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. A )

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 9 adantr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { ( X .+ Y ) } ) ) -> ( K e. HL /\ W e. H ) )
14 10 adantr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { ( X .+ Y ) } ) ) -> X e. ( V \ { .0. } ) )
15 11 adantr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { ( X .+ Y ) } ) ) -> Y e. ( V \ { .0. } ) )
16 12 adantr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { ( X .+ Y ) } ) ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
17 simpr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { ( X .+ Y ) } ) ) -> -. X e. ( ._|_ ` { ( X .+ Y ) } ) )
18 1 2 3 4 5 6 7 8 13 14 15 16 17 lcfrlem20 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { ( X .+ Y ) } ) ) -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. A )
19 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
20 10 eldifad 
 |-  ( ph -> X e. V )
21 11 eldifad 
 |-  ( ph -> Y e. V )
22 4 5 lmodcom 
 |-  ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) = ( Y .+ X ) )
23 19 20 21 22 syl3anc 
 |-  ( ph -> ( X .+ Y ) = ( Y .+ X ) )
24 23 sneqd 
 |-  ( ph -> { ( X .+ Y ) } = { ( Y .+ X ) } )
25 24 fveq2d 
 |-  ( ph -> ( ._|_ ` { ( X .+ Y ) } ) = ( ._|_ ` { ( Y .+ X ) } ) )
26 25 eleq2d 
 |-  ( ph -> ( Y e. ( ._|_ ` { ( X .+ Y ) } ) <-> Y e. ( ._|_ ` { ( Y .+ X ) } ) ) )
27 26 biimprd 
 |-  ( ph -> ( Y e. ( ._|_ ` { ( Y .+ X ) } ) -> Y e. ( ._|_ ` { ( X .+ Y ) } ) ) )
28 27 con3dimp 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { ( X .+ Y ) } ) ) -> -. Y e. ( ._|_ ` { ( Y .+ X ) } ) )
29 prcom 
 |-  { X , Y } = { Y , X }
30 29 fveq2i 
 |-  ( N ` { X , Y } ) = ( N ` { Y , X } )
31 30 a1i 
 |-  ( ph -> ( N ` { X , Y } ) = ( N ` { Y , X } ) )
32 31 25 ineq12d 
 |-  ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) = ( ( N ` { Y , X } ) i^i ( ._|_ ` { ( Y .+ X ) } ) ) )
33 32 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { ( Y .+ X ) } ) ) -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) = ( ( N ` { Y , X } ) i^i ( ._|_ ` { ( Y .+ X ) } ) ) )
34 9 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { ( Y .+ X ) } ) ) -> ( K e. HL /\ W e. H ) )
35 11 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { ( Y .+ X ) } ) ) -> Y e. ( V \ { .0. } ) )
36 10 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { ( Y .+ X ) } ) ) -> X e. ( V \ { .0. } ) )
37 12 necomd 
 |-  ( ph -> ( N ` { Y } ) =/= ( N ` { X } ) )
38 37 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { ( Y .+ X ) } ) ) -> ( N ` { Y } ) =/= ( N ` { X } ) )
39 simpr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { ( Y .+ X ) } ) ) -> -. Y e. ( ._|_ ` { ( Y .+ X ) } ) )
40 1 2 3 4 5 6 7 8 34 35 36 38 39 lcfrlem20 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { ( Y .+ X ) } ) ) -> ( ( N ` { Y , X } ) i^i ( ._|_ ` { ( Y .+ X ) } ) ) e. A )
41 33 40 eqeltrd 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { ( Y .+ X ) } ) ) -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. A )
42 28 41 syldan 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { ( X .+ Y ) } ) ) -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. A )
43 1 2 3 4 5 6 7 8 9 10 11 12 lcfrlem19 
 |-  ( ph -> ( -. X e. ( ._|_ ` { ( X .+ Y ) } ) \/ -. Y e. ( ._|_ ` { ( X .+ Y ) } ) ) )
44 18 42 43 mpjaodan 
 |-  ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. A )