Metamath Proof Explorer

Theorem islshpat

Description: Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm . (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses islshpat.v 
|- V = ( Base ` W )
islshpat.s 
|- S = ( LSubSp ` W )
islshpat.p 
|- .(+) = ( LSSum ` W )
islshpat.h 
|- H = ( LSHyp ` W )
islshpat.a 
|- A = ( LSAtoms ` W )
islshpat.w 
|- ( ph -> W e. LMod )
Assertion islshpat 
|- ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. q e. A ( U .(+) q ) = V ) ) )

Proof

Step Hyp Ref Expression
1 islshpat.v 
 |-  V = ( Base ` W )
2 islshpat.s 
 |-  S = ( LSubSp ` W )
3 islshpat.p 
 |-  .(+) = ( LSSum ` W )
4 islshpat.h 
 |-  H = ( LSHyp ` W )
5 islshpat.a 
 |-  A = ( LSAtoms ` W )
6 islshpat.w 
 |-  ( ph -> W e. LMod )
7 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
8 1 7 2 3 4 6 islshpsm 
 |-  ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
9 df-3an 
 |-  ( ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> ( ( U e. S /\ U =/= V ) /\ E. v e. V ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) )
10 r19.42v 
 |-  ( E. v e. V ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> ( ( U e. S /\ U =/= V ) /\ E. v e. V ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) )
11 9 10 bitr4i 
 |-  ( ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> E. v e. V ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) )
12 df-rex 
 |-  ( E. v e. V ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> E. v ( v e. V /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
13 simpr 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> v = ( 0g ` W ) )
14 13 sneqd 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> { v } = { ( 0g ` W ) } )
15 14 fveq2d 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> ( ( LSpan ` W ) ` { v } ) = ( ( LSpan ` W ) ` { ( 0g ` W ) } ) )
16 6 ad3antrrr 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> W e. LMod )
17 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
18 17 7 lspsn0 
 |-  ( W e. LMod -> ( ( LSpan ` W ) ` { ( 0g ` W ) } ) = { ( 0g ` W ) } )
19 16 18 syl 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> ( ( LSpan ` W ) ` { ( 0g ` W ) } ) = { ( 0g ` W ) } )
20 15 19 eqtrd 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> ( ( LSpan ` W ) ` { v } ) = { ( 0g ` W ) } )
21 20 oveq2d 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = ( U .(+) { ( 0g ` W ) } ) )
22 simplrl 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> U e. S )
23 2 lsssubg 
 |-  ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )
24 16 22 23 syl2anc 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> U e. ( SubGrp ` W ) )
25 17 3 lsm01 
 |-  ( U e. ( SubGrp ` W ) -> ( U .(+) { ( 0g ` W ) } ) = U )
26 24 25 syl 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> ( U .(+) { ( 0g ` W ) } ) = U )
27 21 26 eqtrd 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = U )
28 simplrr 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> U =/= V )
29 27 28 eqnetrd 
 |-  ( ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) /\ v = ( 0g ` W ) ) -> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) =/= V )
30 29 ex 
 |-  ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) -> ( v = ( 0g ` W ) -> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) =/= V ) )
31 30 necon2d 
 |-  ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) -> ( ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V -> v =/= ( 0g ` W ) ) )
