dihjat

Description: Isomorphism H of lattice join of two atoms. (Contributed by NM, 29-Sep-2014)

	Ref	Expression
Hypotheses	dihjat.h	$⊢ H = LHyp (K)$
	dihjat.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihjat.a	$⊢ A = Atoms (K)$
	dihjat.u	$⊢ U = DVecH (K) (W)$
	dihjat.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihjat.i	$⊢ I = DIsoH (K) (W)$
	dihjat.k	$⊢ φ \to (K \in HL \land W \in H)$
	dihjat.p	$⊢ φ \to P \in A$
	dihjat.q	$⊢ φ \to Q \in A$
Assertion	dihjat	$⊢ φ \to I (P \underset{˙}{\lor} Q) = I (P) \underset{˙}{\oplus} I (Q)$

Proof

Step	Hyp	Ref	Expression
1		dihjat.h	$⊢ H = LHyp (K)$
2		dihjat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dihjat.a	$⊢ A = Atoms (K)$
4		dihjat.u	$⊢ U = DVecH (K) (W)$
5		dihjat.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
6		dihjat.i	$⊢ I = DIsoH (K) (W)$
7		dihjat.k	$⊢ φ \to (K \in HL \land W \in H)$
8		dihjat.p	$⊢ φ \to P \in A$
9		dihjat.q	$⊢ φ \to Q \in A$
10		eqid	$⊢ \leq_{K} = \leq_{K}$
11	7	adantr	$⊢ (φ \land (P \leq_{K} W \land Q \leq_{K} W)) \to (K \in HL \land W \in H)$
12	8	adantr	$⊢ (φ \land (P \leq_{K} W \land Q \leq_{K} W)) \to P \in A$
13		simprl	$⊢ (φ \land (P \leq_{K} W \land Q \leq_{K} W)) \to P \leq_{K} W$
14	12 13	jca	$⊢ (φ \land (P \leq_{K} W \land Q \leq_{K} W)) \to (P \in A \land P \leq_{K} W)$
15	9	adantr	$⊢ (φ \land (P \leq_{K} W \land Q \leq_{K} W)) \to Q \in A$
16		simprr	$⊢ (φ \land (P \leq_{K} W \land Q \leq_{K} W)) \to Q \leq_{K} W$
17	15 16	jca	$⊢ (φ \land (P \leq_{K} W \land Q \leq_{K} W)) \to (Q \in A \land Q \leq_{K} W)$
18	10 1 2 3 4 5 6 11 14 17	dihjatb	$⊢ (φ \land (P \leq_{K} W \land Q \leq_{K} W)) \to I (P \underset{˙}{\lor} Q) = I (P) \underset{˙}{\oplus} I (Q)$
19		eqid	$⊢ {Base}_{K} = {Base}_{K}$
20	7	adantr	$⊢ (φ \land (P \leq_{K} W \land \neg Q \leq_{K} W)) \to (K \in HL \land W \in H)$
21	19 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
22	8 21	syl	$⊢ φ \to P \in {Base}_{K}$
23	22	adantr	$⊢ (φ \land (P \leq_{K} W \land \neg Q \leq_{K} W)) \to P \in {Base}_{K}$
24		simprl	$⊢ (φ \land (P \leq_{K} W \land \neg Q \leq_{K} W)) \to P \leq_{K} W$
25	23 24	jca	$⊢ (φ \land (P \leq_{K} W \land \neg Q \leq_{K} W)) \to (P \in {Base}_{K} \land P \leq_{K} W)$
26	9	adantr	$⊢ (φ \land (P \leq_{K} W \land \neg Q \leq_{K} W)) \to Q \in A$
27		simprr	$⊢ (φ \land (P \leq_{K} W \land \neg Q \leq_{K} W)) \to \neg Q \leq_{K} W$
28	26 27	jca	$⊢ (φ \land (P \leq_{K} W \land \neg Q \leq_{K} W)) \to (Q \in A \land \neg Q \leq_{K} W)$
29	19 10 1 2 3 4 5 6 20 25 28	dihjatc	$⊢ (φ \land (P \leq_{K} W \land \neg Q \leq_{K} W)) \to I (P \underset{˙}{\lor} Q) = I (P) \underset{˙}{\oplus} I (Q)$
30	7	adantr	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to (K \in HL \land W \in H)$
31	19 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
32	9 31	syl	$⊢ φ \to Q \in {Base}_{K}$
33	32	adantr	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to Q \in {Base}_{K}$
34		simprr	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to Q \leq_{K} W$
35	33 34	jca	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to (Q \in {Base}_{K} \land Q \leq_{K} W)$
36	8	adantr	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to P \in A$
37		simprl	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to \neg P \leq_{K} W$
38	36 37	jca	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to (P \in A \land \neg P \leq_{K} W)$
39	19 10 1 2 3 4 5 6 30 35 38	dihjatc	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to I (Q \underset{˙}{\lor} P) = I (Q) \underset{˙}{\oplus} I (P)$
40	7	simpld	$⊢ φ \to K \in HL$
41	2 3	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
42	40 8 9 41	syl3anc	$⊢ φ \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
43	42	fveq2d	$⊢ φ \to I (P \underset{˙}{\lor} Q) = I (Q \underset{˙}{\lor} P)$
44	43	adantr	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to I (P \underset{˙}{\lor} Q) = I (Q \underset{˙}{\lor} P)$
45	1 4 7	dvhlmod	$⊢ φ \to U \in LMod$
46		lmodabl	$⊢ U \in LMod \to U \in Abel$
47	45 46	syl	$⊢ φ \to U \in Abel$
48		eqid	$⊢ LSubSp (U) = LSubSp (U)$
49	48	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
50	45 49	syl	$⊢ φ \to LSubSp (U) \subseteq SubGrp (U)$
51	19 1 6 4 48	dihlss	$⊢ ((K \in HL \land W \in H) \land P \in {Base}_{K}) \to I (P) \in LSubSp (U)$
52	7 22 51	syl2anc	$⊢ φ \to I (P) \in LSubSp (U)$
53	50 52	sseldd	$⊢ φ \to I (P) \in SubGrp (U)$
54	19 1 6 4 48	dihlss	$⊢ ((K \in HL \land W \in H) \land Q \in {Base}_{K}) \to I (Q) \in LSubSp (U)$
55	7 32 54	syl2anc	$⊢ φ \to I (Q) \in LSubSp (U)$
56	50 55	sseldd	$⊢ φ \to I (Q) \in SubGrp (U)$
57	5	lsmcom	$⊢ (U \in Abel \land I (P) \in SubGrp (U) \land I (Q) \in SubGrp (U)) \to I (P) \underset{˙}{\oplus} I (Q) = I (Q) \underset{˙}{\oplus} I (P)$
58	47 53 56 57	syl3anc	$⊢ φ \to I (P) \underset{˙}{\oplus} I (Q) = I (Q) \underset{˙}{\oplus} I (P)$
59	58	adantr	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to I (P) \underset{˙}{\oplus} I (Q) = I (Q) \underset{˙}{\oplus} I (P)$
60	39 44 59	3eqtr4d	$⊢ (φ \land (\neg P \leq_{K} W \land Q \leq_{K} W)) \to I (P \underset{˙}{\lor} Q) = I (P) \underset{˙}{\oplus} I (Q)$
61	7	adantr	$⊢ (φ \land (\neg P \leq_{K} W \land \neg Q \leq_{K} W)) \to (K \in HL \land W \in H)$
62	8	adantr	$⊢ (φ \land (\neg P \leq_{K} W \land \neg Q \leq_{K} W)) \to P \in A$
63		simprl	$⊢ (φ \land (\neg P \leq_{K} W \land \neg Q \leq_{K} W)) \to \neg P \leq_{K} W$
64	62 63	jca	$⊢ (φ \land (\neg P \leq_{K} W \land \neg Q \leq_{K} W)) \to (P \in A \land \neg P \leq_{K} W)$
65	9	adantr	$⊢ (φ \land (\neg P \leq_{K} W \land \neg Q \leq_{K} W)) \to Q \in A$
66		simprr	$⊢ (φ \land (\neg P \leq_{K} W \land \neg Q \leq_{K} W)) \to \neg Q \leq_{K} W$
67	65 66	jca	$⊢ (φ \land (\neg P \leq_{K} W \land \neg Q \leq_{K} W)) \to (Q \in A \land \neg Q \leq_{K} W)$
68	10 1 2 3 4 5 6 61 64 67	dihjatcc	$⊢ (φ \land (\neg P \leq_{K} W \land \neg Q \leq_{K} W)) \to I (P \underset{˙}{\lor} Q) = I (P) \underset{˙}{\oplus} I (Q)$
69	18 29 60 68	4casesdan	$⊢ φ \to I (P \underset{˙}{\lor} Q) = I (P) \underset{˙}{\oplus} I (Q)$

Metamath Proof Explorer

Theorem dihjat

Proof