Metamath Proof Explorer

Theorem chirredlem3

Description: Lemma for chirredi . (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses chirred.1 
|- A e. CH
chirred.2 
|- ( x e. CH -> A C_H x )
Assertion chirredlem3 
|- ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( r C_ A -> r = p ) )

Proof

Step Hyp Ref Expression
1 chirred.1 
 |-  A e. CH
2 chirred.2 
 |-  ( x e. CH -> A C_H x )
3 atelch 
 |-  ( q e. HAtoms -> q e. CH )
4 1 chirredlem2 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( ( _|_ ` r ) i^i ( p vH q ) ) = q )
5 4 oveq2d 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( r vH ( ( _|_ ` r ) i^i ( p vH q ) ) ) = ( r vH q ) )
6 atelch 
 |-  ( r e. HAtoms -> r e. CH )
7 6 adantr 
 |-  ( ( r e. HAtoms /\ r C_ A ) -> r e. CH )
8 atelch 
 |-  ( p e. HAtoms -> p e. CH )
9 chjcl 
 |-  ( ( p e. CH /\ q e. CH ) -> ( p vH q ) e. CH )
10 8 9 sylan 
 |-  ( ( p e. HAtoms /\ q e. CH ) -> ( p vH q ) e. CH )
11 10 ad2ant2r 
 |-  ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) -> ( p vH q ) e. CH )
12 id 
 |-  ( r C_ ( p vH q ) -> r C_ ( p vH q ) )
13 pjoml2 
 |-  ( ( r e. CH /\ ( p vH q ) e. CH /\ r C_ ( p vH q ) ) -> ( r vH ( ( _|_ ` r ) i^i ( p vH q ) ) ) = ( p vH q ) )
14 7 11 12 13 syl3an 
 |-  ( ( ( r e. HAtoms /\ r C_ A ) /\ ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ r C_ ( p vH q ) ) -> ( r vH ( ( _|_ ` r ) i^i ( p vH q ) ) ) = ( p vH q ) )
15 14 3com12 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) -> ( r vH ( ( _|_ ` r ) i^i ( p vH q ) ) ) = ( p vH q ) )
16 15 3expb 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( r vH ( ( _|_ ` r ) i^i ( p vH q ) ) ) = ( p vH q ) )
17 5 16 eqtr3d 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( r vH q ) = ( p vH q ) )
18 17 ineq2d 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( A i^i ( r vH q ) ) = ( A i^i ( p vH q ) ) )
19 breq2 
 |-  ( x = r -> ( A C_H x <-> A C_H r ) )
20 19 2 vtoclga 
 |-  ( r e. CH -> A C_H r )
21 breq2 
 |-  ( x = q -> ( A C_H x <-> A C_H q ) )
22 21 2 vtoclga 
 |-  ( q e. CH -> A C_H q )
23 20 22 anim12i 
 |-  ( ( r e. CH /\ q e. CH ) -> ( A C_H r /\ A C_H q ) )
24 fh1 
 |-  ( ( ( A e. CH /\ r e. CH /\ q e. CH ) /\ ( A C_H r /\ A C_H q ) ) -> ( A i^i ( r vH q ) ) = ( ( A i^i r ) vH ( A i^i q ) ) )
25 1 24 mp3anl1 
 |-  ( ( ( r e. CH /\ q e. CH ) /\ ( A C_H r /\ A C_H q ) ) -> ( A i^i ( r vH q ) ) = ( ( A i^i r ) vH ( A i^i q ) ) )
26 23 25 mpdan 
 |-  ( ( r e. CH /\ q e. CH ) -> ( A i^i ( r vH q ) ) = ( ( A i^i r ) vH ( A i^i q ) ) )
27 6 26 sylan 
 |-  ( ( r e. HAtoms /\ q e. CH ) -> ( A i^i ( r vH q ) ) = ( ( A i^i r ) vH ( A i^i q ) ) )
28 27 ancoms 
 |-  ( ( q e. CH /\ r e. HAtoms ) -> ( A i^i ( r vH q ) ) = ( ( A i^i r ) vH ( A i^i q ) ) )
29 28 adantrr 
 |-  ( ( q e. CH /\ ( r e. HAtoms /\ r C_ A ) ) -> ( A i^i ( r vH q ) ) = ( ( A i^i r ) vH ( A i^i q ) ) )