32 31 pm4.71rd 
 |-  ( ( ( ph /\ v e. V ) /\ ( U e. S /\ U =/= V ) ) -> ( ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V <-> ( v =/= ( 0g ` W ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
33 32 pm5.32da 
 |-  ( ( ph /\ v e. V ) -> ( ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> ( ( U e. S /\ U =/= V ) /\ ( v =/= ( 0g ` W ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) )
34 33 pm5.32da 
 |-  ( ph -> ( ( v e. V /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) <-> ( v e. V /\ ( ( U e. S /\ U =/= V ) /\ ( v =/= ( 0g ` W ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) ) )
35 eldifsn 
 |-  ( v e. ( V \ { ( 0g ` W ) } ) <-> ( v e. V /\ v =/= ( 0g ` W ) ) )
36 35 anbi1i 
 |-  ( ( v e. ( V \ { ( 0g ` W ) } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) <-> ( ( v e. V /\ v =/= ( 0g ` W ) ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
37 anass 
 |-  ( ( ( v e. V /\ v =/= ( 0g ` W ) ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) <-> ( v e. V /\ ( v =/= ( 0g ` W ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) )
38 an12 
 |-  ( ( v =/= ( 0g ` W ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) <-> ( ( U e. S /\ U =/= V ) /\ ( v =/= ( 0g ` W ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
39 38 anbi2i 
 |-  ( ( v e. V /\ ( v =/= ( 0g ` W ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) <-> ( v e. V /\ ( ( U e. S /\ U =/= V ) /\ ( v =/= ( 0g ` W ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) )
40 37 39 bitri 
 |-  ( ( ( v e. V /\ v =/= ( 0g ` W ) ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) <-> ( v e. V /\ ( ( U e. S /\ U =/= V ) /\ ( v =/= ( 0g ` W ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) )
41 36 40 bitr2i 
 |-  ( ( v e. V /\ ( ( U e. S /\ U =/= V ) /\ ( v =/= ( 0g ` W ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) <-> ( v e. ( V \ { ( 0g ` W ) } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
42 34 41 bitrdi 
 |-  ( ph -> ( ( v e. V /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) <-> ( v e. ( V \ { ( 0g ` W ) } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) )
43 42 exbidv 
 |-  ( ph -> ( E. v ( v e. V /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) <-> E. v ( v e. ( V \ { ( 0g ` W ) } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) )
44 12 43 syl5bb 
 |-  ( ph -> ( E. v e. V ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> E. v ( v e. ( V \ { ( 0g ` W ) } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) )
45 fvex 
 |-  ( ( LSpan ` W ) ` { v } ) e. _V
46 45 rexcom4b 
 |-  ( E. q E. v e. ( V \ { ( 0g ` W ) } ) ( ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) /\ q = ( ( LSpan ` W ) ` { v } ) ) <-> E. v e. ( V \ { ( 0g ` W ) } ) ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) )
47 df-rex 
 |-  ( E. v e. ( V \ { ( 0g ` W ) } ) ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> E. v ( v e. ( V \ { ( 0g ` W ) } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
48 46 47 bitr2i 
 |-  ( E. v ( v e. ( V \ { ( 0g ` W ) } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) <-> E. q E. v e. ( V \ { ( 0g ` W ) } ) ( ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) /\ q = ( ( LSpan ` W ) ` { v } ) ) )
49 ancom 
 |-  ( ( ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) /\ q = ( ( LSpan ` W ) ` { v } ) ) <-> ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
50 49 rexbii 
 |-  ( E. v e. ( V \ { ( 0g ` W ) } ) ( ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) /\ q = ( ( LSpan ` W ) ` { v } ) ) <-> E. v e. ( V \ { ( 0g ` W ) } ) ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
51 50 exbii 
 |-  ( E. q E. v e. ( V \ { ( 0g ` W ) } ) ( ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) /\ q = ( ( LSpan ` W ) ` { v } ) ) <-> E. q E. v e. ( V \ { ( 0g ` W ) } ) ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
52 48 51 bitri 
 |-  ( E. v ( v e. ( V \ { ( 0g ` W ) } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) <-> E. q E. v e. ( V \ { ( 0g ` W ) } ) ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
53 44 52 bitrdi 
 |-  ( ph -> ( E. v e. V ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> E. q E. v e. ( V \ { ( 0g ` W ) } ) ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) ) )
54 r19.41v 
 |-  ( E. v e. ( V \ { ( 0g ` W ) } ) ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) <-> ( E. v e. ( V \ { ( 0g ` W ) } ) q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) )
55 oveq2 
 |-  ( q = ( ( LSpan ` W ) ` { v } ) -> ( U .(+) q ) = ( U .(+) ( ( LSpan ` W ) ` { v } ) ) )
56 55 eqeq1d 
 |-  ( q = ( ( LSpan ` W ) ` { v } ) -> ( ( U .(+) q ) = V <-> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) )
57 56 anbi2d 
 |-  ( q = ( ( LSpan ` W ) ` { v } ) -> ( ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) <-> ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
58 57 pm5.32i 
 |-  ( ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) <-> ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
59 58 rexbii 
 |-  ( E. v e. ( V \ { ( 0g ` W ) } ) ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) <-> E. v e. ( V \ { ( 0g ` W ) } ) ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
60 54 59 bitr3i 
 |-  ( ( E. v e. ( V \ { ( 0g ` W ) } ) q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) <-> E. v e. ( V \ { ( 0g ` W ) } ) ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
61 60 exbii 
 |-  ( E. q ( E. v e. ( V \ { ( 0g ` W ) } ) q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) <-> E. q E. v e. ( V \ { ( 0g ` W ) } ) ( q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
62 53 61 bitr4di 
 |-  ( ph -> ( E. v e. V ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> E. q ( E. v e. ( V \ { ( 0g ` W ) } ) q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) ) )
63 1 7 17 5 islsat 
 |-  ( W e. LMod -> ( q e. A <-> E. v e. ( V \ { ( 0g ` W ) } ) q = ( ( LSpan ` W ) ` { v } ) ) )
64 6 63 syl 
 |-  ( ph -> ( q e. A <-> E. v e. ( V \ { ( 0g ` W ) } ) q = ( ( LSpan ` W ) ` { v } ) ) )
65 64 anbi1d 
 |-  ( ph -> ( ( q e. A /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) <-> ( E. v e. ( V \ { ( 0g ` W ) } ) q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) ) )
66 65 exbidv 
 |-  ( ph -> ( E. q ( q e. A /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) <-> E. q ( E. v e. ( V \ { ( 0g ` W ) } ) q = ( ( LSpan ` W ) ` { v } ) /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) ) )
67 62 66 bitr4d 
 |-  ( ph -> ( E. v e. V ( ( U e. S /\ U =/= V ) /\ ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> E. q ( q e. A /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) ) )
68 11 67 syl5bb 
 |-  ( ph -> ( ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> E. q ( q e. A /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) ) )
69 df-3an 
 |-  ( ( U e. S /\ U =/= V /\ E. q e. A ( U .(+) q ) = V ) <-> ( ( U e. S /\ U =/= V ) /\ E. q e. A ( U .(+) q ) = V ) )
70 r19.42v 
 |-  ( E. q e. A ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) <-> ( ( U e. S /\ U =/= V ) /\ E. q e. A ( U .(+) q ) = V ) )
71 df-rex 
 |-  ( E. q e. A ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) <-> E. q ( q e. A /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) )
72 70 71 bitr3i 
 |-  ( ( ( U e. S /\ U =/= V ) /\ E. q e. A ( U .(+) q ) = V ) <-> E. q ( q e. A /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) )
73 69 72 bitr2i 
 |-  ( E. q ( q e. A /\ ( ( U e. S /\ U =/= V ) /\ ( U .(+) q ) = V ) ) <-> ( U e. S /\ U =/= V /\ E. q e. A ( U .(+) q ) = V ) )
74 68 73 bitrdi 
 |-  ( ph -> ( ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) <-> ( U e. S /\ U =/= V /\ E. q e. A ( U .(+) q ) = V ) ) )
75 8 74 bitrd 
 |-  ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. q e. A ( U .(+) q ) = V ) ) )