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.

Step	Hyp	Ref	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 )
4	2, 3	dihvalrel 34810	. . 3 |- ( ( K e. HL /\ W e. H ) -> Rel ( I ` V ) )
5	1, 4	syl 17	. 2 |- ( ph -> Rel ( I ` V ) )
6	1	adantr 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 )
10	7, 8, 2, 9	lhpocnel2 33547	. . . . . . . . . . 11 |- ( ( K e. HL /\ W e. H ) -> ( C e. A /\ -. C .<_ W ) )
11	1, 10	syl 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 )
15	7, 8, 2, 13, 14	ltrniotacl 34109	. . . . . . . . . 10 |- ( ( ( K e. HL /\ W e. H ) /\ ( C e. A /\ -. C .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> G e. T )
16	1, 11, 12, 15	syl3anc 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 )
19	7, 8, 2, 13, 18	ltrniotacl 34109	. . . . . . . . . . 11 |- ( ( ( K e. HL /\ W e. H ) /\ ( C e. A /\ -. C .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> D e. T )
20	1, 11, 17, 19	syl3anc 1265	. . . . . . . . . 10 |- ( ph -> D e. T )
21	2, 13	ltrncnv 33674	. . . . . . . . . 10 |- ( ( ( K e. HL /\ W e. H ) /\ D e. T ) -> `' D e. T )
22	1, 20, 21	syl2anc 666	. . . . . . . . 9 |- ( ph -> `' D e. T )
23	2, 13	ltrnco 34249	. . . . . . . . 9 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ `' D e. T ) -> ( G o. `' D ) e. T )
24	1, 16, 22, 23	syl3anc 1265	. . . . . . . 8 |- ( ph -> ( G o. `' D ) e. T )
25	24	adantr 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 )
36	28, 7, 2, 29, 30, 8, 31, 32, 3, 33, 1, 12, 17, 9, 13, 34, 35, 14, 18	dihjatcclem3 34951	. . . . . . . . 9 |- ( ph -> ( R ` ( G o. `' D ) ) = V )
37	36	adantr 467	. . . . . . . 8 |- ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> ( R ` ( G o. `' D ) ) = V )
38	27, 37	breqtrrd 4448	. . . . . . 7 |- ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> ( R ` f ) .<_ ( R ` ( G o. `' D ) ) )
39	7, 2, 13, 34, 35	tendoex 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 )
40	6, 25, 26, 38, 39	syl121anc 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 ) )
42	40, 41	sylib 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 )
45	1	ad2antrr 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 ) )
46	12	ad2antrr 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
49	7, 8, 2, 9, 13, 35, 3, 14, 47, 48	dihopelvalcqat 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 ) ) )
50	45, 46, 49	syl2anc 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 ) ) )
51	43, 44, 50	mpbir2and 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 ) ) )
54	2, 13, 35, 53	tendoicl 34326	. . . . . . . . . . 11 |- ( ( ( K e. HL /\ W e. H ) /\ t e. E ) -> ( N ` t ) e. E )
55	45, 44, 54	syl2anc 666	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( N ` t ) e. E )
56	17	ad2antrr 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
59	7, 8, 2, 9, 13, 35, 3, 18, 57, 58	dihopelvalcqat 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 ) ) )
60	45, 56, 59	syl2anc 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 ) ) )
61	52, 55, 60	mpbir2and 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 ) )
62	16	ad2antrr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> G e. T )
63	22	ad2antrr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> `' D e. T )
64	2, 13, 35	tendospdi1 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 ) ) )
65	45, 44, 62, 63, 64	syl13anc 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 )
67	20	ad2antrr 731	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> D e. T )
68	53, 13	tendoi2 34325	. . . . . . . . . . . . 13 |- ( ( t e. E /\ D e. T ) -> ( ( N ` t ) ` D ) = `' ( t ` D ) )
69	44, 67, 68	syl2anc 666	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( ( N ` t ) ` D ) = `' ( t ` D ) )
70	2, 13, 35	tendocnv 34552	. . . . . . . . . . . . 13 |- ( ( ( K e. HL /\ W e. H ) /\ t e. E /\ D e. T ) -> `' ( t ` D ) = ( t ` `' D ) )
71	45, 44, 67, 70	syl3anc 1265	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> `' ( t ` D ) = ( t ` `' D ) )
72	69, 71	eqtr2d 2465	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( t ` `' D ) = ( ( N ` t ) ` D ) )
73	72	coeq2d 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 ) ) )
74	65, 66, 73	3eqtr3d 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 ) )
78	2, 13, 35, 53, 28, 76, 77	tendoipl2 34328	. . . . . . . . . . 11 |- ( ( ( K e. HL /\ W e. H ) /\ t e. E ) -> ( t J ( N ` t ) ) = .0. )
79	45, 44, 78	syl2anc 666	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( t J ( N ` t ) ) = .0. )
80	75, 79	eqtr4d 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 >. )
82	81	eleq1d 2492	. . . . . . . . . . . . . 14 |- ( g = ( t ` G ) -> ( <. g , t >. e. ( I ` P ) <-> <. ( t ` G ) , t >. e. ( I ` P ) ) )
83	82	anbi1d 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 ) )
85	84	eqeq2d 2437	. . . . . . . . . . . . . 14 |- ( g = ( t ` G ) -> ( f = ( g o. h ) <-> f = ( ( t ` G ) o. h ) ) )
86	85	anbi1d 710	. . . . . . . . . . . . 13 |- ( g = ( t ` G ) -> ( ( f = ( g o. h ) /\ s = ( t J u ) ) <-> ( f = ( ( t ` G ) o. h ) /\ s = ( t J u ) ) ) )
87	83, 86	anbi12d 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 >. )
89	88	eleq1d 2492	. . . . . . . . . . . . . 14 |- ( h = ( ( N ` t ) ` D ) -> ( <. h , u >. e. ( I ` Q ) <-> <. ( ( N ` t ) ` D ) , u >. e. ( I ` Q ) ) )
90	89	anbi2d 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 ) ) )
92	91	eqeq2d 2437	. . . . . . . . . . . . . 14 |- ( h = ( ( N ` t ) ` D ) -> ( f = ( ( t ` G ) o. h ) <-> f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) ) )
93	92	anbi1d 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 ) ) ) )
94	90, 93	anbi12d 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 ) >. )
96	95	eleq1d 2492	. . . . . . . . . . . . . 14 |- ( u = ( N ` t ) -> ( <. ( ( N ` t ) ` D ) , u >. e. ( I ` Q ) <-> <. ( ( N ` t ) ` D ) , ( N ` t ) >. e. ( I ` Q ) ) )
97	96	anbi2d 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 ) ) )
99	98	eqeq2d 2437	. . . . . . . . . . . . . 14 |- ( u = ( N ` t ) -> ( s = ( t J u ) <-> s = ( t J ( N ` t ) ) ) )
100	99	anbi2d 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 ) ) ) ) )
101	97, 100	anbi12d 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 ) ) ) ) ) )
102	87, 94, 101	syl3an9b 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 ) ) ) ) ) )
103	102	spc3egv 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 ) ) ) ) )
104	47, 57, 58, 103	mp3an 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 ) ) ) )
105	51, 61, 74, 80, 104	syl22anc 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 ) ) ) )
106	105	ex 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 ) ) ) ) )
107	106	eximdv 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 ) ) ) )
109	107, 108	syl6ib 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 ) ) ) ) )
110	42, 109	mpd 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 ) ) ) )
111	110	ex 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 ) ) ) ) )
112	1	simpld 461	. . . . . . . . 9 |- ( ph -> K e. HL )
113		hllat 32892	. . . . . . . . 9 |- ( K e. HL -> K e. Lat )
114	112, 113	syl 17	. . . . . . . 8 |- ( ph -> K e. Lat )
115	12	simpld 461	. . . . . . . . 9 |- ( ph -> P e. A )
116	17	simpld 461	. . . . . . . . 9 |- ( ph -> Q e. A )
117	28, 29, 8	hlatjcl 32895	. . . . . . . . 9 |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. B )
118	112, 115, 116, 117	syl3anc 1265	. . . . . . . 8 |- ( ph -> ( P .\/ Q ) e. B )
119	1	simprd 465	. . . . . . . . 9 |- ( ph -> W e. H )
120	28, 2	lhpbase 33526	. . . . . . . . 9 |- ( W e. H -> W e. B )
121	119, 120	syl 17	. . . . . . . 8 |- ( ph -> W e. B )
122	28, 30	latmcl 16291	. . . . . . . 8 |- ( ( K e. Lat /\ ( P .\/ Q ) e. B /\ W e. B ) -> ( ( P .\/ Q ) ./\ W ) e. B )
123	114, 118, 121, 122	syl3anc 1265	. . . . . . 7 |- ( ph -> ( ( P .\/ Q ) ./\ W ) e. B )
124	33, 123	syl5eqel 2515	. . . . . 6 |- ( ph -> V e. B )
125	28, 7, 30	latmle2 16316	. . . . . . . 8 |- ( ( K e. Lat /\ ( P .\/ Q ) e. B /\ W e. B ) -> ( ( P .\/ Q ) ./\ W ) .<_ W )
126	114, 118, 121, 125	syl3anc 1265	. . . . . . 7 |- ( ph -> ( ( P .\/ Q ) ./\ W ) .<_ W )
127	33, 126	syl5eqbr 4455	. . . . . 6 |- ( ph -> V .<_ W )
128		eqid 2423	. . . . . . 7 |- ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
129	28, 7, 2, 3, 128	dihvalb 34768	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( V e. B /\ V .<_ W ) ) -> ( I ` V ) = ( ( ( DIsoB ` K ) ` W ) ` V ) )
130	1, 124, 127, 129	syl12anc 1263	. . . . 5 |- ( ph -> ( I ` V ) = ( ( ( DIsoB ` K ) ` W ) ` V ) )
131	130	eleq2d 2493	. . . 4 |- ( ph -> ( <. f , s >. e. ( I ` V ) <-> <. f , s >. e. ( ( ( DIsoB ` K ) ` W ) ` V ) ) )
132	28, 7, 2, 13, 34, 77, 128	dibopelval3 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. ) ) )
133	1, 124, 127, 132	syl12anc 1263	. . . 4 |- ( ph -> ( <. f , s >. e. ( ( ( DIsoB ` K ) ` W ) ` V ) <-> ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) )
134	131, 133	bitrd 257	. . 3 |- ( ph -> ( <. f , s >. e. ( I ` V ) <-> ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) )
135		eqid 2423	. . . 4 |- ( LSubSp ` U ) = ( LSubSp ` U )
136	28, 8	atbase 32818	. . . . 5 |- ( P e. A -> P e. B )
137	115, 136	syl 17	. . . 4 |- ( ph -> P e. B )
138	28, 8	atbase 32818	. . . . 5 |- ( Q e. A -> Q e. B )
139	116, 138	syl 17	. . . 4 |- ( ph -> Q e. B )
140	28, 2, 13, 35, 76, 31, 135, 32, 3, 1, 137, 139	dihopellsm 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 ) ) ) ) )
141	111, 134, 140	3imtr4d 272	. 2 |- ( ph -> ( <. f , s >. e. ( I ` V ) -> <. f , s >. e. ( ( I ` P ) .(+) ( I ` Q ) ) ) )
142	5, 141	relssdv 4944	1 |- ( ph -> ( I ` V ) C_ ( ( I ` P ) .(+) ( I ` Q ) ) )

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