30 29 ad2ant2r 
 |-  ( ( ( q e. CH /\ q C_ ( _|_ ` A ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( A i^i ( r vH q ) ) = ( ( A i^i r ) vH ( A i^i q ) ) )
31 30 adantll 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( A i^i ( r vH q ) ) = ( ( A i^i r ) vH ( A i^i q ) ) )
32 breq2 
 |-  ( x = p -> ( A C_H x <-> A C_H p ) )
33 32 2 vtoclga 
 |-  ( p e. CH -> A C_H p )
34 33 22 anim12i 
 |-  ( ( p e. CH /\ q e. CH ) -> ( A C_H p /\ A C_H q ) )
35 fh1 
 |-  ( ( ( A e. CH /\ p e. CH /\ q e. CH ) /\ ( A C_H p /\ A C_H q ) ) -> ( A i^i ( p vH q ) ) = ( ( A i^i p ) vH ( A i^i q ) ) )
36 1 35 mp3anl1 
 |-  ( ( ( p e. CH /\ q e. CH ) /\ ( A C_H p /\ A C_H q ) ) -> ( A i^i ( p vH q ) ) = ( ( A i^i p ) vH ( A i^i q ) ) )
37 34 36 mpdan 
 |-  ( ( p e. CH /\ q e. CH ) -> ( A i^i ( p vH q ) ) = ( ( A i^i p ) vH ( A i^i q ) ) )
38 8 37 sylan 
 |-  ( ( p e. HAtoms /\ q e. CH ) -> ( A i^i ( p vH q ) ) = ( ( A i^i p ) vH ( A i^i q ) ) )
39 38 ad2ant2r 
 |-  ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) -> ( A i^i ( p vH q ) ) = ( ( A i^i p ) vH ( A i^i q ) ) )
40 39 adantr 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( A i^i ( p vH q ) ) = ( ( A i^i p ) vH ( A i^i q ) ) )
41 18 31 40 3eqtr3d 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( ( A i^i r ) vH ( A i^i q ) ) = ( ( A i^i p ) vH ( A i^i q ) ) )
42 sseqin2 
 |-  ( r C_ A <-> ( A i^i r ) = r )
43 42 biimpi 
 |-  ( r C_ A -> ( A i^i r ) = r )
44 43 ad2antlr 
 |-  ( ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) -> ( A i^i r ) = r )
45 44 adantl 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( A i^i r ) = r )
46 incom 
 |-  ( A i^i q ) = ( q i^i A )
47 chsh 
 |-  ( q e. CH -> q e. SH )
48 1 chshii 
 |-  A e. SH
49 orthin 
 |-  ( ( q e. SH /\ A e. SH ) -> ( q C_ ( _|_ ` A ) -> ( q i^i A ) = 0H ) )
50 47 48 49 sylancl 
 |-  ( q e. CH -> ( q C_ ( _|_ ` A ) -> ( q i^i A ) = 0H ) )
51 50 imp 
 |-  ( ( q e. CH /\ q C_ ( _|_ ` A ) ) -> ( q i^i A ) = 0H )
52 46 51 syl5eq 
 |-  ( ( q e. CH /\ q C_ ( _|_ ` A ) ) -> ( A i^i q ) = 0H )
53 52 ad2antlr 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( A i^i q ) = 0H )
54 45 53 oveq12d 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( ( A i^i r ) vH ( A i^i q ) ) = ( r vH 0H ) )
55 sseqin2 
 |-  ( p C_ A <-> ( A i^i p ) = p )
56 55 biimpi 
 |-  ( p C_ A -> ( A i^i p ) = p )
57 56 adantl 
 |-  ( ( p e. HAtoms /\ p C_ A ) -> ( A i^i p ) = p )
58 57 ad2antrr 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( A i^i p ) = p )
59 58 53 oveq12d 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( ( A i^i p ) vH ( A i^i q ) ) = ( p vH 0H ) )
60 41 54 59 3eqtr3d 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( r vH 0H ) = ( p vH 0H ) )
61 chj0 
 |-  ( r e. CH -> ( r vH 0H ) = r )
62 6 61 syl 
 |-  ( r e. HAtoms -> ( r vH 0H ) = r )
63 62 ad2antrr 
 |-  ( ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) -> ( r vH 0H ) = r )
64 63 adantl 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( r vH 0H ) = r )
65 chj0 
 |-  ( p e. CH -> ( p vH 0H ) = p )
66 8 65 syl 
 |-  ( p e. HAtoms -> ( p vH 0H ) = p )
67 66 ad3antrrr 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( p vH 0H ) = p )
68 60 64 67 3eqtr3d 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> r = p )
69 68 exp44 
 |-  ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) -> ( r e. HAtoms -> ( r C_ A -> ( r C_ ( p vH q ) -> r = p ) ) ) )
70 69 com34 
 |-  ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) -> ( r e. HAtoms -> ( r C_ ( p vH q ) -> ( r C_ A -> r = p ) ) ) )
71 3 70 sylanr1 
 |-  ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) -> ( r e. HAtoms -> ( r C_ ( p vH q ) -> ( r C_ A -> r = p ) ) ) )
72 71 imp32 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( r C_ A -> r = p ) )