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