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 φ W LMod
Assertion islshpat φ U H U S U V q 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 φ W LMod
7 eqid LSpan W = LSpan W
8 1 7 2 3 4 6 islshpsm φ U H U S U V v V U ˙ LSpan W v = V
9 df-3an U S U V v V U ˙ LSpan W v = V U S U V v V U ˙ LSpan W v = V
10 r19.42v v V U S U V U ˙ LSpan W v = V U S U V v V U ˙ LSpan W v = V
11 9 10 bitr4i U S U V v V U ˙ LSpan W v = V v V U S U V U ˙ LSpan W v = V
12 df-rex v V U S U V U ˙ LSpan W v = V v v V U S U V U ˙ LSpan W v = V
13 simpr φ v V U S U V v = 0 W v = 0 W
14 13 sneqd φ v V U S U V v = 0 W v = 0 W
15 14 fveq2d φ v V U S U V v = 0 W LSpan W v = LSpan W 0 W
16 6 ad3antrrr φ v V U S U V v = 0 W W LMod
17 eqid 0 W = 0 W
18 17 7 lspsn0 W LMod LSpan W 0 W = 0 W
19 16 18 syl φ v V U S U V v = 0 W LSpan W 0 W = 0 W
20 15 19 eqtrd φ v V U S U V v = 0 W LSpan W v = 0 W
21 20 oveq2d φ v V U S U V v = 0 W U ˙ LSpan W v = U ˙ 0 W
22 simplrl φ v V U S U V v = 0 W U S
23 2 lsssubg W LMod U S U SubGrp W
24 16 22 23 syl2anc φ v V U S U V v = 0 W U SubGrp W
25 17 3 lsm01 U SubGrp W U ˙ 0 W = U
26 24 25 syl φ v V U S U V v = 0 W U ˙ 0 W = U
27 21 26 eqtrd φ v V U S U V v = 0 W U ˙ LSpan W v = U
28 simplrr φ v V U S U V v = 0 W U V
29 27 28 eqnetrd φ v V U S U V v = 0 W U ˙ LSpan W v V
30 29 ex φ v V U S U V v = 0 W U ˙ LSpan W v V
31 30 necon2d φ v V U S U V U ˙ LSpan W v = V v 0 W
32 31 pm4.71rd φ v V U S U V U ˙ LSpan W v = V v 0 W U ˙ LSpan W v = V
33 32 pm5.32da φ v V U S U V U ˙ LSpan W v = V U S U V v 0 W U ˙ LSpan W v = V
34 33 pm5.32da φ v V U S U V U ˙ LSpan W v = V v V U S U V v 0 W U ˙ LSpan W v = V
35 eldifsn v V 0 W v V v 0 W
36 35 anbi1i v V 0 W U S U V U ˙ LSpan W v = V v V v 0 W U S U V U ˙ LSpan W v = V
37 anass v V v 0 W U S U V U ˙ LSpan W v = V v V v 0 W U S U V U ˙ LSpan W v = V
38 an12 v 0 W U S U V U ˙ LSpan W v = V U S U V v 0 W U ˙ LSpan W v = V
39 38 anbi2i v V v 0 W U S U V U ˙ LSpan W v = V v V U S U V v 0 W U ˙ LSpan W v = V
40 37 39 bitri v V v 0 W U S U V U ˙ LSpan W v = V v V U S U V v 0 W U ˙ LSpan W v = V
41 36 40 bitr2i v V U S U V v 0 W U ˙ LSpan W v = V v V 0 W U S U V U ˙ LSpan W v = V
42 34 41 bitrdi φ v V U S U V U ˙ LSpan W v = V v V 0 W U S U V U ˙ LSpan W v = V
43 42 exbidv φ v v V U S U V U ˙ LSpan W v = V v v V 0 W U S U V U ˙ LSpan W v = V
44 12 43 syl5bb φ v V U S U V U ˙ LSpan W v = V v v V 0 W U S U V U ˙ LSpan W v = V
45 fvex LSpan W v V
46 45 rexcom4b q v V 0 W U S U V U ˙ LSpan W v = V q = LSpan W v v V 0 W U S U V U ˙ LSpan W v = V
47 df-rex v V 0 W U S U V U ˙ LSpan W v = V v v V 0 W U S U V U ˙ LSpan W v = V
48 46 47 bitr2i v v V 0 W U S U V U ˙ LSpan W v = V q v V 0 W U S U V U ˙ LSpan W v = V q = LSpan W v
49 ancom U S U V U ˙ LSpan W v = V q = LSpan W v q = LSpan W v U S U V U ˙ LSpan W v = V
50 49 rexbii v V 0 W U S U V U ˙ LSpan W v = V q = LSpan W v v V 0 W q = LSpan W v U S U V U ˙ LSpan W v = V
51 50 exbii q v V 0 W U S U V U ˙ LSpan W v = V q = LSpan W v q v V 0 W q = LSpan W v U S U V U ˙ LSpan W v = V
52 48 51 bitri v v V 0 W U S U V U ˙ LSpan W v = V q v V 0 W q = LSpan W v U S U V U ˙ LSpan W v = V
53 44 52 bitrdi φ v V U S U V U ˙ LSpan W v = V q v V 0 W q = LSpan W v U S U V U ˙ LSpan W v = V
54 r19.41v v V 0 W q = LSpan W v U S U V U ˙ q = V v V 0 W q = LSpan W v U 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 S U V U ˙ q = V U S U V U ˙ LSpan W v = V
58 57 pm5.32i q = LSpan W v U S U V U ˙ q = V q = LSpan W v U S U V U ˙ LSpan W v = V
59 58 rexbii v V 0 W q = LSpan W v U S U V U ˙ q = V v V 0 W q = LSpan W v U S U V U ˙ LSpan W v = V
60 54 59 bitr3i v V 0 W q = LSpan W v U S U V U ˙ q = V v V 0 W q = LSpan W v U S U V U ˙ LSpan W v = V
61 60 exbii q v V 0 W q = LSpan W v U S U V U ˙ q = V q v V 0 W q = LSpan W v U S U V U ˙ LSpan W v = V
62 53 61 bitr4di φ v V U S U V U ˙ LSpan W v = V q v V 0 W q = LSpan W v U S U V U ˙ q = V
63 1 7 17 5 islsat W LMod q A v V 0 W q = LSpan W v
64 6 63 syl φ q A v V 0 W q = LSpan W v
65 64 anbi1d φ q A U S U V U ˙ q = V v V 0 W q = LSpan W v U S U V U ˙ q = V
66 65 exbidv φ q q A U S U V U ˙ q = V q v V 0 W q = LSpan W v U S U V U ˙ q = V
67 62 66 bitr4d φ v V U S U V U ˙ LSpan W v = V q q A U S U V U ˙ q = V
68 11 67 syl5bb φ U S U V v V U ˙ LSpan W v = V q q A U S U V U ˙ q = V
69 df-3an U S U V q A U ˙ q = V U S U V q A U ˙ q = V
70 r19.42v q A U S U V U ˙ q = V U S U V q A U ˙ q = V
71 df-rex q A U S U V U ˙ q = V q q A U S U V U ˙ q = V
72 70 71 bitr3i U S U V q A U ˙ q = V q q A U S U V U ˙ q = V
73 69 72 bitr2i q q A U S U V U ˙ q = V U S U V q A U ˙ q = V
74 68 73 bitrdi φ U S U V v V U ˙ LSpan W v = V U S U V q A U ˙ q = V
75 8 74 bitrd φ U H U S U V q A U ˙ q = V