Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihjatcclem4 Structured version   Unicode version

Theorem dihjatcclem4 34952
Description: Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 29-Sep-2014.)
Hypotheses
Ref Expression
dihjatcclem.b  |-  B  =  ( Base `  K
)
dihjatcclem.l  |-  .<_  =  ( le `  K )
dihjatcclem.h  |-  H  =  ( LHyp `  K
)
dihjatcclem.j  |-  .\/  =  ( join `  K )
dihjatcclem.m  |-  ./\  =  ( meet `  K )
dihjatcclem.a  |-  A  =  ( Atoms `  K )
dihjatcclem.u  |-  U  =  ( ( DVecH `  K
) `  W )
dihjatcclem.s  |-  .(+)  =  (
LSSum `  U )
dihjatcclem.i  |-  I  =  ( ( DIsoH `  K
) `  W )
dihjatcclem.v  |-  V  =  ( ( P  .\/  Q )  ./\  W )
dihjatcclem.k  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
dihjatcclem.p  |-  ( ph  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
dihjatcclem.q  |-  ( ph  ->  ( Q  e.  A  /\  -.  Q  .<_  W ) )
dihjatcc.w  |-  C  =  ( ( oc `  K ) `  W
)
dihjatcc.t  |-  T  =  ( ( LTrn `  K
) `  W )
dihjatcc.r  |-  R  =  ( ( trL `  K
) `  W )
dihjatcc.e  |-  E  =  ( ( TEndo `  K
) `  W )
dihjatcc.g  |-  G  =  ( iota_ d  e.  T  ( d `  C
)  =  P )
dihjatcc.dd  |-  D  =  ( iota_ d  e.  T  ( d `  C
)  =  Q )
dihjatcc.n  |-  N  =  ( a  e.  E  |->  ( d  e.  T  |->  `' ( a `  d ) ) )
dihjatcc.o  |-  .0.  =  ( d  e.  T  |->  (  _I  |`  B ) )
dihjatcc.d  |-  J  =  ( a  e.  E ,  b  e.  E  |->  ( d  e.  T  |->  ( ( a `  d )  o.  (
b `  d )
) ) )
Assertion
Ref Expression
dihjatcclem4  |-  ( ph  ->  ( I `  V
)  C_  ( (
I `  P )  .(+)  ( I `  Q
) ) )
Distinct variable groups:    .<_ , d    A, d    B, d    C, d   
a, b, E    H, d    P, d    a, d, K, b    Q, d    T, a, b, d    W, a, b, d
Allowed substitution hints:    ph( a, b, d)    A( a, b)    B( a, b)    C( a, b)    D( a, b, d)    P( a, b)    .(+) ( a, b,
d)    Q( a, b)    R( a, b, d)    U( a, b, d)    E( d)    G( a, b, d)    H( a, b)    I( a, b, d)    J( a, b, d)    .\/ ( a, b, d)    .<_ ( a, b)    ./\ ( a, b, d)    N( a, b, d)    V( a, b, d)    .0. ( a,
b, d)

Proof of Theorem dihjatcclem4
Dummy variables  t 
f  s  g  h  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dihjatcclem.k . . 3  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
2 dihjatcclem.h . . . 4  |-  H  =  ( LHyp `  K
)
3 dihjatcclem.i . . . 4  |-  I  =  ( ( DIsoH `  K
) `  W )
42, 3dihvalrel 34810 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  Rel  ( I `  V ) )
51, 4syl 17 . 2  |-  ( ph  ->  Rel  ( I `  V ) )
61adantr 467 . . . . . . 7  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
7 dihjatcclem.l . . . . . . . . . . . 12  |-  .<_  =  ( le `  K )
8 dihjatcclem.a . . . . . . . . . . . 12  |-  A  =  ( Atoms `  K )
9 dihjatcc.w . . . . . . . . . . . 12  |-  C  =  ( ( oc `  K ) `  W
)
107, 8, 2, 9lhpocnel2 33547 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( C  e.  A  /\  -.  C  .<_  W ) )
111, 10syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( C  e.  A  /\  -.  C  .<_  W ) )
12 dihjatcclem.p . . . . . . . . . 10  |-  ( ph  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
13 dihjatcc.t . . . . . . . . . . 11  |-  T  =  ( ( LTrn `  K
) `  W )
14 dihjatcc.g . . . . . . . . . . 11  |-  G  =  ( iota_ d  e.  T  ( d `  C
)  =  P )
157, 8, 2, 13, 14ltrniotacl 34109 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( C  e.  A  /\  -.  C  .<_  W )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  G  e.  T )
161, 11, 12, 15syl3anc 1265 . . . . . . . . 9  |-  ( ph  ->  G  e.  T )
17 dihjatcclem.q . . . . . . . . . . 11  |-  ( ph  ->  ( Q  e.  A  /\  -.  Q  .<_  W ) )
18 dihjatcc.dd . . . . . . . . . . . 12  |-  D  =  ( iota_ d  e.  T  ( d `  C
)  =  Q )
197, 8, 2, 13, 18ltrniotacl 34109 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( C  e.  A  /\  -.  C  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  D  e.  T )
201, 11, 17, 19syl3anc 1265 . . . . . . . . . 10  |-  ( ph  ->  D  e.  T )
212, 13ltrncnv 33674 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  D  e.  T
)  ->  `' D  e.  T )
221, 20, 21syl2anc 666 . . . . . . . . 9  |-  ( ph  ->  `' D  e.  T
)
232, 13ltrnco 34249 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  `' D  e.  T
)  ->  ( G  o.  `' D )  e.  T
)
241, 16, 22, 23syl3anc 1265 . . . . . . . 8  |-  ( ph  ->  ( G  o.  `' D )  e.  T
)
2524adantr 467 . . . . . . 7  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  -> 
( G  o.  `' D )  e.  T
)
26 simprll 771 . . . . . . 7  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  -> 
f  e.  T )
27 simprlr 772 . . . . . . . 8  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  -> 
( R `  f
)  .<_  V )
28 dihjatcclem.b . . . . . . . . . 10  |-  B  =  ( Base `  K
)
29 dihjatcclem.j . . . . . . . . . 10  |-  .\/  =  ( join `  K )
30 dihjatcclem.m . . . . . . . . . 10  |-  ./\  =  ( meet `  K )
31 dihjatcclem.u . . . . . . . . . 10  |-  U  =  ( ( DVecH `  K
) `  W )
32 dihjatcclem.s . . . . . . . . . 10  |-  .(+)  =  (
LSSum `  U )
33 dihjatcclem.v . . . . . . . . . 10  |-  V  =  ( ( P  .\/  Q )  ./\  W )
34 dihjatcc.r . . . . . . . . . 10  |-  R  =  ( ( trL `  K
) `  W )
35 dihjatcc.e . . . . . . . . . 10  |-  E  =  ( ( TEndo `  K
) `  W )
3628, 7, 2, 29, 30, 8, 31, 32, 3, 33, 1, 12, 17, 9, 13, 34, 35, 14, 18dihjatcclem3 34951 . . . . . . . . 9  |-  ( ph  ->  ( R `  ( G  o.  `' D
) )  =  V )
3736adantr 467 . . . . . . . 8  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  -> 
( R `  ( G  o.  `' D
) )  =  V )
3827, 37breqtrrd 4448 . . . . . . 7  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  -> 
( R `  f
)  .<_  ( R `  ( G  o.  `' D ) ) )
397, 2, 13, 34, 35tendoex 34505 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( G  o.  `' D )  e.  T  /\  f  e.  T )  /\  ( R `  f )  .<_  ( R `  ( G  o.  `' D
) ) )  ->  E. t  e.  E  ( t `  ( G  o.  `' D
) )  =  f )
406, 25, 26, 38, 39syl121anc 1270 . . . . . 6  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  ->  E. t  e.  E  ( t `  ( G  o.  `' D
) )  =  f )
41 df-rex 2782 . . . . . 6  |-  ( E. t  e.  E  ( t `  ( G  o.  `' D ) )  =  f  <->  E. t
( t  e.  E  /\  ( t `  ( G  o.  `' D
) )  =  f ) )
4240, 41sylib 200 . . . . 5  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  ->  E. t ( t  e.  E  /\  ( t `
 ( G  o.  `' D ) )  =  f ) )
43 eqidd 2424 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( t `  G
)  =  ( t `
 G ) )
44 simprl 763 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
t  e.  E )
451ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
4612ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( P  e.  A  /\  -.  P  .<_  W ) )
47 fvex 5889 . . . . . . . . . . . 12  |-  ( t `
 G )  e. 
_V
48 vex 3085 . . . . . . . . . . . 12  |-  t  e. 
_V
497, 8, 2, 9, 13, 35, 3, 14, 47, 48dihopelvalcqat 34777 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  -> 
( <. ( t `  G ) ,  t
>.  e.  ( I `  P )  <->  ( (
t `  G )  =  ( t `  G )  /\  t  e.  E ) ) )
5045, 46, 49syl2anc 666 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( <. ( t `  G ) ,  t
>.  e.  ( I `  P )  <->  ( (
t `  G )  =  ( t `  G )  /\  t  e.  E ) ) )
5143, 44, 50mpbir2and 931 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  ->  <. ( t `  G
) ,  t >.  e.  ( I `  P
) )
52 eqidd 2424 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( ( N `  t ) `  D
)  =  ( ( N `  t ) `
 D ) )
53 dihjatcc.n . . . . . . . . . . . 12  |-  N  =  ( a  e.  E  |->  ( d  e.  T  |->  `' ( a `  d ) ) )
542, 13, 35, 53tendoicl 34326 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  t  e.  E
)  ->  ( N `  t )  e.  E
)
5545, 44, 54syl2anc 666 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( N `  t
)  e.  E )
5617ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( Q  e.  A  /\  -.  Q  .<_  W ) )
57 fvex 5889 . . . . . . . . . . . 12  |-  ( ( N `  t ) `
 D )  e. 
_V
58 fvex 5889 . . . . . . . . . . . 12  |-  ( N `
 t )  e. 
_V
597, 8, 2, 9, 13, 35, 3, 18, 57, 58dihopelvalcqat 34777 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  -> 
( <. ( ( N `
 t ) `  D ) ,  ( N `  t )
