pwssplit4

Description: Splitting for structure powers 4: maps isomorphically onto the other half. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Hypotheses	pwssplit4.e	$⊢ E = R ↑_{𝑠} (A \cup B)$
	pwssplit4.g	$⊢ G = {Base}_{E}$
	pwssplit4.z	$⊢ \underset{˙}{0} = 0_{R}$
	pwssplit4.k	$⊢ K = \{y \in G \| {y ↾}_{A} = A \times \{\underset{˙}{0}\}\}$
	pwssplit4.f	$⊢ F = (x \in K ⟼ {x ↾}_{B})$
	pwssplit4.c	$⊢ C = R ↑_{𝑠} A$
	pwssplit4.d	$⊢ D = R ↑_{𝑠} B$
	pwssplit4.l	$⊢ L = E ↾_{𝑠} K$
Assertion	pwssplit4	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to F \in (L LMIso D)$

Proof

Step	Hyp	Ref	Expression
1		pwssplit4.e	$⊢ E = R ↑_{𝑠} (A \cup B)$
2		pwssplit4.g	$⊢ G = {Base}_{E}$
3		pwssplit4.z	$⊢ \underset{˙}{0} = 0_{R}$
4		pwssplit4.k	$⊢ K = \{y \in G \| {y ↾}_{A} = A \times \{\underset{˙}{0}\}\}$
5		pwssplit4.f	$⊢ F = (x \in K ⟼ {x ↾}_{B})$
6		pwssplit4.c	$⊢ C = R ↑_{𝑠} A$
7		pwssplit4.d	$⊢ D = R ↑_{𝑠} B$
8		pwssplit4.l	$⊢ L = E ↾_{𝑠} K$
9		ssrab2	$⊢ \{y \in G \| {y ↾}_{A} = A \times \{\underset{˙}{0}\}\} \subseteq G$
10	4 9	eqsstri	$⊢ K \subseteq G$
11		resmpt	$⊢ K \subseteq G \to {(x \in G ⟼ {x ↾}_{B}) ↾}_{K} = (x \in K ⟼ {x ↾}_{B})$
12	10 11	ax-mp	$⊢ {(x \in G ⟼ {x ↾}_{B}) ↾}_{K} = (x \in K ⟼ {x ↾}_{B})$
13	5 12	eqtr4i	$⊢ F = {(x \in G ⟼ {x ↾}_{B}) ↾}_{K}$
14		ssun2	$⊢ B \subseteq A \cup B$
15	14	a1i	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to B \subseteq A \cup B$
16		eqid	$⊢ {Base}_{D} = {Base}_{D}$
17		eqid	$⊢ (x \in G ⟼ {x ↾}_{B}) = (x \in G ⟼ {x ↾}_{B})$
18	1 7 2 16 17	pwssplit3	$⊢ (R \in LMod \land A \cup B \in V \land B \subseteq A \cup B) \to (x \in G ⟼ {x ↾}_{B}) \in (E LMHom D)$
19	15 18	syld3an3	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to (x \in G ⟼ {x ↾}_{B}) \in (E LMHom D)$
20		simp1	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to R \in LMod$
21		lmodgrp	$⊢ R \in LMod \to R \in Grp$
22		grpmnd	$⊢ R \in Grp \to R \in Mnd$
23	20 21 22	3syl	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to R \in Mnd$
24		ssun1	$⊢ A \subseteq A \cup B$
25		ssexg	$⊢ (A \subseteq A \cup B \land A \cup B \in V) \to A \in V$
26	24 25	mpan	$⊢ A \cup B \in V \to A \in V$
27	26	3ad2ant2	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to A \in V$
28	6 3	pws0g	$⊢ (R \in Mnd \land A \in V) \to A \times \{\underset{˙}{0}\} = 0_{C}$
29	23 27 28	syl2anc	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to A \times \{\underset{˙}{0}\} = 0_{C}$
30	29	eqeq2d	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to ({y ↾}_{A} = A \times \{\underset{˙}{0}\} \leftrightarrow {y ↾}_{A} = 0_{C})$
31	30	rabbidv	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to \{y \in G \| {y ↾}_{A} = A \times \{\underset{˙}{0}\}\} = \{y \in G \| {y ↾}_{A} = 0_{C}\}$
32	4 31	syl5eq	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to K = \{y \in G \| {y ↾}_{A} = 0_{C}\}$
33	24	a1i	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to A \subseteq A \cup B$
34		eqid	$⊢ {Base}_{C} = {Base}_{C}$
35		eqid	$⊢ (y \in G ⟼ {y ↾}_{A}) = (y \in G ⟼ {y ↾}_{A})$
36	1 6 2 34 35	pwssplit3	$⊢ (R \in LMod \land A \cup B \in V \land A \subseteq A \cup B) \to (y \in G ⟼ {y ↾}_{A}) \in (E LMHom C)$
37	33 36	syld3an3	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to (y \in G ⟼ {y ↾}_{A}) \in (E LMHom C)$
38		fvex	$⊢ 0_{C} \in V$
39	35	mptiniseg	$⊢ 0_{C} \in V \to {(y \in G ⟼ {y ↾}_{A})}^{-1} [\{0_{C}\}] = \{y \in G \| {y ↾}_{A} = 0_{C}\}$
40	38 39	ax-mp	$⊢ {(y \in G ⟼ {y ↾}_{A})}^{-1} [\{0_{C}\}] = \{y \in G \| {y ↾}_{A} = 0_{C}\}$
41	40	eqcomi	$⊢ \{y \in G \| {y ↾}_{A} = 0_{C}\} = {(y \in G ⟼ {y ↾}_{A})}^{-1} [\{0_{C}\}]$
42		eqid	$⊢ 0_{C} = 0_{C}$
43		eqid	$⊢ LSubSp (E) = LSubSp (E)$
44	41 42 43	lmhmkerlss	$⊢ (y \in G ⟼ {y ↾}_{A}) \in (E LMHom C) \to \{y \in G \| {y ↾}_{A} = 0_{C}\} \in LSubSp (E)$
45	37 44	syl	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to \{y \in G \| {y ↾}_{A} = 0_{C}\} \in LSubSp (E)$
46	32 45	eqeltrd	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to K \in LSubSp (E)$
47	43 8	reslmhm	$⊢ ((x \in G ⟼ {x ↾}_{B}) \in (E LMHom D) \land K \in LSubSp (E)) \to {(x \in G ⟼ {x ↾}_{B}) ↾}_{K} \in (L LMHom D)$
48	19 46 47	syl2anc	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to {(x \in G ⟼ {x ↾}_{B}) ↾}_{K} \in (L LMHom D)$
49	13 48	eqeltrid	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to F \in (L LMHom D)$
50	5	fvtresfn	$⊢ a \in K \to F (a) = {a ↾}_{B}$
51		ssexg	$⊢ (B \subseteq A \cup B \land A \cup B \in V) \to B \in V$
52	14 51	mpan	$⊢ A \cup B \in V \to B \in V$
53	52	3ad2ant2	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to B \in V$
54	7 3	pws0g	$⊢ (R \in Mnd \land B \in V) \to B \times \{\underset{˙}{0}\} = 0_{D}$
55	23 53 54	syl2anc	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to B \times \{\underset{˙}{0}\} = 0_{D}$
56	55	eqcomd	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to 0_{D} = B \times \{\underset{˙}{0}\}$
57	50 56	eqeqan12rd	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in K) \to (F (a) = 0_{D} \leftrightarrow {a ↾}_{B} = B \times \{\underset{˙}{0}\})$
58		reseq1	$⊢ y = a \to {y ↾}_{A} = {a ↾}_{A}$
59	58	eqeq1d	$⊢ y = a \to ({y ↾}_{A} = A \times \{\underset{˙}{0}\} \leftrightarrow {a ↾}_{A} = A \times \{\underset{˙}{0}\})$
60	59 4	elrab2	$⊢ a \in K \leftrightarrow (a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\})$
61		uneq12	$⊢ ({a ↾}_{A} = A \times \{\underset{˙}{0}\} \land {a ↾}_{B} = B \times \{\underset{˙}{0}\}) \to ({a ↾}_{A}) \cup ({a ↾}_{B}) = (A \times \{\underset{˙}{0}\}) \cup (B \times \{\underset{˙}{0}\})$
62		resundi	$⊢ {a ↾}_{(A \cup B)} = ({a ↾}_{A}) \cup ({a ↾}_{B})$
63		xpundir	$⊢ (A \cup B) \times \{\underset{˙}{0}\} = (A \times \{\underset{˙}{0}\}) \cup (B \times \{\underset{˙}{0}\})$
64	61 62 63	3eqtr4g	$⊢ ({a ↾}_{A} = A \times \{\underset{˙}{0}\} \land {a ↾}_{B} = B \times \{\underset{˙}{0}\}) \to {a ↾}_{(A \cup B)} = (A \cup B) \times \{\underset{˙}{0}\}$
65	64	adantll	$⊢ ((a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\}) \land {a ↾}_{B} = B \times \{\underset{˙}{0}\}) \to {a ↾}_{(A \cup B)} = (A \cup B) \times \{\underset{˙}{0}\}$
66	65	adantl	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land ((a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\}) \land {a ↾}_{B} = B \times \{\underset{˙}{0}\})) \to {a ↾}_{(A \cup B)} = (A \cup B) \times \{\underset{˙}{0}\}$
67		eqid	$⊢ {Base}_{R} = {Base}_{R}$
68		simpl1	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land ((a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\}) \land {a ↾}_{B} = B \times \{\underset{˙}{0}\})) \to R \in LMod$
69		simp2	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to A \cup B \in V$
70	69	adantr	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land ((a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\}) \land {a ↾}_{B} = B \times \{\underset{˙}{0}\})) \to A \cup B \in V$
71		simprll	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land ((a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\}) \land {a ↾}_{B} = B \times \{\underset{˙}{0}\})) \to a \in G$
72	1 67 2 68 70 71	pwselbas	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land ((a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\}) \land {a ↾}_{B} = B \times \{\underset{˙}{0}\})) \to a : A \cup B ⟶ {Base}_{R}$
73		ffn	$⊢ a : A \cup B ⟶ {Base}_{R} \to a Fn (A \cup B)$
74		fnresdm	$⊢ a Fn (A \cup B) \to {a ↾}_{(A \cup B)} = a$
75	72 73 74	3syl	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land ((a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\}) \land {a ↾}_{B} = B \times \{\underset{˙}{0}\})) \to {a ↾}_{(A \cup B)} = a$
76	1 3	pws0g	$⊢ (R \in Mnd \land A \cup B \in V) \to (A \cup B) \times \{\underset{˙}{0}\} = 0_{E}$
77	23 69 76	syl2anc	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to (A \cup B) \times \{\underset{˙}{0}\} = 0_{E}$
78	1	pwslmod	$⊢ (R \in LMod \land A \cup B \in V) \to E \in LMod$
79	78	3adant3	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to E \in LMod$
80	43	lsssubg	$⊢ (E \in LMod \land K \in LSubSp (E)) \to K \in SubGrp (E)$
81	79 46 80	syl2anc	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to K \in SubGrp (E)$
82		eqid	$⊢ 0_{E} = 0_{E}$
83	8 82	subg0	$⊢ K \in SubGrp (E) \to 0_{E} = 0_{L}$
84	81 83	syl	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to 0_{E} = 0_{L}$
85	77 84	eqtrd	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to (A \cup B) \times \{\underset{˙}{0}\} = 0_{L}$
86	85	adantr	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land ((a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\}) \land {a ↾}_{B} = B \times \{\underset{˙}{0}\})) \to (A \cup B) \times \{\underset{˙}{0}\} = 0_{L}$
87	66 75 86	3eqtr3d	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land ((a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\}) \land {a ↾}_{B} = B \times \{\underset{˙}{0}\})) \to a = 0_{L}$
88	87	exp32	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to ((a \in G \land {a ↾}_{A} = A \times \{\underset{˙}{0}\}) \to ({a ↾}_{B} = B \times \{\underset{˙}{0}\} \to a = 0_{L}))$
89	60 88	syl5bi	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to (a \in K \to ({a ↾}_{B} = B \times \{\underset{˙}{0}\} \to a = 0_{L}))$
90	89	imp	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in K) \to ({a ↾}_{B} = B \times \{\underset{˙}{0}\} \to a = 0_{L})$
91	57 90	sylbid	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in K) \to (F (a) = 0_{D} \to a = 0_{L})$
92	91	ralrimiva	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to \forall a \in K (F (a) = 0_{D} \to a = 0_{L})$
93		lmghm	$⊢ F \in (L LMHom D) \to F \in (L GrpHom D)$
94	8 2	ressbas2	$⊢ K \subseteq G \to K = {Base}_{L}$
95	10 94	ax-mp	$⊢ K = {Base}_{L}$
96		eqid	$⊢ 0_{L} = 0_{L}$
97		eqid	$⊢ 0_{D} = 0_{D}$
98	95 16 96 97	ghmf1	$⊢ F \in (L GrpHom D) \to (F : K \underset{1-1}{⟶} {Base}_{D} \leftrightarrow \forall a \in K (F (a) = 0_{D} \to a = 0_{L}))$
99	49 93 98	3syl	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to (F : K \underset{1-1}{⟶} {Base}_{D} \leftrightarrow \forall a \in K (F (a) = 0_{D} \to a = 0_{L}))$
100	92 99	mpbird	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to F : K \underset{1-1}{⟶} {Base}_{D}$
101		eqid	$⊢ {Base}_{L} = {Base}_{L}$
102	101 16	lmhmf	$⊢ F \in (L LMHom D) \to F : {Base}_{L} ⟶ {Base}_{D}$
103		frn	$⊢ F : {Base}_{L} ⟶ {Base}_{D} \to ran F \subseteq {Base}_{D}$
104	49 102 103	3syl	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to ran F \subseteq {Base}_{D}$
105		reseq1	$⊢ x = a \cup (A \times \{\underset{˙}{0}\}) \to {x ↾}_{B} = {(a \cup (A \times \{\underset{˙}{0}\})) ↾}_{B}$
106	7 67 16	pwselbasb	$⊢ (R \in LMod \land B \in V) \to (a \in {Base}_{D} \leftrightarrow a : B ⟶ {Base}_{R})$
107	20 53 106	syl2anc	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to (a \in {Base}_{D} \leftrightarrow a : B ⟶ {Base}_{R})$
108	107	biimpa	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to a : B ⟶ {Base}_{R}$
109	3	fvexi	$⊢ \underset{˙}{0} \in V$
110	109	fconst	$⊢ (A \times \{\underset{˙}{0}\}) : A ⟶ \{\underset{˙}{0}\}$
111	110	a1i	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to (A \times \{\underset{˙}{0}\}) : A ⟶ \{\underset{˙}{0}\}$
112	23	adantr	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to R \in Mnd$
113	67 3	mndidcl	$⊢ R \in Mnd \to \underset{˙}{0} \in {Base}_{R}$
114	112 113	syl	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to \underset{˙}{0} \in {Base}_{R}$
115	114	snssd	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to \{\underset{˙}{0}\} \subseteq {Base}_{R}$
116	111 115	fssd	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to (A \times \{\underset{˙}{0}\}) : A ⟶ {Base}_{R}$
117		incom	$⊢ B \cap A = A \cap B$
118		simp3	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to A \cap B = \emptyset$
119	117 118	syl5eq	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to B \cap A = \emptyset$
120	119	adantr	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to B \cap A = \emptyset$
121		fun	$⊢ ((a : B ⟶ {Base}_{R} \land (A \times \{\underset{˙}{0}\}) : A ⟶ {Base}_{R}) \land B \cap A = \emptyset) \to (a \cup (A \times \{\underset{˙}{0}\})) : B \cup A ⟶ {Base}_{R} \cup {Base}_{R}$
122	108 116 120 121	syl21anc	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to (a \cup (A \times \{\underset{˙}{0}\})) : B \cup A ⟶ {Base}_{R} \cup {Base}_{R}$
123		uncom	$⊢ B \cup A = A \cup B$
124		unidm	$⊢ {Base}_{R} \cup {Base}_{R} = {Base}_{R}$
125	123 124	feq23i	$⊢ (a \cup (A \times \{\underset{˙}{0}\})) : B \cup A ⟶ {Base}_{R} \cup {Base}_{R} \leftrightarrow (a \cup (A \times \{\underset{˙}{0}\})) : A \cup B ⟶ {Base}_{R}$
126	122 125	sylib	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to (a \cup (A \times \{\underset{˙}{0}\})) : A \cup B ⟶ {Base}_{R}$
127	1 67 2	pwselbasb	$⊢ (R \in LMod \land A \cup B \in V) \to (a \cup (A \times \{\underset{˙}{0}\}) \in G \leftrightarrow (a \cup (A \times \{\underset{˙}{0}\})) : A \cup B ⟶ {Base}_{R})$
128	127	3adant3	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to (a \cup (A \times \{\underset{˙}{0}\}) \in G \leftrightarrow (a \cup (A \times \{\underset{˙}{0}\})) : A \cup B ⟶ {Base}_{R})$
129	128	adantr	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to (a \cup (A \times \{\underset{˙}{0}\}) \in G \leftrightarrow (a \cup (A \times \{\underset{˙}{0}\})) : A \cup B ⟶ {Base}_{R})$
130	126 129	mpbird	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to a \cup (A \times \{\underset{˙}{0}\}) \in G$
131		simpl3	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to A \cap B = \emptyset$
132	117 131	syl5eq	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to B \cap A = \emptyset$
133		ffn	$⊢ a : B ⟶ {Base}_{R} \to a Fn B$
134		fnresdisj	$⊢ a Fn B \to (B \cap A = \emptyset \leftrightarrow {a ↾}_{A} = \emptyset)$
135	108 133 134	3syl	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to (B \cap A = \emptyset \leftrightarrow {a ↾}_{A} = \emptyset)$
136	132 135	mpbid	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to {a ↾}_{A} = \emptyset$
137		fnconstg	$⊢ \underset{˙}{0} \in V \to (A \times \{\underset{˙}{0}\}) Fn A$
138		fnresdm	$⊢ (A \times \{\underset{˙}{0}\}) Fn A \to {(A \times \{\underset{˙}{0}\}) ↾}_{A} = A \times \{\underset{˙}{0}\}$
139	109 137 138	mp2b	$⊢ {(A \times \{\underset{˙}{0}\}) ↾}_{A} = A \times \{\underset{˙}{0}\}$
140	139	a1i	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to {(A \times \{\underset{˙}{0}\}) ↾}_{A} = A \times \{\underset{˙}{0}\}$
141	136 140	uneq12d	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to ({a ↾}_{A}) \cup ({(A \times \{\underset{˙}{0}\}) ↾}_{A}) = \emptyset \cup (A \times \{\underset{˙}{0}\})$
142		resundir	$⊢ {(a \cup (A \times \{\underset{˙}{0}\})) ↾}_{A} = ({a ↾}_{A}) \cup ({(A \times \{\underset{˙}{0}\}) ↾}_{A})$
143		uncom	$⊢ \emptyset \cup (A \times \{\underset{˙}{0}\}) = (A \times \{\underset{˙}{0}\}) \cup \emptyset$
144		un0	$⊢ (A \times \{\underset{˙}{0}\}) \cup \emptyset = A \times \{\underset{˙}{0}\}$
145	143 144	eqtr2i	$⊢ A \times \{\underset{˙}{0}\} = \emptyset \cup (A \times \{\underset{˙}{0}\})$
146	141 142 145	3eqtr4g	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to {(a \cup (A \times \{\underset{˙}{0}\})) ↾}_{A} = A \times \{\underset{˙}{0}\}$
147		reseq1	$⊢ y = a \cup (A \times \{\underset{˙}{0}\}) \to {y ↾}_{A} = {(a \cup (A \times \{\underset{˙}{0}\})) ↾}_{A}$
148	147	eqeq1d	$⊢ y = a \cup (A \times \{\underset{˙}{0}\}) \to ({y ↾}_{A} = A \times \{\underset{˙}{0}\} \leftrightarrow {(a \cup (A \times \{\underset{˙}{0}\})) ↾}_{A} = A \times \{\underset{˙}{0}\})$
149	148 4	elrab2	$⊢ a \cup (A \times \{\underset{˙}{0}\}) \in K \leftrightarrow (a \cup (A \times \{\underset{˙}{0}\}) \in G \land {(a \cup (A \times \{\underset{˙}{0}\})) ↾}_{A} = A \times \{\underset{˙}{0}\})$
150	130 146 149	sylanbrc	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to a \cup (A \times \{\underset{˙}{0}\}) \in K$
151	130	resexd	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to {(a \cup (A \times \{\underset{˙}{0}\})) ↾}_{B} \in V$
152	5 105 150 151	fvmptd3	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to F (a \cup (A \times \{\underset{˙}{0}\})) = {(a \cup (A \times \{\underset{˙}{0}\})) ↾}_{B}$
153		resundir	$⊢ {(a \cup (A \times \{\underset{˙}{0}\})) ↾}_{B} = ({a ↾}_{B}) \cup ({(A \times \{\underset{˙}{0}\}) ↾}_{B})$
154		fnresdm	$⊢ a Fn B \to {a ↾}_{B} = a$
155	108 133 154	3syl	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to {a ↾}_{B} = a$
156		ffn	$⊢ (A \times \{\underset{˙}{0}\}) : A ⟶ \{\underset{˙}{0}\} \to (A \times \{\underset{˙}{0}\}) Fn A$
157		fnresdisj	$⊢ (A \times \{\underset{˙}{0}\}) Fn A \to (A \cap B = \emptyset \leftrightarrow {(A \times \{\underset{˙}{0}\}) ↾}_{B} = \emptyset)$
158	110 156 157	mp2b	$⊢ A \cap B = \emptyset \leftrightarrow {(A \times \{\underset{˙}{0}\}) ↾}_{B} = \emptyset$
159	158	biimpi	$⊢ A \cap B = \emptyset \to {(A \times \{\underset{˙}{0}\}) ↾}_{B} = \emptyset$
160	159	3ad2ant3	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to {(A \times \{\underset{˙}{0}\}) ↾}_{B} = \emptyset$
161	160	adantr	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to {(A \times \{\underset{˙}{0}\}) ↾}_{B} = \emptyset$
162	155 161	uneq12d	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to ({a ↾}_{B}) \cup ({(A \times \{\underset{˙}{0}\}) ↾}_{B}) = a \cup \emptyset$
163		un0	$⊢ a \cup \emptyset = a$
164	162 163	eqtrdi	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to ({a ↾}_{B}) \cup ({(A \times \{\underset{˙}{0}\}) ↾}_{B}) = a$
165	153 164	syl5eq	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to {(a \cup (A \times \{\underset{˙}{0}\})) ↾}_{B} = a$
166	152 165	eqtrd	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to F (a \cup (A \times \{\underset{˙}{0}\})) = a$
167	95 16	lmhmf	$⊢ F \in (L LMHom D) \to F : K ⟶ {Base}_{D}$
168		ffn	$⊢ F : K ⟶ {Base}_{D} \to F Fn K$
169	49 167 168	3syl	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to F Fn K$
170	169	adantr	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to F Fn K$
171		fnfvelrn	$⊢ (F Fn K \land a \cup (A \times \{\underset{˙}{0}\}) \in K) \to F (a \cup (A \times \{\underset{˙}{0}\})) \in ran F$
172	170 150 171	syl2anc	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to F (a \cup (A \times \{\underset{˙}{0}\})) \in ran F$
173	166 172	eqeltrrd	$⊢ ((R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \land a \in {Base}_{D}) \to a \in ran F$
174	104 173	eqelssd	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to ran F = {Base}_{D}$
175		dff1o5	$⊢ F : K \underset{1-1 onto}{⟶} {Base}_{D} \leftrightarrow (F : K \underset{1-1}{⟶} {Base}_{D} \land ran F = {Base}_{D})$
176	100 174 175	sylanbrc	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to F : K \underset{1-1 onto}{⟶} {Base}_{D}$
177	95 16	islmim	$⊢ F \in (L LMIso D) \leftrightarrow (F \in (L LMHom D) \land F : K \underset{1-1 onto}{⟶} {Base}_{D})$
178	49 176 177	sylanbrc	$⊢ (R \in LMod \land A \cup B \in V \land A \cap B = \emptyset) \to F \in (L LMIso D)$

Metamath Proof Explorer

Theorem pwssplit4

Proof