dihjatcclem4

Description: Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 29-Sep-2014)

	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)$
	dihjatcc.n	$⊢ N = (a \in E ⟼ (d \in T ⟼ {a (d)}^{-1}))$
	dihjatcc.o	$⊢ \underset{˙}{0} = (d \in T ⟼ {I ↾}_{B})$
	dihjatcc.d	$⊢ J = (a \in E, b \in E ⟼ (d \in T ⟼ a (d) \circ b (d)))$
Assertion	dihjatcclem4	$⊢ φ \to I (V) \subseteq I (P) \underset{˙}{\oplus} I (Q)$

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		dihjatcc.n	$⊢ N = (a \in E ⟼ (d \in T ⟼ {a (d)}^{-1}))$
21		dihjatcc.o	$⊢ \underset{˙}{0} = (d \in T ⟼ {I ↾}_{B})$
22		dihjatcc.d	$⊢ J = (a \in E, b \in E ⟼ (d \in T ⟼ a (d) \circ b (d)))$
23	3 9	dihvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (V)$
24	11 23	syl	$⊢ φ \to Rel I (V)$
25	11	adantr	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to (K \in HL \land W \in H)$
26	2 6 3 14	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (C \in A \land \neg C \underset{˙}{\leq} W)$
27	11 26	syl	$⊢ φ \to (C \in A \land \neg C \underset{˙}{\leq} W)$
28	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$
29	11 27 12 28	syl3anc	$⊢ φ \to G \in T$
30	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$
31	11 27 13 30	syl3anc	$⊢ φ \to D \in T$
32	3 15	ltrncnv	$⊢ ((K \in HL \land W \in H) \land D \in T) \to D^{-1} \in T$
33	11 31 32	syl2anc	$⊢ φ \to D^{-1} \in T$
34	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$
35	11 29 33 34	syl3anc	$⊢ φ \to G \circ D^{-1} \in T$
36	35	adantr	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to G \circ D^{-1} \in T$
37		simprll	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to f \in T$
38		simprlr	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to R (f) \underset{˙}{\leq} V$
39	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	dihjatcclem3	$⊢ φ \to R (G \circ D^{-1}) = V$
40	39	adantr	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to R (G \circ D^{-1}) = V$
41	38 40	breqtrrd	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to R (f) \underset{˙}{\leq} R (G \circ D^{-1})$
42	2 3 15 16 17	tendoex	$⊢ ((K \in HL \land W \in H) \land (G \circ D^{-1} \in T \land f \in T) \land R (f) \underset{˙}{\leq} R (G \circ D^{-1})) \to \exists t \in E t (G \circ D^{-1}) = f$
43	25 36 37 41 42	syl121anc	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to \exists t \in E t (G \circ D^{-1}) = f$
44		df-rex	$⊢ \exists t \in E t (G \circ D^{-1}) = f \leftrightarrow \exists t (t \in E \land t (G \circ D^{-1}) = f)$
45	43 44	sylib	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to \exists t (t \in E \land t (G \circ D^{-1}) = f)$
46		eqidd	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to t (G) = t (G)$
47		simprl	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to t \in E$
48	11	ad2antrr	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to (K \in HL \land W \in H)$
49	12	ad2antrr	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
50		fvex	$⊢ t (G) \in V$
51		vex	$⊢ t \in V$
52	2 6 3 14 15 17 9 18 50 51	dihopelvalcqat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (⟨t (G), t⟩ \in I (P) \leftrightarrow (t (G) = t (G) \land t \in E))$
53	48 49 52	syl2anc	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to (⟨t (G), t⟩ \in I (P) \leftrightarrow (t (G) = t (G) \land t \in E))$
54	46 47 53	mpbir2and	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to ⟨t (G), t⟩ \in I (P)$
55		eqidd	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to N (t) (D) = N (t) (D)$
56	3 15 17 20	tendoicl	$⊢ ((K \in HL \land W \in H) \land t \in E) \to N (t) \in E$
57	48 47 56	syl2anc	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to N (t) \in E$
58	13	ad2antrr	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
59		fvex	$⊢ N (t) (D) \in V$
60		fvex	$⊢ N (t) \in V$
61	2 6 3 14 15 17 9 19 59 60	dihopelvalcqat	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨N (t) (D), N (t)⟩ \in I (Q) \leftrightarrow (N (t) (D) = N (t) (D) \land N (t) \in E))$
62	48 58 61	syl2anc	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to (⟨N (t) (D), N (t)⟩ \in I (Q) \leftrightarrow (N (t) (D) = N (t) (D) \land N (t) \in E))$
63	55 57 62	mpbir2and	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to ⟨N (t) (D), N (t)⟩ \in I (Q)$
64	29	ad2antrr	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to G \in T$
65	33	ad2antrr	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to D^{-1} \in T$
66	3 15 17	tendospdi1	$⊢ ((K \in HL \land W \in H) \land (t \in E \land G \in T \land D^{-1} \in T)) \to t (G \circ D^{-1}) = t (G) \circ t (D^{-1})$
67	48 47 64 65 66	syl13anc	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to t (G \circ D^{-1}) = t (G) \circ t (D^{-1})$
68		simprr	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to t (G \circ D^{-1}) = f$
69	31	ad2antrr	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to D \in T$
70	20 15	tendoi2	$⊢ (t \in E \land D \in T) \to N (t) (D) = {t (D)}^{-1}$
71	47 69 70	syl2anc	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to N (t) (D) = {t (D)}^{-1}$
72	3 15 17	tendocnv	$⊢ ((K \in HL \land W \in H) \land t \in E \land D \in T) \to {t (D)}^{-1} = t (D^{-1})$
73	48 47 69 72	syl3anc	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to {t (D)}^{-1} = t (D^{-1})$
74	71 73	eqtr2d	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to t (D^{-1}) = N (t) (D)$
75	74	coeq2d	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to t (G) \circ t (D^{-1}) = t (G) \circ N (t) (D)$
76	67 68 75	3eqtr3d	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to f = t (G) \circ N (t) (D)$
77		simplrr	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to s = \underset{˙}{0}$
78	3 15 17 20 1 22 21	tendoipl2	$⊢ ((K \in HL \land W \in H) \land t \in E) \to t J N (t) = \underset{˙}{0}$
79	48 47 78	syl2anc	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to t J N (t) = \underset{˙}{0}$
80	77 79	eqtr4d	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to s = t J N (t)$
81		opeq1	$⊢ g = t (G) \to ⟨g, t⟩ = ⟨t (G), t⟩$
82	81	eleq1d	$⊢ g = t (G) \to (⟨g, t⟩ \in I (P) \leftrightarrow ⟨t (G), t⟩ \in I (P))$
83	82	anbi1d	$⊢ g = t (G) \to ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \leftrightarrow (⟨t (G), t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)))$
84		coeq1	$⊢ g = t (G) \to g \circ h = t (G) \circ h$
85	84	eqeq2d	$⊢ g = t (G) \to (f = g \circ h \leftrightarrow f = t (G) \circ h)$
86	85	anbi1d	$⊢ g = t (G) \to ((f = g \circ h \land s = t J u) \leftrightarrow (f = t (G) \circ h \land s = t J u))$
87	83 86	anbi12d	$⊢ g = t (G) \to (((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u)) \leftrightarrow ((⟨t (G), t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = t (G) \circ h \land s = t J u)))$
88		opeq1	$⊢ h = N (t) (D) \to ⟨h, u⟩ = ⟨N (t) (D), u⟩$
89	88	eleq1d	$⊢ h = N (t) (D) \to (⟨h, u⟩ \in I (Q) \leftrightarrow ⟨N (t) (D), u⟩ \in I (Q))$
90	89	anbi2d	$⊢ h = N (t) (D) \to ((⟨t (G), t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \leftrightarrow (⟨t (G), t⟩ \in I (P) \land ⟨N (t) (D), u⟩ \in I (Q)))$
91		coeq2	$⊢ h = N (t) (D) \to t (G) \circ h = t (G) \circ N (t) (D)$
92	91	eqeq2d	$⊢ h = N (t) (D) \to (f = t (G) \circ h \leftrightarrow f = t (G) \circ N (t) (D))$
93	92	anbi1d	$⊢ h = N (t) (D) \to ((f = t (G) \circ h \land s = t J u) \leftrightarrow (f = t (G) \circ N (t) (D) \land s = t J u))$
94	90 93	anbi12d	$⊢ h = N (t) (D) \to (((⟨t (G), t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = t (G) \circ h \land s = t J u)) \leftrightarrow ((⟨t (G), t⟩ \in I (P) \land ⟨N (t) (D), u⟩ \in I (Q)) \land (f = t (G) \circ N (t) (D) \land s = t J u)))$
95		opeq2	$⊢ u = N (t) \to ⟨N (t) (D), u⟩ = ⟨N (t) (D), N (t)⟩$
96	95	eleq1d	$⊢ u = N (t) \to (⟨N (t) (D), u⟩ \in I (Q) \leftrightarrow ⟨N (t) (D), N (t)⟩ \in I (Q))$
97	96	anbi2d	$⊢ u = N (t) \to ((⟨t (G), t⟩ \in I (P) \land ⟨N (t) (D), u⟩ \in I (Q)) \leftrightarrow (⟨t (G), t⟩ \in I (P) \land ⟨N (t) (D), N (t)⟩ \in I (Q)))$
98		oveq2	$⊢ u = N (t) \to t J u = t J N (t)$
99	98	eqeq2d	$⊢ u = N (t) \to (s = t J u \leftrightarrow s = t J N (t))$
100	99	anbi2d	$⊢ u = N (t) \to ((f = t (G) \circ N (t) (D) \land s = t J u) \leftrightarrow (f = t (G) \circ N (t) (D) \land s = t J N (t)))$
101	97 100	anbi12d	$⊢ u = N (t) \to (((⟨t (G), t⟩ \in I (P) \land ⟨N (t) (D), u⟩ \in I (Q)) \land (f = t (G) \circ N (t) (D) \land s = t J u)) \leftrightarrow ((⟨t (G), t⟩ \in I (P) \land ⟨N (t) (D), N (t)⟩ \in I (Q)) \land (f = t (G) \circ N (t) (D) \land s = t J N (t))))$
102	87 94 101	syl3an9b	$⊢ (g = t (G) \land h = N (t) (D) \land u = N (t)) \to (((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u)) \leftrightarrow ((⟨t (G), t⟩ \in I (P) \land ⟨N (t) (D), N (t)⟩ \in I (Q)) \land (f = t (G) \circ N (t) (D) \land s = t J N (t))))$
103	102	spc3egv	$⊢ (t (G) \in V \land N (t) (D) \in V \land N (t) \in V) \to (((⟨t (G), t⟩ \in I (P) \land ⟨N (t) (D), N (t)⟩ \in I (Q)) \land (f = t (G) \circ N (t) (D) \land s = t J N (t))) \to \exists g \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u)))$
104	50 59 60 103	mp3an	$⊢ ((⟨t (G), t⟩ \in I (P) \land ⟨N (t) (D), N (t)⟩ \in I (Q)) \land (f = t (G) \circ N (t) (D) \land s = t J N (t))) \to \exists g \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u))$
105	54 63 76 80 104	syl22anc	$⊢ ((φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \land (t \in E \land t (G \circ D^{-1}) = f)) \to \exists g \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u))$
106	105	ex	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to ((t \in E \land t (G \circ D^{-1}) = f) \to \exists g \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u)))$
107	106	eximdv	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to (\exists t (t \in E \land t (G \circ D^{-1}) = f) \to \exists t \exists g \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u)))$
108		excom	$⊢ \exists t \exists g \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u)) \leftrightarrow \exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u))$
109	107 108	syl6ib	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to (\exists t (t \in E \land t (G \circ D^{-1}) = f) \to \exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u)))$
110	45 109	mpd	$⊢ (φ \land ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0})) \to \exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u))$
111	110	ex	$⊢ φ \to (((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0}) \to \exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u)))$
112	11	simpld	$⊢ φ \to K \in HL$
113	112	hllatd	$⊢ φ \to K \in Lat$
114	12	simpld	$⊢ φ \to P \in A$
115	13	simpld	$⊢ φ \to Q \in A$
116	1 4 6	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in B$
117	112 114 115 116	syl3anc	$⊢ φ \to P \underset{˙}{\lor} Q \in B$
118	11	simprd	$⊢ φ \to W \in H$
119	1 3	lhpbase	$⊢ W \in H \to W \in B$
120	118 119	syl	$⊢ φ \to W \in B$
121	1 5	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in B \land W \in B) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in B$
122	113 117 120 121	syl3anc	$⊢ φ \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in B$
123	10 122	eqeltrid	$⊢ φ \to V \in B$
124	1 2 5	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in B \land W \in B) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
125	113 117 120 124	syl3anc	$⊢ φ \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
126	10 125	eqbrtrid	$⊢ φ \to V \underset{˙}{\leq} W$
127		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
128	1 2 3 9 127	dihvalb	$⊢ ((K \in HL \land W \in H) \land (V \in B \land V \underset{˙}{\leq} W)) \to I (V) = DIsoB (K) (W) (V)$
129	11 123 126 128	syl12anc	$⊢ φ \to I (V) = DIsoB (K) (W) (V)$
130	129	eleq2d	$⊢ φ \to (⟨f, s⟩ \in I (V) \leftrightarrow ⟨f, s⟩ \in DIsoB (K) (W) (V))$
131	1 2 3 15 16 21 127	dibopelval3	$⊢ ((K \in HL \land W \in H) \land (V \in B \land V \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in DIsoB (K) (W) (V) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0}))$
132	11 123 126 131	syl12anc	$⊢ φ \to (⟨f, s⟩ \in DIsoB (K) (W) (V) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0}))$
133	130 132	bitrd	$⊢ φ \to (⟨f, s⟩ \in I (V) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} V) \land s = \underset{˙}{0}))$
134		eqid	$⊢ LSubSp (U) = LSubSp (U)$
135	1 6	atbase	$⊢ P \in A \to P \in B$
136	114 135	syl	$⊢ φ \to P \in B$
137	1 6	atbase	$⊢ Q \in A \to Q \in B$
138	115 137	syl	$⊢ φ \to Q \in B$
139	1 3 15 17 22 7 134 8 9 11 136 138	dihopellsm	$⊢ φ \to (⟨f, s⟩ \in (I (P) \underset{˙}{\oplus} I (Q)) \leftrightarrow \exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (P) \land ⟨h, u⟩ \in I (Q)) \land (f = g \circ h \land s = t J u)))$
140	111 133 139	3imtr4d	$⊢ φ \to (⟨f, s⟩ \in I (V) \to ⟨f, s⟩ \in (I (P) \underset{˙}{\oplus} I (Q)))$
141	24 140	relssdv	$⊢ φ \to I (V) \subseteq I (P) \underset{˙}{\oplus} I (Q)$

Metamath Proof Explorer

Theorem dihjatcclem4

Proof