>.  e.  ( I `  Q )  <->  ( (
( N `  t
) `  D )  =  ( ( N `
 t ) `  D )  /\  ( N `  t )  e.  E ) ) )
6045, 56, 59syl2anc 666 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( <. ( ( N `
 t ) `  D ) ,  ( N `  t )
>.  e.  ( I `  Q )  <->  ( (
( N `  t
) `  D )  =  ( ( N `
 t ) `  D )  /\  ( N `  t )  e.  E ) ) )
6152, 55, 60mpbir2and 931 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  ->  <. ( ( N `  t ) `  D
) ,  ( N `
 t ) >.  e.  ( I `  Q
) )
6216ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  ->  G  e.  T )
6322ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  ->  `' D  e.  T
)
642, 13, 35tendospdi1 34551 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( t  e.  E  /\  G  e.  T  /\  `' D  e.  T ) )  -> 
( t `  ( G  o.  `' D
) )  =  ( ( t `  G
)  o.  ( t `
 `' D ) ) )
6545, 44, 62, 63, 64syl13anc 1267 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( t `  ( G  o.  `' D
) )  =  ( ( t `  G
)  o.  ( t `
 `' D ) ) )
66 simprr 765 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( t `  ( G  o.  `' D
) )  =  f )
6720ad2antrr 731 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  ->  D  e.  T )
6853, 13tendoi2 34325 . . . . . . . . . . . . 13  |-  ( ( t  e.  E  /\  D  e.  T )  ->  ( ( N `  t ) `  D
)  =  `' ( t `  D ) )
6944, 67, 68syl2anc 666 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( ( N `  t ) `  D
)  =  `' ( t `  D ) )
702, 13, 35tendocnv 34552 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  t  e.  E  /\  D  e.  T
)  ->  `' (
t `  D )  =  ( t `  `' D ) )
7145, 44, 67, 70syl3anc 1265 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  ->  `' ( t `  D )  =  ( t `  `' D
) )
7269, 71eqtr2d 2465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( t `  `' D )  =  ( ( N `  t
) `  D )
)
7372coeq2d 5014 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( ( t `  G )  o.  (
t `  `' D
) )  =  ( ( t `  G
)  o.  ( ( N `  t ) `
 D ) ) )
7465, 66, 733eqtr3d 2472 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
f  =  ( ( t `  G )  o.  ( ( N `
 t ) `  D ) ) )
