lcfrlem34

	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 } ) )
	lcfrlem22.b	\|- B = ( ( N ` { X , Y } ) i^i ( ._\|_ ` { ( X .+ Y ) } ) )
	lcfrlem24.t	\|- .x. = ( .s ` U )
	lcfrlem24.s	\|- S = ( Scalar ` U )
	lcfrlem24.q	\|- Q = ( 0g ` S )
	lcfrlem24.r	\|- R = ( Base ` S )
	lcfrlem24.j	\|- J = ( x e. ( V \ { .0. } ) \|-> ( v e. V \|-> ( iota_ k e. R E. w e. ( ._\|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
	lcfrlem24.ib	\|- ( ph -> I e. B )
	lcfrlem24.l	\|- L = ( LKer ` U )
	lcfrlem25.d	\|- D = ( LDual ` U )
	lcfrlem28.jn	\|- ( ph -> ( ( J ` Y ) ` I ) =/= Q )
	lcfrlem29.i	\|- F = ( invr ` S )
	lcfrlem30.m	\|- .- = ( -g ` D )
	lcfrlem30.c	\|- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )
Assertion	lcfrlem34	\|- ( ph -> C =/= ( 0g ` D ) )

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		lcfrlem22.b	\|- B = ( ( N ` { X , Y } ) i^i ( ._\|_ ` { ( X .+ Y ) } ) )
14		lcfrlem24.t	\|- .x. = ( .s ` U )
15		lcfrlem24.s	\|- S = ( Scalar ` U )
16		lcfrlem24.q	\|- Q = ( 0g ` S )
17		lcfrlem24.r	\|- R = ( Base ` S )
18		lcfrlem24.j	\|- J = ( x e. ( V \ { .0. } ) \|-> ( v e. V \|-> ( iota_ k e. R E. w e. ( ._\|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
19		lcfrlem24.ib	\|- ( ph -> I e. B )
20		lcfrlem24.l	\|- L = ( LKer ` U )
21		lcfrlem25.d	\|- D = ( LDual ` U )
22		lcfrlem28.jn	\|- ( ph -> ( ( J ` Y ) ` I ) =/= Q )
23		lcfrlem29.i	\|- F = ( invr ` S )
24		lcfrlem30.m	\|- .- = ( -g ` D )
25		lcfrlem30.c	\|- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )
26	9	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) = Q ) -> ( K e. HL /\ W e. H ) )
27	10	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) = Q ) -> X e. ( V \ { .0. } ) )
28	11	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) = Q ) -> Y e. ( V \ { .0. } ) )
29	12	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) = Q ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
30	19	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) = Q ) -> I e. B )
31	22	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) = Q ) -> ( ( J ` Y ) ` I ) =/= Q )
32		simpr	\|- ( ( ph /\ ( ( J ` X ) ` I ) = Q ) -> ( ( J ` X ) ` I ) = Q )
33	1 2 3 4 5 6 7 8 26 27 28 29 13 14 15 16 17 18 30 20 21 31 23 24 25 32	lcfrlem33	\|- ( ( ph /\ ( ( J ` X ) ` I ) = Q ) -> C =/= ( 0g ` D ) )
34	9	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) =/= Q ) -> ( K e. HL /\ W e. H ) )
35	10	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) =/= Q ) -> X e. ( V \ { .0. } ) )
36	11	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) =/= Q ) -> Y e. ( V \ { .0. } ) )
37	12	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) =/= Q ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
38	19	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) =/= Q ) -> I e. B )
39	22	adantr	\|- ( ( ph /\ ( ( J ` X ) ` I ) =/= Q ) -> ( ( J ` Y ) ` I ) =/= Q )
40		simpr	\|- ( ( ph /\ ( ( J ` X ) ` I ) =/= Q ) -> ( ( J ` X ) ` I ) =/= Q )
41	1 2 3 4 5 6 7 8 34 35 36 37 13 14 15 16 17 18 38 20 21 39 23 24 25 40	lcfrlem32	\|- ( ( ph /\ ( ( J ` X ) ` I ) =/= Q ) -> C =/= ( 0g ` D ) )
42	33 41	pm2.61dane	\|- ( ph -> C =/= ( 0g ` D ) )

Metamath Proof Explorer

Theorem lcfrlem34

Proof