dihjatcclem3

	Ref	Expression
Hypotheses	dihjatcclem.b	$⊢ B = {Base}_{K}$
	dihjatcclem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihjatcclem.h	$⊢ H = LHyp (K)$
	dihjatcclem.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihjatcclem.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihjatcclem.a	$⊢ A = Atoms (K)$
	dihjatcclem.u	$⊢ U = DVecH (K) (W)$
	dihjatcclem.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihjatcclem.i	$⊢ I = DIsoH (K) (W)$
	dihjatcclem.v	$⊢ V = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	dihjatcclem.k	$⊢ φ \to (K \in HL \land W \in H)$
	dihjatcclem.p	$⊢ φ \to (P \in A \land \neg P \underset{˙}{\leq} W)$
	dihjatcclem.q	$⊢ φ \to (Q \in A \land \neg Q \underset{˙}{\leq} 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 = (ι d \in T \| d (C) = P)$
	dihjatcc.dd	$⊢ D = (ι d \in T \| d (C) = Q)$
Assertion	dihjatcclem3	$⊢ φ \to R (G \circ D^{-1}) = V$

Proof

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

Metamath Proof Explorer

Theorem dihjatcclem3

Proof