75 simplrr 770 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
s  =  .0.  )
76 dihjatcc.d . . . . . . . . . . . 12  |-  J  =  ( a  e.  E ,  b  e.  E  |->  ( d  e.  T  |->  ( ( a `  d )  o.  (
b `  d )
) ) )
77 dihjatcc.o . . . . . . . . . . . 12  |-  .0.  =  ( d  e.  T  |->  (  _I  |`  B ) )
782, 13, 35, 53, 28, 76, 77tendoipl2 34328 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  t  e.  E
)  ->  ( t J ( N `  t ) )  =  .0.  )
7945, 44, 78syl2anc 666 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
( t J ( N `  t ) )  =  .0.  )
8075, 79eqtr4d 2467 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  -> 
s  =  ( t J ( N `  t ) ) )
81 opeq1 4185 . . . . . . . . . . . . . . 15  |-  ( g  =  ( t `  G )  ->  <. g ,  t >.  =  <. ( t `  G ) ,  t >. )
8281eleq1d 2492 . . . . . . . . . . . . . 14  |-  ( g  =  ( t `  G )  ->  ( <. g ,  t >.  e.  ( I `  P
)  <->  <. ( t `  G ) ,  t
>.  e.  ( I `  P ) ) )
8382anbi1d 710 . . . . . . . . . . . . 13  |-  ( g  =  ( t `  G )  ->  (
( <. g ,  t
>.  e.  ( I `  P )  /\  <. h ,  u >.  e.  ( I `  Q ) )  <->  ( <. (
t `  G ) ,  t >.  e.  ( I `  P )  /\  <. h ,  u >.  e.  ( I `  Q ) ) ) )
84 coeq1 5009 . . . . . . . . . . . . . . 15  |-  ( g  =  ( t `  G )  ->  (
g  o.  h )  =  ( ( t `
 G )  o.  h ) )
