Metamath Proof Explorer

Theorem pjssmii

Description: Projection meet property. Remark in Kalmbach p. 66. Also Theorem 4.5(i)->(iv) of Beran p. 112. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 
|- H e. CH
pjidm.2 
|- A e. ~H
pjsslem.1 
|- G e. CH
Assertion pjssmii 
|- ( H C_ G -> ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 
 |-  H e. CH
2 pjidm.2 
 |-  A e. ~H
3 pjsslem.1 
 |-  G e. CH
4 3 2 pjclii 
 |-  ( ( projh ` G ) ` A ) e. G
5 1 2 pjclii 
 |-  ( ( projh ` H ) ` A ) e. H
6 ssel 
 |-  ( H C_ G -> ( ( ( projh ` H ) ` A ) e. H -> ( ( projh ` H ) ` A ) e. G ) )
7 5 6 mpi 
 |-  ( H C_ G -> ( ( projh ` H ) ` A ) e. G )
8 3 chshii 
 |-  G e. SH
9 shsubcl 
 |-  ( ( G e. SH /\ ( ( projh ` G ) ` A ) e. G /\ ( ( projh ` H ) ` A ) e. G ) -> ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. G )
10 8 9 mp3an1 
 |-  ( ( ( ( projh ` G ) ` A ) e. G /\ ( ( projh ` H ) ` A ) e. G ) -> ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. G )
11 4 7 10 sylancr 
 |-  ( H C_ G -> ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. G )
12 1 2 3 pjsslem 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) = ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) )
13 1 3 chsscon3i 
 |-  ( H C_ G <-> ( _|_ ` G ) C_ ( _|_ ` H ) )
14 1 choccli 
 |-  ( _|_ ` H ) e. CH
15 14 2 pjclii 
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H )
16 3 choccli 
 |-  ( _|_ ` G ) e. CH
17 16 2 pjclii 
 |-  ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` G )
18 ssel 
 |-  ( ( _|_ ` G ) C_ ( _|_ ` H ) -> ( ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` G ) -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` H ) ) )
19 17 18 mpi 
 |-  ( ( _|_ ` G ) C_ ( _|_ ` H ) -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` H ) )
20 14 chshii 
 |-  ( _|_ ` H ) e. SH
21 shsubcl 
 |-  ( ( ( _|_ ` H ) e. SH /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) /\ ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` H ) ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` H ) )
22 20 21 mp3an1 
 |-  ( ( ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) /\ ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` H ) ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` H ) )
23 15 19 22 sylancr 
 |-  ( ( _|_ ` G ) C_ ( _|_ ` H ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` H ) )
24 13 23 sylbi 
 |-  ( H C_ G -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` H ) )
25 12 24 eqeltrrid 
 |-  ( H C_ G -> ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ( _|_ ` H ) )
26 11 25 jca 
 |-  ( H C_ G -> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. G /\ ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ( _|_ ` H ) ) )
27 elin 
 |-  ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ( G i^i ( _|_ ` H ) ) <-> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. G /\ ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ( _|_ ` H ) ) )
28 3 14 chincli 
 |-  ( G i^i ( _|_ ` H ) ) e. CH
29 3 2 pjhclii 
 |-  ( ( projh ` G ) ` A ) e. ~H
30 1 2 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
31 29 30 hvsubcli 
 |-  ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ~H
32 28 31 pjchi 
 |-  ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ( G i^i ( _|_ ` H ) ) <-> ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) )
33 27 32 bitr3i 
 |-  ( ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. G /\ ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) e. ( _|_ ` H ) ) <-> ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) )
34 26 33 sylib 
 |-  ( H C_ G -> ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) )
35 28 29 30 pjsubii 
 |-  ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` G ) ` A ) ) -h ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) )
36 28 29 pjhclii 
 |-  ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` G ) ` A ) ) e. ~H
37 28 30 pjhclii 
 |-  ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) e. ~H
38 36 37 hvsubvali 
 |-  ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` G ) ` A ) ) -h ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) ) = ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` G ) ` A ) ) +h ( -u 1 .h ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) ) )
39 inss1 
 |-  ( G i^i ( _|_ ` H ) ) C_ G
40 28 2 3 pjss2i 
 |-  ( ( G i^i ( _|_ ` H ) ) C_ G -> ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` G ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) )
41 39 40 ax-mp 
 |-  ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` G ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A )
42 1 chshii 
 |-  H e. SH
43 shococss 
 |-  ( H e. SH -> H C_ ( _|_ ` ( _|_ ` H ) ) )
44 42 43 ax-mp 
 |-  H C_ ( _|_ ` ( _|_ ` H ) )
45 inss2 
 |-  ( G i^i ( _|_ ` H ) ) C_ ( _|_ ` H )
46 28 14 chsscon3i 
 |-  ( ( G i^i ( _|_ ` H ) ) C_ ( _|_ ` H ) <-> ( _|_ ` ( _|_ ` H ) ) C_ ( _|_ ` ( G i^i ( _|_ ` H ) ) ) )
47 45 46 mpbi 
 |-  ( _|_ ` ( _|_ ` H ) ) C_ ( _|_ ` ( G i^i ( _|_ ` H ) ) )
48 44 47 sstri 
 |-  H C_ ( _|_ ` ( G i^i ( _|_ ` H ) ) )
49 48 5 sselii 
 |-  ( ( projh ` H ) ` A ) e. ( _|_ ` ( G i^i ( _|_ ` H ) ) )
50 28 30 pjoc2i 
 |-  ( ( ( projh ` H ) ` A ) e. ( _|_ ` ( G i^i ( _|_ ` H ) ) ) <-> ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) = 0h )
51 49 50 mpbi 
 |-  ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) = 0h
52 51 oveq2i 
 |-  ( -u 1 .h ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) ) = ( -u 1 .h 0h )
53 neg1cn 
 |-  -u 1 e. CC
54 hvmul0 
 |-  ( -u 1 e. CC -> ( -u 1 .h 0h ) = 0h )
55 53 54 ax-mp 
 |-  ( -u 1 .h 0h ) = 0h
56 52 55 eqtri 
 |-  ( -u 1 .h ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) ) = 0h
57 41 56 oveq12i 
 |-  ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` G ) ` A ) ) +h ( -u 1 .h ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) ) ) = ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) +h 0h )
58 28 2 pjhclii 
 |-  ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) e. ~H
59 ax-hvaddid 
 |-  ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) e. ~H -> ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) +h 0h ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) )
60 58 59 ax-mp 
 |-  ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) +h 0h ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A )
61 57 60 eqtri 
 |-  ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` G ) ` A ) ) +h ( -u 1 .h ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A )
62 38 61 eqtri 
 |-  ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` G ) ` A ) ) -h ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( projh ` H ) ` A ) ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A )
63 35 62 eqtri 
 |-  ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A )
64 34 63 eqtr3di 
 |-  ( H C_ G -> ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) )