Theorem dihjatcclem3

Description: Lemma for dihjatcc . (Contributed by NM, 28-Sep-2014)

	Ref	Expression
Hypotheses	dihjatcclem.b	$$⊢B={\mathrm{Base}}_K$$
	dihjatcclem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dihjatcclem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihjatcclem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dihjatcclem.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dihjatcclem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dihjatcclem.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihjatcclem.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dihjatcclem.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihjatcclem.v	$$⊢V=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
	dihjatcclem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dihjatcclem.p	$$⊢\phi \to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
	dihjatcclem.q	$$⊢\phi \to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
	dihjatcc.w	$$⊢C=\mathrm{oc}\left(K\right)\left(W\right)$$
	dihjatcc.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dihjatcc.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	dihjatcc.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dihjatcc.g	$$⊢G=\left(\iota d\in T|d\left(C\right)=P\right)$$
	dihjatcc.dd	$$⊢D=\left(\iota d\in T|d\left(C\right)=Q\right)$$
Assertion	dihjatcclem3	$$⊢\phi \to R\left(G\circ D^{-1}\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		dihjatcclem.b	$$⊢B={\mathrm{Base}}_K$$
2		dihjatcclem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dihjatcclem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dihjatcclem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
5		dihjatcclem.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
6		dihjatcclem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
7		dihjatcclem.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
8		dihjatcclem.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
9		dihjatcclem.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
10		dihjatcclem.v	$$⊢V=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
11		dihjatcclem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		dihjatcclem.p	$$⊢\phi \to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
13		dihjatcclem.q	$$⊢\phi \to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
14		dihjatcc.w	$$⊢C=\mathrm{oc}\left(K\right)\left(W\right)$$
15		dihjatcc.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
16		dihjatcc.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
17		dihjatcc.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
18		dihjatcc.g	$$⊢G=\left(\iota d\in T|d\left(C\right)=P\right)$$
19		dihjatcc.dd	$$⊢D=\left(\iota d\in T|d\left(C\right)=Q\right)$$
20	2 6 3 14	lhpocnel2	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \left(C\in A\wedge \neg C\underset{\dot{}}{\le }W\right)$$
21	11 20	syl	$$⊢\phi \to \left(C\in A\wedge \neg C\underset{\dot{}}{\le }W\right)$$
22	2 6 3 15 18	ltrniotacl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(C\in A\wedge \neg C\underset{\dot{}}{\le }W\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to G\in T$$
23	11 21 12 22	syl3anc	$$⊢\phi \to G\in T$$
24	2 6 3 15 19	ltrniotacl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(C\in A\wedge \neg C\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to D\in T$$
25	11 21 13 24	syl3anc	$$⊢\phi \to D\in T$$
26	3 15	ltrncnv	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge D\in T\right)\to D^{-1}\in T$$
27	11 25 26	syl2anc	$$⊢\phi \to D^{-1}\in T$$
28	3 15	ltrnco	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge G\in T\wedge D^{-1}\in T\right)\to G\circ D^{-1}\in T$$
29	11 23 27 28	syl3anc	$$⊢\phi \to G\circ D^{-1}\in T$$
30	2 4 5 6 3 15 16	trlval2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge G\circ D^{-1}\in T\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to R\left(G\circ D^{-1}\right)=\left(Q\underset{\dot{}}{\vee }\left(G\circ D^{-1}\right)\left(Q\right)\right)\underset{\dot{}}{\wedge }W$$
31	11 29 13 30	syl3anc	$$⊢\phi \to R\left(G\circ D^{-1}\right)=\left(Q\underset{\dot{}}{\vee }\left(G\circ D^{-1}\right)\left(Q\right)\right)\underset{\dot{}}{\wedge }W$$
32	13	simpld	$$⊢\phi \to Q\in A$$
33	2 6 3 15	ltrncoval	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(G\in T\wedge D^{-1}\in T\right)\wedge Q\in A\right)\to \left(G\circ D^{-1}\right)\left(Q\right)=G\left(D^{-1}\left(Q\right)\right)$$
34	11 23 27 32 33	syl121anc	$$⊢\phi \to \left(G\circ D^{-1}\right)\left(Q\right)=G\left(D^{-1}\left(Q\right)\right)$$
35	2 6 3 15 19	ltrniotacnvval	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(C\in A\wedge \neg C\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to D^{-1}\left(Q\right)=C$$
36	11 21 13 35	syl3anc	$$⊢\phi \to D^{-1}\left(Q\right)=C$$
37	36	fveq2d	$$⊢\phi \to G\left(D^{-1}\left(Q\right)\right)=G\left(C\right)$$
38	2 6 3 15 18	ltrniotaval	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(C\in A\wedge \neg C\underset{\dot{}}{\le }W\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\to G\left(C\right)=P$$
39	11 21 12 38	syl3anc	$$⊢\phi \to G\left(C\right)=P$$
40	37 39	eqtrd	$$⊢\phi \to G\left(D^{-1}\left(Q\right)\right)=P$$
41	34 40	eqtrd	$$⊢\phi \to \left(G\circ D^{-1}\right)\left(Q\right)=P$$
42	41	oveq2d	$$⊢\phi \to Q\underset{\dot{}}{\vee }\left(G\circ D^{-1}\right)\left(Q\right)=Q\underset{\dot{}}{\vee }P$$
43	11	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
44	12	simpld	$$⊢\phi \to P\in A$$
45	4 6	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to P\underset{\dot{}}{\vee }Q=Q\underset{\dot{}}{\vee }P$$
46	43 44 32 45	syl3anc	$$⊢\phi \to P\underset{\dot{}}{\vee }Q=Q\underset{\dot{}}{\vee }P$$
47	42 46	eqtr4d	$$⊢\phi \to Q\underset{\dot{}}{\vee }\left(G\circ D^{-1}\right)\left(Q\right)=P\underset{\dot{}}{\vee }Q$$
48	47	oveq1d	$$⊢\phi \to \left(Q\underset{\dot{}}{\vee }\left(G\circ D^{-1}\right)\left(Q\right)\right)\underset{\dot{}}{\wedge }W=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
49	48 10	eqtr4di	$$⊢\phi \to \left(Q\underset{\dot{}}{\vee }\left(G\circ D^{-1}\right)\left(Q\right)\right)\underset{\dot{}}{\wedge }W=V$$
50	31 49	eqtrd	$$⊢\phi \to R\left(G\circ D^{-1}\right)=V$$