Metamath Proof Explorer

Theorem 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 ⊢ 𝐸 = ( 𝑅 ↑s ( 𝐴 ∪ 𝐵 ) )
pwssplit4.g ⊢ 𝐺 = ( Base ‘ 𝐸 )
pwssplit4.z ⊢ 0 = ( 0g ‘ 𝑅 )
pwssplit4.k ⊢ 𝐾 = { 𝑦 ∈ 𝐺 ∣ ( 𝑦 ↾ 𝐴 ) = ( 𝐴 × { 0 } ) }
pwssplit4.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ↾ 𝐵 ) )
pwssplit4.c ⊢ 𝐶 = ( 𝑅 ↑s 𝐴 )
pwssplit4.d ⊢ 𝐷 = ( 𝑅 ↑s 𝐵 )
pwssplit4.l ⊢ 𝐿 = ( 𝐸 ↾s 𝐾 )
Assertion pwssplit4 ( ( 𝑅 ∈ LMod ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐹 ∈ ( 𝐿 LMIso 𝐷 ) )

Proof

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