8584eqeq2d 2437 . . . . . . . . . . . . . 14  |-  ( g  =  ( t `  G )  ->  (
f  =  ( g  o.  h )  <->  f  =  ( ( t `  G )  o.  h
) ) )
8685anbi1d 710 . . . . . . . . . . . . 13  |-  ( g  =  ( t `  G )  ->  (
( f  =  ( g  o.  h )  /\  s  =  ( t J u ) )  <->  ( f  =  ( ( t `  G )  o.  h
)  /\  s  =  ( t J u ) ) ) )
8783, 86anbi12d 716 . . . . . . . . . . . 12  |-  ( g  =  ( t `  G )  ->  (
( ( <. g ,  t >.  e.  ( I `  P )  /\  <. h ,  u >.  e.  ( I `  Q ) )  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) )  <->  ( ( <. ( t `  G
) ,  t >.  e.  ( I `  P
)  /\  <. h ,  u >.  e.  (
I `  Q )
)  /\  ( f  =  ( ( t `
 G )  o.  h )  /\  s  =  ( t J u ) ) ) ) )
88 opeq1 4185 . . . . . . . . . . . . . . 15  |-  ( h  =  ( ( N `
 t ) `  D )  ->  <. h ,  u >.  =  <. ( ( N `  t
) `  D ) ,  u >. )
8988eleq1d 2492 . . . . . . . . . . . . . 14  |-  ( h  =  ( ( N `
 t ) `  D )  ->  ( <. h ,  u >.  e.  ( I `  Q
)  <->  <. ( ( N `
 t ) `  D ) ,  u >.  e.  ( I `  Q ) ) )
9089anbi2d 709 . . . . . . . . . . . . 13  |-  ( h  =  ( ( N `
 t ) `  D )  ->  (
( <. ( t `  G ) ,  t
>.  e.  ( I `  P )  /\  <. h ,  u >.  e.  ( I `  Q ) )  <->  ( <. (
t `  G ) ,  t >.  e.  ( I `  P )  /\  <. ( ( N `
 t ) `  D ) ,  u >.  e.  ( I `  Q ) ) ) )
91 coeq2 5010 . . . . . . . . . . . . . . 15  |-  ( h  =  ( ( N `
 t ) `  D )  ->  (
( t `  G
)  o.  h )  =  ( ( t `
 G )  o.  ( ( N `  t ) `  D
) ) )
9291eqeq2d 2437 . . . . . . . . . . . . . 14  |-  ( h  =  ( ( N `
 t ) `  D )  ->  (
f  =  ( ( t `  G )  o.  h )  <->  f  =  ( ( t `  G )  o.  (
( N `  t
) `  D )
) ) )
9392anbi1d 710 . . . . . . . . . . . . 13  |-  ( h  =  ( ( N `
 t ) `  D )  ->  (
( f  =  ( ( t `  G
)  o.  h )  /\  s  =  ( t J u ) )  <->  ( f  =  ( ( t `  G )  o.  (
( N `  t
) `  D )
)  /\  s  =  ( t J u ) ) ) )
9490, 93anbi12d 716 . . . . . . . . . . . 12  |-  ( h  =  ( ( N `
 t ) `  D )  ->  (
( ( <. (
t `  G ) ,  t >.  e.  ( I `  P )  /\  <. h ,  u >.  e.  ( I `  Q ) )  /\  ( f  =  ( ( t `  G
)  o.  h )  /\  s  =  ( t J u ) ) )  <->  ( ( <. ( t `  G
) ,  t >.  e.  ( I `  P
)  /\  <. ( ( N `  t ) `
 D ) ,  u >.  e.  (
I `  Q )
)  /\  ( f  =  ( ( t `
 G )  o.  ( ( N `  t ) `  D
) )  /\  s  =  ( t J u ) ) ) ) )
95 opeq2 4186 . . . . . . . . . . . . . . 15  |-  ( u  =  ( N `  t )  ->  <. (
( N `  t
) `  D ) ,  u >.  =  <. ( ( N `  t
) `  D ) ,  ( N `  t ) >. )
9695eleq1d 2492 . . . . . . . . . . . . . 14  |-  ( u  =  ( N `  t )  ->  ( <. ( ( N `  t ) `  D
) ,  u >.  e.  ( I `  Q
)  <->  <. ( ( N `
 t ) `  D ) ,  ( N `  t )
>.  e.  ( I `  Q ) ) )
9796anbi2d 709 . . . . . . . . . . . . 13  |-  ( u  =  ( N `  t )  ->  (
( <. ( t `  G ) ,  t
>.  e.  ( I `  P )  /\  <. ( ( N `  t
) `  D ) ,  u >.  e.  (
I `  Q )
)  <->  ( <. (
t `  G ) ,  t >.  e.  ( I `  P )  /\  <. ( ( N `
 t ) `  D ) ,  ( N `  t )
>.  e.  ( I `  Q ) ) ) )
98 oveq2 6311 . . . . . . . . . . . . . . 15  |-  ( u  =  ( N `  t )  ->  (
t J u )  =  ( t J ( N `  t
) ) )
9998eqeq2d 2437 . . . . . . . . . . . . . 14  |-  ( u  =  ( N `  t )  ->  (
s  =  ( t J u )  <->  s  =  ( t J ( N `  t ) ) ) )
10099anbi2d 709 . . . . . . . . . . . . 13  |-  ( u  =  ( N `  t )  ->  (
( f  =  ( ( t `  G
)  o.  ( ( N `  t ) `
 D ) )  /\  s  =  ( t J u ) )  <->  ( f  =  ( ( t `  G )  o.  (
( N `  t
) `  D )
)  /\  s  =  ( t J ( N `  t ) ) ) ) )
10197, 100anbi12d 716 . . . . . . . . . . . 12  |-  ( u  =  ( N `  t )  ->  (
( ( <. (
t `  G ) ,  t >.  e.  ( I `  P )  /\  <. ( ( N `
 t ) `  D ) ,  u >.  e.  ( I `  Q ) )  /\  ( f  =  ( ( t `  G
)  o.  ( ( N `  t ) `
 D ) )  /\  s  =  ( t J u ) ) )  <->  ( ( <. ( t `  G
) ,  t >.  e.  ( I `  P
)  /\  <. ( ( N `  t ) `
 D ) ,  ( N `  t
) >.  e.  ( I `
 Q ) )  /\  ( f  =  ( ( t `  G )  o.  (
( N `  t
) `  D )
)  /\  s  =  ( t J ( N `  t ) ) ) ) ) )
10287, 94, 101syl3an9b 1334 . . . . . . . . . . 11  |-  ( ( g  =  ( t `
 G )  /\  h  =  ( ( N `  t ) `  D )  /\  u  =  ( N `  t ) )  -> 
( ( ( <.
g ,  t >.  e.  ( I `  P
)  /\  <. h ,  u >.  e.  (
I `  Q )
)  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) )  <-> 
( ( <. (
t `  G ) ,  t >.  e.  ( I `  P )  /\  <. ( ( N `
 t ) `  D ) ,  ( N `  t )
>.  e.  ( I `  Q ) )  /\  ( f  =  ( ( t `  G
)  o.  ( ( N `  t ) `
 D ) )  /\  s  =  ( t J ( N `
 t ) ) ) ) ) )
103102spc3egv 3171 . . . . . . . . . 10  |-  ( ( ( t `  G
)  e.  _V  /\  ( ( N `  t ) `  D
)  e.  _V  /\  ( N `  t )  e.  _V )  -> 
( ( ( <.
( t `  G
) ,  t >.  e.  ( I `  P
)  /\  <. ( ( N `  t ) `
 D ) ,  ( N `  t
) >.  e.  ( I `
 Q ) )  /\  ( f  =  ( ( t `  G )  o.  (
( N `  t
) `  D )
)  /\  s  =  ( t J ( N `  t ) ) ) )  ->  E. g E. h E. u ( ( <.
g ,  t >.  e.  ( I `  P
)  /\  <. h ,  u >.  e.  (
I `  Q )
)  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) ) ) )
10447, 57, 58, 103mp3an 1361 . . . . . . . . 9  |-  ( ( ( <. ( t `  G ) ,  t
>.  e.  ( I `  P )  /\  <. ( ( N `  t
) `  D ) ,  ( N `  t ) >.  e.  ( I `  Q ) )  /\  ( f  =  ( ( t `
 G )  o.  ( ( N `  t ) `  D
) )  /\  s  =  ( t J ( N `  t
) ) ) )  ->  E. g E. h E. u ( ( <.
g ,  t >.  e.  ( I `  P
)  /\  <. h ,  u >.  e.  (
I `  Q )
)  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) ) )
10551, 61, 74, 80, 104syl22anc 1266 . . . . . . . 8  |-  ( ( ( ph  /\  (
( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
)  /\  ( t  e.  E  /\  (
t `  ( G  o.  `' D ) )  =  f ) )  ->  E. g E. h E. u ( ( <.
g ,  t >.  e.  ( I `  P
)  /\  <. h ,  u >.  e.  (
I `  Q )
)  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) ) )
106105ex 436 . . . . . . 7  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  -> 
( ( t  e.  E  /\  ( t `
 ( G  o.  `' D ) )  =  f )  ->  E. g E. h E. u ( ( <. g ,  t
>.  e.  ( I `  P )  /\  <. h ,  u >.  e.  ( I `  Q ) )  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) ) ) )
107106eximdv 1755 . . . . . 6  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  -> 
( E. t ( t  e.  E  /\  ( t `  ( G  o.  `' D
) )  =  f )  ->  E. t E. g E. h E. u ( ( <.
g ,  t >.  e.  ( I `  P
)  /\  <. h ,  u >.  e.  (
I `  Q )
)  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) ) ) )
108 excom 1900 . . . . . 6  |-  ( E. t E. g E. h E. u ( ( <. g ,  t
>.  e.  ( I `  P )  /\  <. h ,  u >.  e.  ( I `  Q ) )  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) )  <->  E. g E. t E. h E. u ( ( <. g ,  t
>.  e.  ( I `  P )  /\  <. h ,  u >.  e.  ( I `  Q ) )  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) ) )
109107, 108syl6ib 230 . . . . 5  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  -> 
( E. t ( t  e.  E  /\  ( t `  ( G  o.  `' D
) )  =  f )  ->  E. g E. t E. h E. u ( ( <.
g ,  t >.  e.  ( I `  P
)  /\  <. h ,  u >.  e.  (
I `  Q )
)  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) ) ) )
11042, 109mpd 15 . . . 4  |-  ( (
ph  /\  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) )  ->  E. g E. t E. h E. u ( ( <. g ,  t
>.  e.  ( I `  P )  /\  <. h ,  u >.  e.  ( I `  Q ) )  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) ) )
111110ex 436 . . 3  |-  ( ph  ->  ( ( ( f  e.  T  /\  ( R `  f )  .<_  V )  /\  s  =  .0.  )  ->  E. g E. t E. h E. u ( ( <.
g ,  t >.  e.  ( I `  P
)  /\  <. h ,  u >.  e.  (
I `  Q )
)  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) ) ) )
1121simpld 461 . . . . . . . . 9  |-  ( ph  ->  K  e.  HL )
113 hllat 32892 . . . . . . . . 9  |-  ( K  e.  HL  ->  K  e.  Lat )
114112, 113syl 17 . . . . . . . 8  |-  ( ph  ->  K  e.  Lat )
11512simpld 461 . . . . . . . . 9  |-  ( ph  ->  P  e.  A )
11617simpld 461 . . . . . . . . 9  |-  ( ph  ->  Q  e.  A )
11728, 29, 8hlatjcl 32895 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .\/  Q
)  e.  B )
118112, 115, 116, 117syl3anc 1265 . . . . . . . 8  |-  ( ph  ->  ( P  .\/  Q
)  e.  B )
1191simprd 465 . . . . . . . . 9  |-  ( ph  ->  W  e.  H )
12028, 2lhpbase 33526 . . . . . . . . 9  |-  ( W  e.  H  ->  W  e.  B )
121119, 120syl 17 . . . . . . . 8  |-  ( ph  ->  W  e.  B )
12228, 30latmcl 16291 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( P  .\/  Q )  e.  B  /\  W  e.  B )  ->  (
( P  .\/  Q
)  ./\  W )  e.  B )
123114, 118, 121, 122syl3anc 1265 . . . . . . 7  |-  ( ph  ->  ( ( P  .\/  Q )  ./\  W )  e.  B )
12433, 123syl5eqel 2515 . . . . . 6  |-  ( ph  ->  V  e.  B )
12528, 7, 30latmle2 16316 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( P  .\/  Q )  e.  B  /\  W  e.  B )  ->  (
( P  .\/  Q
)  ./\  W )  .<_  W )
126114, 118, 121, 125syl3anc 1265 . . . . . . 7  |-  ( ph  ->  ( ( P  .\/  Q )  ./\  W )  .<_  W )
12733, 126syl5eqbr 4455 . . . . . 6  |-  ( ph  ->  V  .<_  W )
128 eqid 2423 . . . . . . 7  |-  ( (
DIsoB `  K ) `  W )  =  ( ( DIsoB `  K ) `  W )
12928, 7, 2, 3, 128dihvalb 34768 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( V  e.  B  /\  V  .<_  W ) )  ->  (
I `  V )  =  ( ( (
DIsoB `  K ) `  W ) `  V
) )
1301, 124, 127, 129syl12anc 1263 . . . . 5  |-  ( ph  ->  ( I `  V
)  =  ( ( ( DIsoB `  K ) `  W ) `  V
) )
131130eleq2d 2493 . . . 4  |-  ( ph  ->  ( <. f ,  s
>.  e.  ( I `  V )  <->  <. f ,  s >.  e.  (
( ( DIsoB `  K
) `  W ) `  V ) ) )
13228, 7, 2, 13, 34, 77, 128dibopelval3 34679 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( V  e.  B  /\  V  .<_  W ) )  ->  ( <. f ,  s >.  e.  ( ( ( DIsoB `  K ) `  W
) `  V )  <->  ( ( f  e.  T  /\  ( R `  f
)  .<_  V )  /\  s  =  .0.  )
) )
1331, 124, 127, 132syl12anc 1263 . . . 4  |-  ( ph  ->  ( <. f ,  s
>.  e.  ( ( (
DIsoB `  K ) `  W ) `  V
)  <->  ( ( f  e.  T  /\  ( R `  f )  .<_  V )  /\  s  =  .0.  ) ) )
134131, 133bitrd 257 . . 3  |-  ( ph  ->  ( <. f ,  s
>.  e.  ( I `  V )  <->  ( (
f  e.  T  /\  ( R `  f ) 
.<_  V )  /\  s  =  .0.  ) ) )
135 eqid 2423 . . . 4  |-  ( LSubSp `  U )  =  (
LSubSp `  U )
13628, 8atbase 32818 . . . . 5  |-  ( P  e.  A  ->  P  e.  B )
137115, 136syl 17 . . . 4  |-  ( ph  ->  P  e.  B )
13828, 8atbase 32818 . . . . 5  |-  ( Q  e.  A  ->  Q  e.  B )
139116, 138syl 17 . . . 4  |-  ( ph  ->  Q  e.  B )
14028, 2, 13, 35, 76, 31, 135, 32, 3, 1, 137, 139dihopellsm 34786 . . 3  |-  ( ph  ->  ( <. f ,  s
>.  e.  ( ( I `
 P )  .(+)  ( I `  Q ) )  <->  E. g E. t E. h E. u ( ( <. g ,  t
>.  e.  ( I `  P )  /\  <. h ,  u >.  e.  ( I `  Q ) )  /\  ( f  =  ( g  o.  h )  /\  s  =  ( t J u ) ) ) ) )
141111, 134, 1403imtr4d 272 . 2  |-  ( ph  ->  ( <. f ,  s
>.  e.  ( I `  V )  ->  <. f ,  s >.  e.  ( ( I `  P
)  .(+)  ( I `  Q ) ) ) )
1425, 141relssdv 4944 1  |-  ( ph  ->  ( I `  V
)  C_  ( (
I `  P )  .(+)  ( I `  Q
) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1438   E.wex 1660    e. wcel 1869   E.wrex 2777   _Vcvv 3082    C_ wss 3437   <.cop 4003   class class class wbr 4421    |-> cmpt 4480    _I cid 4761   `'ccnv 4850    |` cres 4853    o. ccom 4855   Rel wrel 4856   ` cfv 5599   iota_crio 6264  (class class class)co 6303    |-> cmpt2 6305   Basecbs 15114   lecple 15190   occoc 15191   joincjn 16182   meetcmee 16183   Latclat 16284   LSSumclsm 17279   LSubSpclss 18148   Atomscatm 32792   HLchlt 32879   LHypclh 33512   LTrncltrn 33629   trLctrl 33687   TEndoctendo 34282   DVecHcdvh 34609   DIsoBcdib 34669   DIsoHcdih 34759
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-riotaBAD 32488
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-iin 4300  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-tpos 6979  df-undef 7026  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-oadd 7192  df-er 7369  df-map 7480  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-nn 10612  df-2 10670  df-3 10671  df-4 10672  df-5 10673  df-6 10674  df-n0 10872  df-z 10940  df-uz 11162  df-fz 11787  df-struct 15116  df-ndx 15117  df-slot 15118  df-base 15119  df-sets 15120  df-ress 15121  df-plusg 15196  df-mulr 15197  df-sca 15199  df-vsca 15200  df-0g 15333  df-preset 16166  df-poset 16184  df-plt 16197  df-lub 16213  df-glb 16214  df-join 16215  df-meet 16216  df-p0 16278  df-p1 16279  df-lat 16285  df-clat 16347  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-submnd 16576  df-grp 16666  df-minusg 16667  df-sbg 16668  df-subg 16807  df-cntz 16964  df-lsm 17281  df-cmn 17425  df-abl 17426  df-mgp 17717  df-ur 17729  df-ring 17775  df-oppr 17844  df-dvdsr 17862  df-unit 17863  df-invr 17893  df-dvr 17904  df-drng 17970  df-lmod 18086  df-lss 18149  df-lsp 18188  df-lvec 18319  df-oposet 32705  df-ol 32707  df-oml 32708  df-covers 32795  df-ats 32796  df-atl 32827  df-cvlat 32851  df-hlat 32880  df-llines 33026  df-lplanes 33027  df-lvols 33028  df-lines 33029  df-psubsp 33031  df-pmap 33032  df-padd 33324  df-lhyp 33516  df-laut 33517  df-ldil 33632  df-ltrn 33633  df-trl 33688  df-tendo 34285  df-edring 34287  df-disoa 34560  df-dvech 34610  df-dib 34670  df-dic 34704  df-dih 34760
This theorem is referenced by:  dihjatcc  34953
  Copyright terms: Public domain W3C validator